Colloquium in Honor of Thérèse Hardin

Paris, France    9th July 2010


Friday, July 9th 2010

Session 1 (9:45-10:30)

9:45-10:30 The Genesis of Lucid Synchrone and ReactiveML in the SPI Team
Marc Pouzet

Coffee Break (10:30-11:00)

Session 2 (11:00-12:30)

11:00-11:45 Lessons from Therese's Work
Fairouz Kamareddine
11:45-12:30 From Bip to Focalize
Véronique Donzeau-Gouge and Catherine Dubois

Lunch (12:30-14:00)

MKM Invited Talk (14:00-15:00, Chair: Alan Sexton)

14:00-15:00 Against Rigor
Doron Zeilberger

Abstract:The ancient Greeks gave (western) civilization quite a few gifts, but we should beware of Greeks bearing gifts. The gifts of theatre and democracy were definitely good ones, and perhaps even the gift of philosophy, but the "gift" of the so-called "axiomatic method" and the notion of "rigorous" proof did much more harm than good. If we want to maximize Mathematical Knowledge, and its Management, we have to return to Euclid this dubious gift, and give-up our fanatical insistence on perfect rigor. Of course, we should not go to the other extreme, of demanding that everything should be non-rigorous. We should encourage diversity of proof-styles and rigor levels, and remember that nothing is absolutely sure in this world, and there does not exist an absolutely rigorous proof, nor absolute certainty, and "truth" has many shades and levels.

Session 3 (15:00-16:30)

15:00-15:15 Video Message
Jean-Charles Pomerol
15:15-16:00 Système d'exploitation certifiés
Emmanuel Gureghian
16:00-16:30 La déduction modulo: des preuves aux modèles
Gilles Dowek

Coffee Break (16:30-17:00)

Session 4 (17:00)

17:00 Closing Session
Thérèse Hardin