Current Workshop | Overview | Back | Home | Search | | ||||||||||
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
( Henri
Lombardi (France Comté, France) Peter Paule ( Bas Spitters
( Tutorials Per Martin-Löf ( Invited
lectures: Organizing Committee Co-sponsored
by the EU 6th Framework Program, Marie Curie SCF. [Back] |