Formal proofs development and decision procedures

Theorem provers like Coq enjoy a mechanism that incorporates computations within deductions. This allows replacing the proof of a proposition by the proof of an equivalent proposition obtained from the former thanks to possibly complex computations. Adding more power to this mechanism leads to a calculus which is more expressive (more terms are typable), which provides more automation (more deduction steps are hidden in computations) and eases the use of dependent data types in programs or proofs development.

I will introduce CoqMT, an extension and implementation of the core logic of the Coq proof assistant which allows the embedding of decision procedures in its conversion mechanism. The impact of CoqMT is two-folded. On the theoretical side, it provides a general and unified view for introducing computations within its deduction machinery. On the practical side, it gives a generic architecture for introducing complex code in the core of the Coq proof assistant while keeping its surety.

Because the introduced decision procedures may require a quite complex code which cannot be assumed to be free of bugs, the architecture of the kernel of Coq has been modified such that it can accept and verify certificates. This approach yield a readable, modular, incremental kernel, made of the Coq kernel together with the certificate checkers.