Specific Logical Frameworks and Implementations

ALF

ALF (Another Logical Framework) is a logical framework based on Martin-Löf type theory.

• Implementation
• Contact: Lena Magnusson, lena@cs.chalmers.se

Automath

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.

• Contact: N.G. de Bruijn, wsdwnb@win.tue.nl or
  Herman Geuvers, herman@info.win.tue.nl

ELAN

ELAN is a logical framework based on rewriting logic developed by the PROTHEO group managed by Claude Kirchner (CRIN-CNRS & INRIA Lorraine).

• Home page
• Contact: Marian Vittek, Marion.Vittek@loria.fr

Elf

Elf is a constraint logic programming language based on (Edinburgh) LF. It is now integrated in the Twelf implementation (see below).

• Home page
• Implementation: in Standard ML (of New Jersey)
• Mailing list: elf-list@cs.cmu.edu;
  use elf-list-request@cs.cmu.edu for administrative requests
• Contact: Frank Pfenning, fp@cs

Forum

Forum is a framework based on classical linear logic.

• Home page
• Contact Dale Miller, dale@saul.cis.upenn.edu

Isabelle

Isabelle is a generic theorem prover based on higher-order resolution and tactics.

• Home page
• Implementation: available from Cambridge or
  from the Technical University of Munich
• Mailing list: isabelle-users@cl.cam.ac.uk;
  use isabelle-users-request@cl.cam.ac.uk for administrative requests.
• Contact: Larry Paulson, Larry.Paulson@cl.cam.ac.uk or
  Tobias Nipkow, Tobias.Nipkow@Informatik.TU-Muenchen.De

lambda Prolog

lambda Prolog is a logic programming language based on hereditary Harrop formulas.

• Home page
• Implementations: (see also this index)
  • lambda Prolog/Mali which compiles to C (contact: pm@irisa.fr),
  • Standard ML version of eLP (contact Amy Felty, felty@bell-labs.com),
  • a WAM-based compiler (in progress, contact Gopalan Nadathur, gopalan@cs.uchicago.edu).
  • eLP, an interpreter written in Common Lisp (no longer maintained, contact Frank Pfenning, fp@cs),
• Mailing list: lprolog@cis.upenn.edu;
  use lprolog-request@cis.upenn.edu for administrative requests.
• Contact: Dale Miller, dale@saul.cis.upenn.edu or
  Gopalan Nadathur, gopalan@cs.uchicago.edu.

Maude

Maude is a reflective language and system supporting equational and rewriting logic specfication and programming.

• Home page
• Mailing list: maude@csl.sri.com;
  use maude-request@csl.sri.com for administrative requests

Pi

Pi is a generic logic based on partial inductive definitions.

• Contact: Lars Eriksson, lhe@sics.se

Twelf

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.

• Home page
• Mailing list: elf-list@cs.cmu.edu;
  use elf-list-request@cs.cmu.edu for administrative requests
• Contact: Frank Pfenning, fp@cs

Last Updated: Sun Jun 22 1997
Frank Pfenning