Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax

Select |




Print


Cheney, James; Norrish, Michael; Vestergaard, René

Cheney, James; Norrish, Michael; Vestergaard, René


2012-08-01


Journal Article


Journal of Automated Reasoning


49


2


209--239


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 of untyped lambda-calculus within a higher-order metalanguage in Isabelle/HOL using the Nominal Datatype Package. Formalization elucidates some subtle issues that have been neglected in informal arguments concerning adequacy.


https://doi.org/10.1007/s10817-011-9221-6


nicta:4836


Cheney, James; Norrish, Michael; Vestergaard, René. Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax. Journal of Automated Reasoning. 2012-08-01; 49(2):209--239. https://doi.org/10.1007/s10817-011-9221-6



Loading citation data...

Citation counts
(Requires subscription to view)