Logic programming

From The Twelf Project
Jump to: navigation, search

Most of the articles and examples on this wiki are focused towards using Twelf as a specification language, useful for encoding an object logic and then stating and proving metatheorems about that object logic. However, Twelf originated from Elf, and like Elf it is a dependently-typed, higher-order logic programming language based on the logic LF.

A Twelf signature may contain, among other things, some type family declarations and some constants inhabiting those type families. A logic programming language takes a type as an input, and it then uses a simple search strategy to try and discover a term that has that type using the constants that have been defined. By the judgments as types principle, this means that Twelf is searching for a derivation - a proof witness - of a particular judgment.

Twelf's logic programming engine is activated by %solve and %query directives. It can also be activated directly inside ML; see the section on interactive queries in the User's Guide for more information. Twelf's tabled logic programming engine is activated by the %querytabled directive.

Uses of logic programming in Twelf

  • Implementing a reference typechecker/evaluator - If the static and dynamic semantics of a programming language are written correctly, then the specification of the static semantics can be . This was a component to the The POPLmark Challenge challenge; the case study of a language with references, among other examples, demonstarte Twelf in this capacity.
  • Writing programs and then proving things about them: The TALT project [1] includes a code checker written as a Twelf logic program, along with a proof in Twelf that code that passes the checker is safe according to a safety policy.
  • Tactical theorem proving - in the style described by Appel and Felty in [2].

See also

References

  1. Karl Crary - Toward a Foundational Typed Assembly Language
    2003 Symposium on Principles of Programming Languages ,2003
    Bibtex
    Author : Karl Crary
    Title : Toward a Foundational Typed Assembly Language
    In : 2003 Symposium on Principles of Programming Languages -
    Address :
    Date : 2003
  2. Andrew W. Appel, Amy P. Felty - Dependent Types Ensure Partial Correctness of Theorem Provers
    Journal of Functional Programming 14(1):3--19, January 2004
    Bibtex
    Author : Andrew W. Appel, Amy P. Felty
    Title : Dependent Types Ensure Partial Correctness of Theorem Provers
    In : Journal of Functional Programming -
    Address :
    Date : January 2004