| 9:00-9:30 | Welcome and Introductory Remarks |
| Session 1: | Invited Talk |
| 9:30-10:30 | Some Reflections on Proof Transformations |
| Peter Andrews | |
| 10:30-11:00 | Coffee Break |
| Session 2: | Proof Transformation and Complexities |
| 11:00-11:30 | Proofs as constraints for abstraction and refinement |
| Xiaochun Cheng, Matt Fairtlough, and Michael Mendler | |
| 11:30-12:00 | An analysis of Frege-Hilbert calculi |
| Elmar Eder | |
| 12:00-12:30 | Object languages in a type-theoretic meta-framework |
| Paul Callaghan, Zhaohui Luo, and Michael Mendler | |
| 12:30-14:00 | Lunch Break |
| Session 3: | Proof Presentation |
| 14:00-14:30 | Human-readable machine-verifiable proofs for teaching constructive logic |
| Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning | |
| 14:30-15:00 | Mathematics and proof presentation in Pcoq |
| Ahmed Amerkad, Yves Bertot, and Laurence Rideau | |
| 15:00-15:30 | Presenting proofs using logicographic symbols |
| Koji Nakagawa and Bruno Buchberger | |
| 15:30-16:00 | Coffee Break |
| Session 4: | Short Presentations and Group Discussions |
| 16:00-16:15 | A User-Extensible Natural Language Interface to the Proof Editor Alfa |
| Aarne Ranta | |
| 16:15-16:30 | A faithful embedding of lax logic into intuitionistic logic |
| Uwe Egly | |
| 16:30-16:45 | 11 years of `Formalized Mathematics'---proof checked journal automatically translated into English |
| Roman Matuszewski | |
| 16:45-17:00 | Aspects of human-oriented proof presentation |
| Helmut Horacek and Armin Fiedler | |
| 17:00-18:00 | Group Discussion |