Researcher Yves Bertot visited Joint Center
September 3 to 5, 2009, Yves Bertot, a senior researcher of INRIA was invited to visit USTC-Yale joint research center of high confidence software. During that time, Yves Bertot gave us a brief talk about the proof assistant "Coq" and how to formally describe programming language semantics and do static analysis with it. Post-doc Yu Guo, Zhaopeng Li and Dr. Ming Fu reported about projects on Operating System Verification, Certifying Compiler, Concurrent Program Verification, respectively. Yves Bertot had an in-depth discussion about these projects with us.
Coq is a leading high-order theorem proof assistant. Most of our projects use Coq as an important tool to proof theorems and describe formal semantics. With Yves's visit, we get a deeper understanding of theorem prooving and formal semantics and also learn some state-of-the-art works in related area.
Yves Bertot is a senior researcher of Sophia Antipolis in INRIA. His main research interest is formal description of algorithms and mathematical theories with proof assistant - Coq. He has deep understanding of Coq, and written "Coq in a hurry", "Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions". These are must read for people to learn Coq. Yves Bertot is currently leading project "Marelle", this research targets techniques to verify software correctness with mathematical proofs and tools to precisely describe data, algorithms and their properties.