Sciweavers

CORR
2008
Springer
122views Education» more  CORR 2008»
13 years 3 months ago
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
Abstract 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 Construct...
Frédéric Blanqui, Jean-Pierre Jouann...