Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax
Adequacy is an important criterion for judging whether a formalization is suitable for reasoning about the actual object of study. The issue is particularly subtle in the expansive case of approaches to languages with name-binding. In prior work, adequacy has been formalized only with respect to specific representation techniques. In this article, we give a general formal definition based on model-theoretic isomorphisms or interpretations. We investigate and formalize an adequate interpretation...[Show more]
|Collections||ANU Research Publications|
|Source:||Journal of Automated Reasoning|
|01_Cheney_Formalizing_Adequacy:_A_Case_2012.pdf||871.45 kB||Adobe PDF||Request a copy|
|02_Cheney_Formalizing_Adequacy:_A_Case_2012.pdf||1 MB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.