Proof editor succeeding ALF, an editor for direct manipulation of proof objects in a logical framework based on Per Martin-LC6f's Type Theory. Free download available.

Article from the Stanford Encyclopedia of Philosophy.

Formal proof management system, based on a logical framework called Calculus of Inductive Constructions extended by a modular development system for theories. With links to download, documentation and related tools.

Provides a working environment for the Coq theorem prover. Developed at INRIA Sophia Antipolis.

Provides an analysis of the effect of the identity combinators in dual systems. Written by Katalin Bimbó.

Automated proof system for higher order logic. Operates as an open source project with a BSD-style license allowing free use in commercial products.

Generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).

Web-based proof assistant for first order-hidden logic, using OBJ3 as a reduction engine. Also generates proof documentation for the web and supports distributed cooperative proving.

Guide to lazy and strict versions of the lambda-calculus interpreter.

Interactive proof development system designed and implemented by Randy Pollack in Edinburgh.

Generic interface for proof assistants, based on the customizable text editor Emacs. Works with either XEmacs or GNU Emacs.

Proof-assistant for Pure Type Systems (PTSs) with several extensions. With user guide, installation guide, tutorials and articles about Yarrow.