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

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.