Release of Twelf 1.2 Logical Framework

To: types@cis.upenn.edu, lprolog-list@cis.upenn.edu, theorem-provers@ai.mit.edu, compunode@compulog.org, bra-types@cs.chalmers.se, elf-list@cs.cmu.edu
Subject: Release of Twelf 1.2 Logical Framework
From: Carsten Schuermann <carsten+@cs.cmu.edu>
Date: Wed, 25 Nov 1998 14:14:29 -0500
CC: fp@cs.cmu.edu, carsten@cs.cmu.edu
Newsgroups: comp.lang.ml, comp.lang.prolog
Organization: School of Computer Science, Carnegie Mellon University
Sender: carsten@postoffice.srv.cs.cmu.edu


                                 Twelf
                              Version 1.2
                             November 1998

                      http://www.cs.cmu.edu/~twelf

We are proud to announce the first release of Twelf (Version 1.2).  The
implementation comprises

     the LF logical framework, including type reconstruction;
     the Elf constraint logic programming language;
     a meta-theorem prover for LF (very preliminary);
     and an Emacs interface.

The principal authors of Twelf are

     Frank Pfenning and
     Carsten Schrmann.

Twelf provides a uniform meta-language for specifying, implementing,
and proving properties of programming languages and logics.  Example
suites include Cartesian Closed Categories and lambda-calculus, the
Church-Rosser theorem for the untyped lambda-calculus, Mini-ML
including type preservation and compilation, cut elimination, theory
of logic programming, and Hilbert's deduction theorem.

It also includes a complete User's Guide and example suite; a tutorial
is available from the Twelf homepage.  Twelf is written in Standard ML
and uses an inference engine based on explicit substitutions.  Twelf
has been developed at Carnegie Mellon University and runs under SML/NJ
and MLWorks on various Unix platforms and Windows 95/98/NT.

We maintain a elf-list@cs.cmu.edu, a low-volume moderated mailing list
for announcements regarding Elf and its implementation in Twelf.  Please

send requests to elf-list-request@cs.cmu.edu.


  Carsten Schrmann
  carsten@cs.cmu.edu

Prev: Professorship in Programming Theory, University of Bergen
Next: Communication errors in the polyadic pi-calculus are undecidable
Index(es):
- Main
- Thread