Formalizing adequacy

Select |




Print


Cheney, James; Vestergaard, René; Norrish, Michael

Cheney, James; Vestergaard, René; Norrish, Michael


2009-03-22


Conference Material


Journal of Automated Reasoning


Journal of Automated Reasoning


York


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


http://www.dcs.kcl.ac.uk/staff/maribel/TAASN.html


nicta:1804


Cheney, James; Vestergaard, René; Norrish, Michael. Formalizing adequacy. In: Maribel Fernández Editor, editor/s. Journal of Automated Reasoning; York. 2009-03-22.



Loading citation data...

Citation counts
(Requires subscription to view)