Reseña: Formalizing adequacy: A case study for higher-order abstract syntax
Se ha publicado un nuevo trabajo de razonamiento formalizado en Isabelle: Formalizing adequacy: A case study for higher-order abstract syntax.
Sus autores son James Cheney, Michael Norrish y René Vestergaard.
Su resumen es
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.
La formalización en Isabelle se encuentra aquí.