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 super-prover that enables the centralized development of proof libraries for other proof assistants, such as Coq and PVS. It implements first-order 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.