TYPES Workshop on Numbers and Proofs
Orsay (France), June 12-13 2006
Scope
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:
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.
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:
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.
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.
