TYPES Workshop on Numbers and Proofs
Orsay (France), June 12-13 2006


There is a growing trend of bringing together formal proofs and efficient numerical computations.
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: In both cases, checking the resulting proof requires efficient computations over integers, rationals or real numbers ...
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:

Benjam in.Werner@inria.fr
Benjamin.Gregoire@sophia.inri a.fr


Monday June 12th at 14.15 (meeting room, building H) :

Benjamin Werner : Pocklington in Coq
Laurent Fousse : The Elliptic Curve Factorization method
Sylvie Boldo Veltkamp & Dekker revisited
Yves Bertot: Reals as Streams

Tuesday June 13th at 9.30 (meeting room, building H):

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

Tuesday June 13th at 13.00 (meeting room of building H):

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

Location and Dates

The workshop will be held in the meeting room of building H, INRIA-Futurs on June 12-13 in France (Orsay / Plateau de Saclay).
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.


This workshop is supported by the TYPES project and by the new joint laboratory of INRIA and Microsoft Research.
The use of numbers in formal developments will be one of the themes of this new lab.


An hotel near the workshop place is hotel d'Orsay:
2 rue Francois Leroux 91400 Orsay
+ 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.