@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
Name:  Elf

Keywords:  logical framework, logic programming, type theory


Description: 
   Semantics:  the LF logical framework based on a predicative type theory
   Deductive machinery:  constraint logic programming
   Dynamics:  used as a specification and programming language
   Persistence:  all data are developed and stored as programs

Contact persons:

  Frank Pfenning
  School of Computer Science
  Carnegie Mellon University
  Pittsburgh, PA 15213-3891
  U.S.A.

  Email: fp@cs.cmu.edu
  Phone: +1 412 268-6343
  Fax  : +1 412 681-5739

User group:
  There is a mailing list with announcement of new papers and
  implementation releases for Elf, elf-list@cs.cmu.edu.  To join
  the list, contact elf-request@cs.cmu.edu.

Pragmatics:
  As a pure logic programming language, Elf is currently not well suited
for interactive development of theories.  On the other hand it lends itself
to the very direct specification of programming languages, type systems,
logics, etc.  One then can program algorithms (for example, for evaluation,
compilation, type inference, or proof search) and express their correctness
proof within the same language.

  The features which make Elf unique in comparison to closely related systems
such as Isabelle or lambdaProlog are the internal notion of deduction and the
very expressive language of types (which includes dependent types).  These
together can be exploited to implement the meta-theory of programming
languages, compiler, logics, etc. (see below).

  The current implementation is an interpreter and even though it is not very
efficient, does some static analysis to obtain reasonable run-time behavior.
It employs a sophisticated term reconstruction algorithm that allows much of
the input information to be ellided without any syntactic restrictions.

Documentation:

There is currently no manual, but there are three papers which serve as
tutorials (see [4,17,25]).  These tutorials,  other Elf-related papers,
and a suite of 16 examples from logic and the theory of programming languages
are distributed via anonymous ftp.   [A current list of Elf-related papers
can be found in ExtendedInfo/elf-bib.  Bib references refer to this
bibliography.]

Three prinicpal papers are:

[1]  Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for
     defining logics.  Journal of the Association for Computing Machinery,
     40(1):143--184, January 1993.

[3]  Frank Pfenning. Logic programming in the LF logical framework. In
     Gerard Huet and Gordon Plotkin, editors, Logical Frameworks, pages
     149--181. Cambridge University Press, 1991.

[17] Spiro Michaylov and Frank Pfenning. Natural semantics and some of its
     meta-theory in Elf. In L.-H. Eriksson, L. Halln"as, and
     P. Schroeder-Heister, editors, Proceedings of the Second International
     Workshop on Extensions of Logic Programming, pages 299--344, Stockholm,
     Sweden, January 1991. Springer-Verlag LNAI 596.

Applications:

  A specification and implementation of Mini-ML, its operational semantics,
  its type system, and a proof of type preservation (see [17])

  An implementation of a compiler for Mini-ML and its correctness proof
  (see [24]).

  A proof of the Church-Rosser theorem for the untyped lambda-calculus
  (see [25]).

  An equivalence proof for Hilbert-style and natural deduction formulations
  of propositional logic (see [12])

Extensions/enhancements:

  We are currently working on an implementation of the module system as
  described in [12].  This combines ideas from ML's module system with work on
  structured presentations of logics [10,11] and work on type theories with
  sigma-types and universes.

Resource requirements:

  Elf is implemented in Standard ML of New Jersey, which runs on a variety
  of architectures.  It requires version 0.72 or greater.  SML of New Jersey
  can be retrieved via anonymous ftp from princeton.edu, directory pub/ml.
  for up-to-date information on Standard ML of New Jersey and supported
  architectures, contact David MacQueen <macqueen@research.att.com>

  No further environment support is required.  Some optional gnu-emacs
  utilities are provided in the distribution.

  I would recommend a minimum of 16mb of memory for small and medium
  size data to be manipulated.  For large proofs and object language
  expression, 24mb give reasonable performance.

Where-to-get-it:

  Retrieving Elf, Version 0.2, Sat Feb 15 12:47:08 1992

  (alonzo.tip.cs.cmu.edu has internet address 128.2.209.194)

  % ftp alonzo.tip.cs.cmu.edu
  Name: anonymous
  Password: (your e-mail address)
  ftp> cd /afs/cs/user/fp/public
  ftp> type binary
  ftp> get elf.tar.Z
  ftp> bye

  % uncompress elf.tar.Z
  % tar -xvf elf.tar
  % rm elf.tar

  This will create a directory elf/ with the sources for the
  implementation and examples in various subdirectories.

  See the file elf/elf/INSTALL for further installation instructions.

  The papers can be found in the directory /afs/cs/user/fp/public/elf-papers

  Be sure to execute the "cd" command exactly as indicated above, or you will
  not be able to read the files in the directory!
  

[Frank Pfenning, January 1993]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%