CMU Artificial Intelligence Repository
Home INFO Search FAQs Repository Root

Elf: LF Logical Framework

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