
Fri, 9 Oct 2009

Thu, 1 Jan 2009

Fri, 6 Feb 2009
Software
Coq
Coq is a interactive proof assistant, based on a dependent type theory with inductive types (the Calculus of Inductive Constructions, or CIC). It is developed by several research teams, mainly π r², ProVal, Marelle, CPR and TypiCal. Several members of TypiCal are deeply involved in the evolution of Coq through the development of extensions for the core system and the implementation of efficient tactics and libraries. Some members of TypiCal are also part of the Mathematical Components project which develops Ssreflect, a powerful extension for Coq.
Dedukti
Dedukti is a universal proof checker, based on the λΠcalculus modulo formalism. It is mainly developed within TypiCal by Mathieu Boespflug. It aims at verifying the proofs generated by various proof assistants (like Coq or Isabelle) by translating proofs into a universal framework mixing λΠcalculus and rewrite rules.
Fellowship
Fellowship is a superprover that enables the centralized development of proof libraries for other proof assistants, such as Coq and PVS. It implements firstorder sequent calculus annotated by λμμ'proof terms, a monadic proof language, and a flurry of other innovative concepts. Fellowship is a joint effort by Florent Kirchner and Claudio Sacerdoti Coen.