## 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