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

James Cheney, Michael Norrish, René Vestergaard

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Pages (from-to)209-239
Number of pages31
JournalJournal of Automated Reasoning
Volume49
Issue number2
DOIs
Publication statusPublished - 2012

Keywords / Materials (for Non-textual outputs)

  • Adequacy
  • Isomorphism
  • Interpretation
  • Nominal abstract syntax
  • Higher-order abstract syntax

Fingerprint

Dive into the research topics of 'Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax'. Together they form a unique fingerprint.

Cite this