|
Seminar by Jean-Pierre Jouannaud
INRIA and Tsinghua Software Chair, Beijing
French Director of LIAMA
Topic : Engineering Proofs: Use and Challenges of Coq, a Curry-Howard based Proof Assistant
Date：2010-12-21 9:30-10:35
Proof assistants which have been invented to develop programs which are "correct by definition". They are also used to develop mathematics which is "correct by definition", therefore moving from "proofs beyond doubt" to "proofs without doubt". In practice, they are now used to prove that programs outputs are correct without doubt.
I shall first explain what is a proof assistant based on the Curry-Howard isomorphism, then introduce Coq, one of the most popular proof assistants on the market, and then explain how it can be used to prove programs correct or results of programs correct.
In conclusion, I will first single out the recent achievements in the design of PAs and proofs that make possible their use in modern mathematics and computer science, and present a roadmap aiming at making PA fullfill their promisses. |
