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