From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub

We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, whi…