| 8:55 - 9:00 | Opening | ||
|
9:00 - 10:00 invited talk |
Decorating proofs | Helmut Schwichtenberg |  |
|
10:00 - 10:30 full paper |
Light Dialectica Revisited | Dan Hernest and Trifon Trifonov | |
| 10:30 - 11:00 | Coffee Break | ||
|
11:00 - 11:30 full paper |
Herbrand Sequent Extraction | Stefan Hetzl, Alexander Leitsch, Daniel Weller and Bruno Woltzenlogel Paleo | |
|
11:30 - 12:00 full paper |
Herbrand expansion proofs and proof identity | Richard McKinley | |
|
12:00 - 12:30 full paper |
From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus | Steffen van Bakel, Luca Cardelli and Maria Grazia Vigliotti | |
| 12:30 - 14:00 | Lunch Break | ||
|
14:00 - 15:00 invited talk |
Inhabiting Negative Types | Stéphane Lengrand | |
|
15:00 - 15:30 full paper |
Inhabitance of Existential Types is Decidable in Negation-Product Fragment | Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa and Hiroshi Nakano | |
| 15:30 - 16:00 | Coffee Break | ||
|
16:00 - 16:15 |
Comparing various approaches to lambda-calculi for classical logic | Silvia Vecchiato | |
|
16:15 - 16:35 short paper |
An Application of the Refined A-Translation for a Variant of the Infinite PHP | Diana Ratiu | |
|
16:35 - 16:55 short paper |
Classical Logic of Bunched Implications | James Brotherston and Cristiano Calcagno | |
|
16:55 - 17:15 short paper |
Proof Forests with Cut-Elimination Based on Herbrand's Theorem | Willem Heijltjes | |
|
17:15 - 17:35 short paper |
Ingredients of a Deep Inference Theorem Prover | Ozan Kahramanogullari | |
|
17:35 - 17:55 short paper |
A Curry-Howard Correspondence for a Canonical Classical Natural Deduction | Alexander Summers | |
| 17:55 | Announcements and Goodbye | ||