Home Page on Logical Frameworks

Dear Colleagues,

  I would like to announce the availability of a world-wide web home page on
logical frameworks at


This includes a (BibTeX) bibliography, pointers to implementations, addresses
of researchers in the area, and a "what's new" page.  Many papers are
available via anonymous ftp; hypertext links to them are provided so they can
be conviently previewed or retrieved by the click of a button.

Corrections, additions and other comments and suggestions are most welcome.

Important Disclaimer: In order to keep the task of compiling this material
manageable I excluded general-purpose theorem proving systems designed for the
formalization of classical or constructive mathematics, such as NQTHM, NuPrl,
Coq, LEGO, and others.  However, I included individual experiments carried out
in these systems that are meta-logical in nature.  I would like to provide
cross references to home pages for such related systems and type theories
where available.

  - Frank Pfenning
Frank Pfenning                      Telephone: +1 412 268-6343       
Department of Computer Science            FAX: +1 412 268-5576       
Carnegie Mellon University           InterNet: fp@cs.cmu.edu         
Pittsburgh, PA 15213-3891, U.S.A.    
URL: http://www.cs.cmu.edu:8001/afs/cs/user/fp/www/homepage.html