Mathematics: Algorithms and Proofs

The goal of the seminar is to bring together people from the communities of formal proofs, constructive mathematics and computer algebra (in a wide meaning). This is a continuation of previous meetings in Schloss Dagstuhl (2003 and 2005), Luminy (2004) and Castro Urdiales (2006). The previous meetings have been quite successful in bringing these communities closer together. A small MAP (`Mathematics: Algorithms and Proofs') community seems to be taking shape. In the present meeting we have succeeded in inviting key figures from the three communities which were previously outside the MAP community. It promises to be an interesting workshop!

One objective of the seminar is to bridge the gap between conceptual (abstract) and computational (constructive) mathematics, by providing a computational understanding of abstract mathematics. It is becoming clear that many parts of abstract mathematics can be made constructive and even computational and that abstract mathematical techniques contain an underlying constructive content. We are not only interested in algorithms however, but also in formal proofs of the correctness of these algorithms.

Computer algebra provides a variety of interesting basic algorithms, from exact linear algebra to various aspects of elimination and real root counting, which are the foundations for much more sophisticated results like nullstellensatz, quantifier elimination etc... It is remarkable that in constructive and computer algebra, progress in sophisticated algorithms often implies progress on these basic algorithms.

Moreover, the scope of computer algebra is now widened by the consideration of seminumerical algorithms. When such algorithms are correctly controlled, they actually deal with real and complex numbers in the constructive meaning of these objects. So computer algebra fills many objectives of computational analysis.

Providing formal proofs of correctness to the computer algebra community is very useful, especially for algorithms which are basic and used everywhere. On the other hand, a collection of mathematically non trivial examples is very useful for the formal proof community, which also needs powerful automatic methods from computer algebra.

For more information about the MAP-community we refer to

http://www.disi.unige.it/map  where one can also find the MAP manifesto.

Scientific Committee

Thierry Coquand (Chalmers, Sweden)

Henri Lombardi (France Comté, France)

Peter Paule (University of Linz, Austria)

Bas Spitters (Nijmegen, the Netherlands)

Tutorials

Arjeh Cohen

Thierry Coquand

Per Martin-Löf (Stockholm)

Invited lectures:

Michael Beeson

Dirk van Dalen

Hendrik Lenstra

Dana Scott

Organizing Committee

Herman Geuvers

Bas Spitters

Freek Wiedijk

Co-sponsored by the EU 6th Framework Program, Marie Curie SCF.