Dagstuhl Seminar 05021
Mathematics, Algorithms, Proofs
( Jan 09 – Jan 14, 2005 )
- Thierry Coquand (Chalmers - Göteborg, SE)
- Henri Lombardi (University of Franche-Comté - Besancon, FR)
- Marie-Françoise Roy (University of Rennes, FR)
This seminar is the continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 january 2003.
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).
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 mathematics techniques contains 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 basics.
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 is lead to fill many objectives of computational analysis.
Providing formal proofs of correctness to the computer algebra community is very useful, specially 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 needs also powerful automatic methods from computer algebra.
We observe that the Dagstuhl seminar 03021, which seems to have been the first meeting devoted to the topic, was a success and has been very satisfactory for the participants. They decided to create a group under the acronym "Mathematics, Algorithms, Proofs". We have organised a similar meeting in Luminy, january 2004, and besides the next Dagstuhl meeting, we are trying to organize a MAP summer school in September 2005 in Santander (Spain).
Since the whole field is rather big, we think that it may be indeed a good idea to choose a focal topic. A good such topic for the next 2005 topic appears to be.
This seminar was the third MAP meeting, a continuation of the seminar "Verification and constructive algebra" held in Dagstuhl from 6 to 10 January 2003. The goal of these meetings is to bring together people from the communities of formal proofs, constructive mathematics and computer algebra (in a wide meaning). The special emphasis of the present meeting was on the constructive mathematics and efficient proofs in computer algebra. We were honored to have as invited speakers Helmut Schwichtenberg, proof theorist who is now working on extraction of programs from proofs, Harold Edwards, specialist of the work of Kronecker, and Fred Richman, the specialist of constructive algebra. A sub-theme was on formalization of mathematics, especially on the flyspec project, lead by Thomas C. Hales, and we were fortunate that most people working on this, in particular, besides Hales himself, Jeremy Avigad and Robert M. Solovay were present at the seminar.
Once again, we would like to thank the team of Schloss Dagsthul. The exceptional working condition we enjoyed there played an important part in the success of this meeting.
- Jeremy Avigad (Carnegie Mellon University, US) [dblp]
- Ulrich Berger (Swansea University, GB) [dblp]
- Jesper Carlström (University of Stockholm, SE)
- Thierry Coquand (Chalmers - Göteborg, SE) [dblp]
- Gema Maria Diaz-Toca (University of Murcia, ES)
- César Domínguez (Universidad de la Rioja, ES)
- Dominique Duval (Université de Grenoble, FR)
- Harold M. Edwards (New York University, US)
- M'hammed El Kahoui (MPI für Informatik - Saarbrücken, DE) [dblp]
- Philipp Gerhardy (TU Darmstadt, DE)
- Thomas C. Hales (University of Pittsburgh, US) [dblp]
- Daisuke Ikegami (Research Center for Verification & Semantics, JP) [dblp]
- Henri Lesourd (Universität des Saarlandes, DE)
- Pierre Letouzey (LMU München, DE)
- Laurentiu Leustean (TU Darmstadt, DE)
- Henri Lombardi (University of Franche-Comté - Besancon, FR) [dblp]
- Assia Mahboubi (INRIA Sophia Antipolis - Méditerranée, FR) [dblp]
- Tobias Nipkow (TU München, DE) [dblp]
- Steven Obua (TU München, DE)
- Paulo Oliva (Queen Mary University of London, GB) [dblp]
- Erik Palmgren (Uppsala University, SE) [dblp]
- Peter Paule (Universität Linz, AT)
- Hervé Perdry (University of Pisa, IT)
- Richard Pollack (New York University, US) [dblp]
- Loic Pottier (INRIA Sophia Antipolis - Méditerranée, FR)
- Virgile Prevosto (MPI für Informatik - Saarbrücken, DE)
- Alban Quadrat (INRIA Sophia Antipolis - Méditerranée, FR)
- Jean-Claude Raoult (University of Rennes, FR)
- Fred Richman (Florida Atlantic University - Boca Raton, US)
- Renaud Rioboo (UPMC - Paris, FR)
- Giuseppe Rosolini (University of Genova, IT) [dblp]
- Marie-Françoise Roy (University of Rennes, FR) [dblp]
- Julio Rubio Garcia (Universidad de la Rioja, ES) [dblp]
- Carsten Schneider (Universität Linz, AT)
- Peter M. Schuster (LMU München, DE) [dblp]
- Helmut Schwichtenberg (LMU München, DE) [dblp]
- Francis Sergeraert (Université de Grenoble, FR)
- Robert M. Solovay (Eugene, US)
- Bas Spitters (Radboud University Nijmegen, NL) [dblp]
- Joris van der Hoeven (University Paris Sud, FR) [dblp]
- Volker Weispfenning (Universität Passau, DE)
- Freek Wiedijk (Radboud University Nijmegen, NL) [dblp]
- Ihsen Yengui (Faculté des Sciences - Sfax, TN) [dblp]
- Julia Zappe (LMU München, DE)
- Roland Zumkeller (Ecole Polytechnique - Palaiseau, FR)