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

- specification of deductive systems,
- search for derivations within deductive systems,
- meta-programming of algorithms pertaining to deductive systems,
- proving meta-theorems about deductive systems.

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