CMU Artificial Intelligence Repository
Elf: LF Logical Framework
areas/reasonng/atp/systems/elf/
Elf implements the LF Logical Framework (based on the theory of
dependent types) and gives it a logic programming interpretation in
order to support search and the implementation of other algorithms (e.g.
evaluation or compilation in programming languages). It comes with a
number of examples from logic and the theory of programming languages
such as the Church Rosser theorem for the untyped lambda-calculus and
type soundness for Mini-ML. It includes some support code for
editing and interaction in GNU Emacs.
Origin:
ftp.cs.cmu.edu:/afs/cs/user/fp/public/
as the files
README (general information)
elf-04.tar.Z (Version 0.4 of Elf, 1 Jul 1993)
elf-examples.tar.Z (Version 0.4 of Elf examples,
unchanged from Version 0.3),
elf-papers/* (DVI files for papers related to
LF and Elf, including a
"tutorial" and a bibliography)
Version: 0.4 (1-JUL-93)
Requires: Standard ML of New Jersey
CD-ROM: Prime Time Freeware for AI, Issue 1-1
Mailing List: To join the mailing list, send mail to
elf-request@cs.cmu.edu.
Author(s): Frank Pfenning, Ekkehard Rohwedder, Spiro Michaylov,
Contact: Frank Pfenning
School of Computer Science
Carnegie Mellon University
Pittsburgh, PA 15213-3891 USA
Tel: +1 412 268-6343
Fax: +1 412 681-5739
Keywords:
Authors!Michaylov, Authors!Pfenning, Authors!Rohwedder,
Automated Reasoning, Church Rosser Theorem, Dependent Types,
Elf, GNU Emacs, LF Logical Framework, Logic Programming,
ML!Code, Reasoning!Automated Reasoning, Search,
Theorem Proving, Type Checking
References: ?
Last Web update on Mon Feb 13 10:27:29 1995
AI.Repository@cs.cmu.edu