Specific Logical Frameworks and Implementations

This provides pointers to the logical frameworks ALF, Automath, ELAN, Elf, Forum, Isabelle, lambda Prolog, Pi. Pointers to related systems are provided at the end.
ALF (Another Logical Framework) is a logical framework based on Martin-Löf type theory.
Automath was the first logical framework, developed by N.G. de Bruijn. A book Selected Papers on Automath, edited by R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer has appeared as volume 133 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1994.
ELAN is a logical framework based on rewriting logic developed by the PROTHEO group managed by Claude Kirchner (CRIN-CNRS & INRIA Lorraine).
Elf is a constraint logic programming language based on (Edinburgh) LF. It is now integrated in the Twelf implementation (see below).
Forum is a framework based on classical linear logic.
Isabelle is a generic theorem prover based on higher-order resolution and tactics.
lambda Prolog
lambda Prolog is a logic programming language based on hereditary Harrop formulas.
Maude is a reflective language and system supporting equational and rewriting logic specfication and programming.
Pi is a generic logic based on partial inductive definitions.
Twelf is a meta-logical framework based on (Edinburgh) LF. It includes an implementation of the Elf constraint logic programming language. The implementation in Standard ML is available for a variety of architectures.

Pointers to home pages for related topics and systems:
  • ACL2
  • AF2 Proof Assistant
  • Coq
  • HOL
  • LEGO
  • Proof General,

    a generic Emacs interface for proof assistants. It is supplied ready-customised for Coq, Isabelle and LEGO.

  • Mizar
  • Nuprl
  • Yarrow Proof Assistant for Pure Type Systems.
  • Mechanized Reasoning (mirrored in Europe)
  • Formal Methods
  • Logic Programming
  • ... others to follow as the information is made available to me ...

  • Further pointers to logical frameworks:
  • Homepage for Logical Frameworks
  • Bibliography on Logical Frameworks
  • Some Researchers in the Area
  • What's New in Logical Frameworks
  • Last Updated: Sun Jun 22 1997
    Frank Pfenning