The Elf Meta-Language

Elf is a constraint logic programming language based on the LF Logical Framework. It has no connection whatsoever to the ELF® statistical package, a commercial product by The Winchendon Group, Inc.

Elf is a uniform meta-language for specifying, implementing, and proving properties of programming languages and logics. It has been applied to various examples, some of which are described in published papers accessible through a bibliography on LF and Elf. Others are described in the notes to a course on Computation and Deduction, which are not yet publicly available. There is also a more complete bibliography on logical frameworks in general. Work on LF and Elf at Carnegie Mellon University is supported by NSF grant CCR-9303383 (Principal Investigators Robert Harper and Frank Pfenning)

Implementation

The implementation of Elf (click here to retrieve the sources as a compressed tar file) is an interpreter written in Standard ML and the execution is slow compared to Prolog. However, type-checking is quite efficient and there are number of optimizations which make it practical for small and medium-sized examples (click here to retrive the examples as a compressed tar file). The implementation also provides an Emacs interface for editing and interacting with an inferior Elf server process. There is no manual, but there are some helpful hints and implementation notes.

The principal contributors to this implementation of Elf are

Thanks also to Conal Elliott and Ken Cline whose first Lisp prototype was influential on the design of this SML implementation.

The installation of Elf requires Standard ML of New Jersey, although it should be easy to port to other implementations of Standard ML. Versions 0.72 and greater are more likely to work than older versions (we recommend version 0.93). Currently, SML of NJ can be retrieved via anonymous ftp from princeton.edu (net address 128.112.128.1), directory pub/ml. For up-to-date information on Standard ML of New Jersey, contact David MacQueen (macqueen@research.att.com). It is available for a large number of machine architectures.

There is a mailing list with announcements about Elf. Please send mail to elf-request@cs.cmu.edu to join the list. For further information contact

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

Email: fp@cs
Phone: +1 412 268-6343
Fax : +1 412 268-5576

fp@cs