Trustworthy Systems

Formalizing adequacy: A case study for higher-order abstract syntax

Authors

James Cheney, Michael Norrish and Ren\'e Vestergaard

University of Edinburgh\ NICTA\ Australian National University\ JAIST

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.

BibTeX Entry

  @article{Cheney_NV_12,
    author           = {Cheney, James and Norrish, Michael and Vestergaard, Ren\'e},
    doi              = {10.1007/s10817-011-9221-6},
    journal          = {Journal of Automated Reasoning},
    month            = aug,
    number           = {2},
    pages            = {209--239},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4836.pdf},
    title            = {Formalizing Adequacy: A Case Study for Higher-order Abstract Syntax},
    volume           = {49},
    year             = {2012}
  }

Download