| Time | Title | Author(s) |
|---|---|---|
[Invited Talk] |
Mechanized Mathematics | Jacques Carette |
| 09:35--10:05 | CTP-based program languages? Considerations about an experimental design | Florian Haftmann, Cezary Kaliszyk, and Walther Neuper |
| 10:05--10:30 | Isabelle/ML vs. Isabelle/Scala | Makarius Wenzel |
| 10:30-11:00 | COFFEE BREAK | |
[Invited Talk] |
Beluga: programming with contextual data, contexts, and ... | Brigitte Pientka |
[Invited Talk] |
The Abella Theorem Prover and Two-level Logic Reasoning | Andrew Gacek |
| 12:30--14:00 | LUNCH | |
[Invited Talk] |
Can we make Mathematics universal as well as fully reliable? | Pierre Cartier |
| 15:05--15:35 | transalpyne: a language for automatic transposition |
Luca De Feo and Eric Schost |
| 15:35--16:05 | LEMA: Towards a language for reliable arithmetic | Vincent Lefèvre, Philippe Théveny, Florent de Dinechin, Claude-Pierre Jeannerod, Christophe Mouilleron, David Pfannholzer, Nathalie Revol |
| 16:05--16:30 | The PIDE-Project : Towards multiple-sided, asynchronous Formal Documents in the Isabelle/ISAR Framework | Burkhart Wolff |
| 14:30--17:00 | COFFEE BREAK | |
| 17:00--17:30 | Recent Developments in Omega's Proof Search Programming Language | Serge Autexier and Dominik Dietrich |