Adequacy

From The Twelf Project

Jump to: navigation, search

Twelf is based on the logical framework LF. When we write down a logical system (an object logic such as a programming language) in Twelf, we are defining the objects and judgments of our language as LF types and terms. The correctness criterion for such a representation is called adequacy. An LF representation is adequate iff it is isomorphic to the original description of the object logic. Specifically, we require a compositional bijection between the original description and the LF representations, which means that:

  1. There is a bijection between object language entities and LF objects of a particular type (the "bijection" part).
  2. For representations that use higher-order abstract syntax and higher-order judgments, LF's notion of substitution correctly models object-language substitution (the "compositional" part).

See the introductory article Proving metatheorems with Twelf, as well as Harper and Licata's paper [1], for example adequacy statements and proofs.

[edit] References

  1. Robert Harper, Daniel R. Licata - Mechanizing Metatheory in a Logical Framework
    Journal of Functional Programming , 2007
    Bibtex
    Auteur : Robert Harper, Daniel R. Licata
    Titre : Mechanizing Metatheory in a Logical Framework
    Dans : Journal of Functional Programming -
    Adresse :
    Date : 2007

Robert Harper, Furio Honsell, Gordon Plotkin - A framework for defining logics
J. ACM 40(1):143--184, New York, NY, USA, 1993
Bibtex
Auteur : Robert Harper, Furio Honsell, Gordon Plotkin
Titre : A framework for defining logics
Dans : J. ACM -
Adresse : New York, NY, USA
Date : 1993

This page is incomplete. We should expand it.
Personal tools