Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax
Date
2012
Authors
Cheney, James
Norrish, Michael
Vestergaard, Rene
Journal Title
Journal ISSN
Volume Title
Publisher
Kluwer Academic Publishers
Abstract
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.
Description
Keywords
Keywords: Abstract syntax; Adequacy; Higher-order abstract syntax; Interpretation; Isomorphism; Differentiation (calculus); Set theory; Syntactics; Abstracting Adequacy; Higher-order abstract syntax; Interpretation; Isomorphism; Nominal abstract syntax
Citation
Collections
Source
Journal of Automated Reasoning
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31