[TYPES/announce] Announcement and CFP : Workshop Proofs & Numbers, June in Orsay, France

[Stephanie Weirich]

     Dear Colleagues,

We plan a workshop on the upcoming research field of interactions
between numerical computations and formal proofs. The workshop will
take place over 1 and 1/2 days, on June 12th and 13th in Orsay; it will
follow a more general seminar the 12th in the morning.

We encourage you to participate and to present work on the topic. The
aim is to bring together from different fields; please feel free to
forward this announcement to other possibly interested colleagues.

More information is given below and can also be found on :

http://www-sop.inria.fr/marelle/Laurent.Thery/microsoft/Workshop%20on%20numbers%20and%20proofs.html

Given the short delay, the program will be established as propositions
come in and the web-site will grow progressively.  We already plan
talks about formal primality proofs, representation of numbers in type
theory, formal real optimization, representation of arbitrary
precision real numbers in Coq...

The workshop will be supported by the EU TYPES project and the new
joint laboratory of INRIA and Microsoft Research. Members of TYPES can
therefore use their TYPES money to fund their trip.

Hoping to see many of you in Orsay,


Benjamin Grégoire,
Laurent Théry,
Benjamin Werner

------------------------------------------

                          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, rational 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.


Location and Dates
*************************
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 organizers before May 25:

Benjamin.Werner at inria.fr
Laurent.Thery at sophia.inria.fr
Benjamin.Gregoire at sophia.inria.fr

---------------------