| 11:00 | Opening Session |
| 11:15 | C. Benzmuller. The Calculemus Research Training Network. A short overview. |
| 11:45 | Ferruccio Guidi, C. Sacerdoti Coen. Querying Distributed Digital Libraries of Mathematics |
| 12:30 | Lunch |
| 14:00 | Manuel Maarek, Virgile Prevosto. The Documentation System of FoC |
| 14:45 | Claudio Sacerdoti Coen, Stefano Zacchiroli. Brokers and Web-Services for Automatic Deduction: a Case Study |
| 15:30 | Coffee |
| 16:00 | Jacques Carette, William Farmer, Jeremie Wajs. Trustable Communication Between Mathematics Systems |
| 16:40 | Edmund Clarke, Michael Kohlhase, Joel Ouaknine, Klaus Sutner. System Description: Analytica 2 |
| 17:00 | Andrew Adams, A New Interface to PVS |
| 17:20 | Martin Pollet, Volker Sorge. Integrating Computational Properties at the Term Level |
| 17:40 | CALCULEMUS network meeting |
| 9:00 | Invited talk: Thierry Coquand
(Chalmers University of Technology, Gteborg, Sweden) (joint speaker with TABLEAUX 2003) Dynamical Method in Algebra: a Survey |
| 10:00 | Jesus Aransay, Clemens Ballarin, Julio Rubio. Towards a higher reasoning level in formalized Homological Algebra |
| 10:30 | Coffee |
| 11:00 | Virgile Prevosto, Mathieu Jaume. Making proofs in a hierarchy of mathematical structures |
| 11:45 | Sylvie Boldo, Marc Daumas, Laurent Théry. Mixing formal proofs and computer algebra about finite precision arithmetic |
| 12:30 | Lunch |
| 14:00 |
OUT-OF-TOWN EXCURSION AND SOCIAL DINNER |
| 9:00 | Invited talk: James Davenport. University of Bath. Definite/indefinite integration |
| 10:00 | Ulrich Berger, Monika Seisenberger. Inductive definitions versus classical dependent choice in the Minlog system |
| 10:30 | Coffee |
| 11:00 | Silvio Ranise. Building Convex Hulls by Combining SAT Solving and Algebric Computing |
| 11:20 | Hidetsune Kobayashi, Hideo Suzuki, Hirokazu Murao. Rings and Modules in Isabelle/HOL |
| 11:40 | Wolfgang Windsteiger. Exploring an Algorithm for Polynomial Interpretation in the Theorema System |
| 12:30 | Lunch |
| 14:00 |
PANEL DISCUSSION ON OPEN CHALLENGES OF COMPUTERIZED MATHEMATICS
Panel Introduction: Jacques Calmet. Are there true Grand
Mathematical Challenges in Mechanized Mathematics?Joint with TABLEAUX and TPHOLs 2003 |