Logical Frameworks

This is a home page for logical frameworks providing pointers to further material, including a bibliography, implementations, some researchers in the area, and recent announcements and papers. A searchable version of this bibliography is now also available. Another useful source for information is the homepage of the Esprit Working Group on Types for Proofs and Programs.

A logical framework is a formal meta-language for deductive systems. The primary tasks supported in logical frameworks to varying degrees are

I include here systems that in other places have been called meta-logics and meta-logical frameworks; for me the choice of terminology merely indicates the relative emphasis placed on these tasks. Logical frameworks have been applied to many examples from logic and the theory of programming languages. A short survey on logical frameworks provides a guide to some papers in this bibliography as of late 1995. Here are short-cuts to home pages for logical frameworks where available: ELAN, Elf, Forum, Isabelle, lambda Prolog.

Important Disclaimer: In order to keep the task of compiling this material manageable I excluded general-purpose theorem proving systems designed for the formalization of classical or constructive mathematics, such as Coq, HOL, LEGO, Mizar, NQTHM, Nuprl, and many others. However, I included individual experiments carried out in these systems that are meta-logical in nature. I am also providing pointers to home pages for related systems and topics where available.

  • Bibliography on Logical Frameworks
  • Specific Frameworks and Implementations
  • Some Researchers in the Area
  • What's New in Logical Frameworks

    • Frank Pfenning

    fp@cs