Verifying simple imperative programs with the Coq proof assistant

Andres Toom

Institute of Cybernetics

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.

Tarmo Uustalu
Last update 12 May 2010