I would like to announce the availability of a world-wide web home page on logical frameworks .
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
Department of Computer Science, Carnegie Mellon University
Pittsburgh, PA 15213-3891, U.S.A.
Telephone: +1 412 268-6343, FAX: +1 412 268-5576, InterNet: fp@cs.cmu.edu