Trustworthy Systems

Formalizing adequacy

Authors

James Cheney, René Vestergaard and Michael Norrish

University of Edinburgh

JAIST

NICTA

Abstract

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

BibTeX Entry

  @inproceedings{Cheney_VN_09,
    address          = {York},
    author           = {Cheney, James and Vestergaard, Ren\'e and Norrish, Michael},
    booktitle        = {2nd International Workshop on Theory and Applications of Abstraction, Substitution and Naming},
    editor           = {{Maribel Fernández}},
    month            = mar,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/1804.pdf},
    title            = {Formalizing adequacy},
    year             = {2009}
  }

Download