Abella is an interactive theorem prover developed by Andrew Gacek while a PhD student at the University of Minnesota and a postdoc within the Parsifal project. This system include declarative support for λ-tree syntax (an approach to syntax with bindings), the two-level approach to reasoning about logic specifications, the ∇-quantification, and nominal abstractions. Many examples in the meta-theory of the lambda-calculus and π-calculus have been developed.


Tac is an interactive and automatic theorem prover for an intuitionistic logic extended with fixed points and generic (∇) quantification. Tac is based on recent research work by David Baelde and others. It has been implemented by David Baelde and Alexandre Viel (INRIA & LIX/Ecole Polytechnique) and Zach Snow (University of Minnesota - Minneapolis). See the Tac page in the Slimmer GForge project.


Bedwyr is a model checker that allows for reasoning directly on syntactic expressions (even those contining bindings). The earlier Level 0/1 prover was rewritten into OCaml by David Baelde and Axelle Zeigler and then greatly extended by David Baelde and Andrew Gacek during the summer of 2006. The system is being developed on the INRIA Gforge open source platform. See the Bedwyr page in the Slimmer GForge project.

Level 0/1

Alwen Tiu has a prototype implementation of a logic system that can reason on “levels 0 and 1”. The system integrates finite success and finite failure as proof search for a single logic.


Teyjus is an implementation of λProlog by Gopalan Nadathur. While Teyjus has no formal connections with the Parsifal project, it is a commonly used prototyping tool for this team.

software.txt · Last modified: 10/05/2010 12:47 by admin
Trace: software
CC Attribution-Noncommercial-Share Alike 3.0 Unported Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0