Formal proofs development and decision procedures


April 9, 2012


Pierre-Yves Strub


Microsoft - INRIA Joint Center


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.


Pierre-Yves Strub

Pierre-Yves Strub obtained his Ph.D. grade, in 2008, from the Computer Science laboratory at École Polytechnique, France. During his Ph.D., he focused on adding more automation to interactive theorem provers. In 2008, he moved for a 2 year postdoctoral stay at Tsinghua University, Beijing, China where he worked on the application of formal methods to the verification of System on Chip simulators. Since 2010, he is a member of the Microsoft – INRIA Joint Center where he works on formal methods applied to the verification of distributed programs.