Program extraction using real arithmetic in Coq.

Sylvain Dailler

(Lyon, currently Internship Swansea)

At first, I will present the Coq proof assistant ( and give a small interactive tutorial about how to prove theorems and extract programs using Coq. Then, I will show how to create certified programs only relying on the axioms of real arithmetic. This can be done with easy specifications and without having to construct a huge set of functions and theorems. As an example, we used our framework to define: unary natural numbers, binary natural numbers, a redundant version of rational numbers and a coinductive characterisation of real numbers that have a signed digit representation.

Thursday 5th August 2010, 14:00
Robert Recorde Room
Department of Computer Science