Skip to content
STELF
Documentation out of dateLearn more

Adequacy

STELF is based on the logical framework LF. When we write down a logical system (an object logic such as a programming language) in STELF, 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 STELF, as well as Harper and Licata’s paper , for example adequacy statements and proofs.

References

Section titled “References”