Events

Archives

Share:
A A

22 July 2010

Pierre-Yves Strub gives a seminar on CoqMT - Coq Modulo Theory

Bât. 1. 1er étage
Microsoft Research - Inria Joint Centre
Parc Orsay Université

CoqMT - Coq Modulo Theory
Pierre-Yves Strub
Tsinghua University

The Calculus of Congruent Constructions is a Calculus of Constructions which allows the embedding of decision procedures in its computational part. In this talk I will present CoqMT, a variation of the Calculus of Congruent Constructions, along with a presentation of the proof in Coq of its main metatheoritical properties. I will also explain how such a calculus can be implemented in a safe way either by:

  • the development of a certified decision procedure, or
  • the development of decisions procedures producing certificates along with a dual-stack type-checker.