Formalizing adequacy

James Cheney, Rene Vestergaard, Michael Norrish

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Adequacy is an important criterion for judging the correctness of formal reasoning. The issue is particularly subtle in the expansive case of approaches to languages with name-binding. We posit that adequacy of a novel representation technique is best addressed by formalizing an isomorphism or, more generally, an interpretation explicating the new approach in terms of a more conventional one. We present an example formalization of an isomorphism relating nominal and higher-order abstract syntax techniques. We also outline steps towards a systematic framework that could be used for proving adequacy results automatically, which we believe would help make representation techniques more transparent to end-users of mechanized metatheory verification systems, and provide insight into the relative merits of different approaches.
Original languageEnglish
Title of host publication2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming
EditorsMaribel Fernández
Publication statusPublished - Mar 2009

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'. Together they form a unique fingerprint.

Cite this