Talk by Prof. Castéran Pierre on Coq: "The hydra game: a formal development with the Coq proof assistant"
June 26 (Tue.)
National Institute of Informatics
Room 1208-1210, 12th floor
The Hydra game was introduced in 1982 by the mathematicians L. Kirby and J. Paris in their article: "Accessible Independence Results for Peano Arithmetic".
This article contains two theorems: (1) Whichever the strategy of Hercules and the Hydra, any battle eventually terminates with Hercules' victory; and (2) The previous result cannot be proved in Peano Arithmetic. We present a formal, self-contained (axiom-free) proof of a variant of both theorems, with the help of the Coq proof assistant.
Since Coq's logic is higher-order intuitionnistic logic, the reference to Peano Arithmetic is replaced with a study of a class of proofs of termination indexed by ordinal numbers less or equal than 0.
We present the main parts of this proof, as well as the main features of Coq that made possible its construction.
Castéran Pierre, a professor at the University of Bordeaux, is interested in type theory, interactive theorem proving, and programming language semantics. Pierre Castéran has been participating in several research projects where a formal semantics is a starting point for proving program correctness or establishing the impossibility of realizing a given specification in a too weak model of computation.
He is co-author of the book on Coq : "Interactive Theorem Proving and Program Development" with Yves Bertot (2000 citations according to Google Scholar ) and scientific co-organizer of 7 international summer schools on Coq, 2 in Paris, 4 in China, and 1 in Japan (Shonan Village Center, Kanagawa). He also co-authored two tutorials on advanced features of Coq: inductive and co-inductive types, type classes and generalized rewriting. He is now working on a project for showing advanced features of the Coq proof assistant, through a set of appropriate medium or large scale formal developments.
Zhenjiang Hu < hu [at] nii.ac.jp >