# Adequacy

### From The Twelf Project

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:

- There is a bijection between object language entities and LF objects of a particular type (the "bijection" part).
- 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

- ↑
*Robert Harper, Daniel R. Licata*-**Mechanizing Metatheory in a Logical Framework**

*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.