Thursday, 6 May 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf], Coq scripts [code]
Abstract: Coq is an interactive theorem prover developed at INRIA in France. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. It is based on the theory of the calculus of inductive constructions.
The Coq theory is closely related to the Curry-Howard isomorphism (aka proofs-as-programs) and it is often used to formally verify the correctness of computer programs. Coq can also be used to extract a certified program from the proof of its formal specification.
I plan to use Coq in the future for a similar task. However, this talk will be about Coq in general. It will be in an introductory style explaining the basics of Coq and demonstrating how to use it to rigorously reason about simple imperative programs using the big-step operational semantics. The talk will be followed in the future by other talks demonstrating reasoning about more complex properties, different semantic approaches and finally, the formalisation of a specific pragmatic approach to specify and prove the correctness of program transformations.