Orsay (France), June 12-13 2006

On one hand, people working designing efficient numerical libraries are more and more interested by proving their correctness. On the other hand, theorem proving people want to use non-trivial numerical computations inside formal proofs.

Indeed, recent examples show that the naive representations of numbers in proof systems are not sufficient anymore:

- New developments like work on Hales' proof of the Kepler conjecture or primality tests show that computations over numbers are a crucial part of the proof.
- New proof tactics like Gröbner bases or Cylindrical Algebraic Decomposition or interval arithmetic show that computation over numbers are crucial to define semi-decision procedures.

We believe that this area is meant to grow in the near future and opens new perspectives to formal mathematics. This workshop 's goal is to encourage the cross-fertilization between theorem proving and computer arithmetic. In particular to promote the design of proof-systems with reasonably efficient computational abilities using certified routines.

More generally, this workshop should be an occasion for the communities of theorem proving and computer arithmetic to meet.

The workshop will be held on June 12-13 in France (Orsay
/ Plateau de
Saclay).

For people that want to give a talk or simply participate, please send
an email to one of the organisers before May 25:

Benjamin Werner
: Pocklington
in Coq

Laurent Fousse : The Elliptic Curve Factorization method

Sylvie Boldo Veltkamp & Dekker revisited

Yves Bertot: Reals as Streams

Laurent Fousse : The Elliptic Curve Factorization method

Sylvie Boldo Veltkamp & Dekker revisited

Yves Bertot: Reals as Streams

Andrea Asperti
: Fermat's Little Theorem in Matita

Russell o'Connor : A Monadic Approach to Certified Exact Real Arithmetic

Roland Zumkeller : Taylor Models in Coq

Diana Ratiu: On Extraction of an Algorithm from a Classical Proof of Dickson's Lemma

Russell o'Connor : A Monadic Approach to Certified Exact Real Arithmetic

Roland Zumkeller : Taylor Models in Coq

Diana Ratiu: On Extraction of an Algorithm from a Classical Proof of Dickson's Lemma

Guillaume Melquiond
: Gappa
certificates of numerical
correctness

Pierre Letouzey : QArith: efficient rational numbers for Coq

Benjamin Grégoire : More Efficient Integers in Coq

Arnaud Spiwack : Towards Machine Integers in Coq

Laurent Théry : Gröbner basis revisited

Pierre Letouzey : QArith: efficient rational numbers for Coq

Benjamin Grégoire : More Efficient Integers in Coq

Arnaud Spiwack : Towards Machine Integers in Coq

Laurent Théry : Gröbner basis revisited

To reach INRIA-Futurs by public transportation:

From Paris, take
underground RER B, direction
to Saint-Rémy
les Chevreuses, stop at Le Guichet
.

Exit the station crossing the railway, on the parking over the coffee place, take bus number 269-002, direction to IUT Orsay and Plateau

Stop at Parc Club (2-minute ride), reaching INRIA-Futurs is a 5-minute walk.

Exit the station crossing the railway, on the parking over the coffee place, take bus number 269-002, direction to IUT Orsay and Plateau

Stop at Parc Club (2-minute ride), reaching INRIA-Futurs is a 5-minute walk.

The use of numbers in formal developments will be one of the themes of this new lab.

2 rue Francois Leroux 91400 Orsay

+ 33 1 64 86 17 47

fax 01 64 86 17 48

+ 33 1 64 86 17 47

fax 01 64 86 17 48

- Sylvie Boldo Veltkamp & Dekker revisited
- Those two floating-point algorithms have been known for decades and are now formally proved. In a will of the most generic property (any radix, Underflow...), we have noticed that the pen and paper proofs from the literature cannot always be applied. More, the proof path is interesting as these cases are hardly looked into and new methods and results had to be developed.
- Guillaume Melquiond : Gappa certificates of numerical correctness
- Statically analyzing numerical applications by hand to ensure they will compute the expected results is tedious and error-prone. Automatized tools are needed to help developers certify their implementations. Gappa is such a tool: it is designed to verify arithmetic properties that usually appear when certifying numerical applications like CRlibm or CGAL. It relies on interval arithmetic, forward error analysis, term rewriting to bound mathematical expressions involving floating-point or fixed-point operators. Finding these bounds is computationally intensive and the tool acts as an oracle. Yet it also generates a proof script of these bounds, so that they can be automatically verified by an independent proof-checker like Coq and included in bigger proofs. This script relies on theorem from Gappa support library to prove the bounds; checking they are correctly applied involves numerical computations on dyadic numbers.
- Diana Ratiu : On Extraction of an Algorithm from a Classical Proof of Dickson's Lemma
- Although the computational content of classical proofs is not explicit, and one cannot extract algorithms from them directly - as it is the case with constructive proofs -, there are techniques at hand for uncovering this information. One such transformation of classical proofs is the Friedman-Dragalin Translation, also known as A-Translation. A refinement of the A-Translation, existing as an underlying mechanism in Minlog, has enabled the extraction of a program for the case of k=2 for a classical proof of Dickson's Lemma. In this talk we present this (old) result, together with a (new) further step: a formalisation in Minlog of the classical proof for the general case. Some comments will be also made as to what differs with respect to the particular case of n=2 and thus to what refined A-translation is missing in oder to enable extraction of an algorithm from this generalised proof.