FISP Workshop (3rd FISP Meeting), TU Wien December 7-8 2018
The Fine Structure of Formal Proof Systems and their Computational Interpretations Workshop (3rd FISP Meeting) brings together the project particpants from Austria and France to discuss recent work and work in progress. Moreover colleagues have been invited to present their work.
Project Overview
The FISP project is part of a long-term, ambitious project whose objective is to apply the powerful and promising techniques from structural proof theory to central problems in computer science for which they have not been used before, especially the understanding of the computational content of proofs, the extraction of programs from proofs and the logical control of refined computational operations. So far, the work done in the area of computational interpretations of logical systems is mainly based on the seminal work of Gentzen, who in the mid-thirties introduced the sequent calculus and natural deduction, along with the cut-elimination procedure. But that approach reveals its limits when it comes to computational interpretations of classical logic or the modelling of parallel computing. The aim of our project, based on the complementary skills of the teams, is to overcome these limits. For instance, deep inference provides new properties, namely full symmetry and atomicity, which were not available until recently and opened new possibilities at the computing level, in the era of parallel and distributed computing.
Programme
| Friday 7 December 2018 |
| 9:00 - 10:00 |
Alexander Leitsch - Proof Schemata and Herbrand Systems |
| 10:00 - 10:30 |
break |
| 10:30 - 11:00 |
Francesco Genco - Intermediate Logic Proofs as Concurrent Programs |
| 11:00 - 11:30 |
Thierry Joly - Distilling sequent calculus yields Curry's combinatory factorization |
| 11:30 - 12:00 |
Lutz Straßburger - Proof Nets for First-Order Additive Linear Logic |
| 12:00 - 14:00 |
break |
| 14:00 - 14:30 |
Hugo Herbelin - tba |
| 14:30 - 15:00 |
Andrea Aler-Tubella - What we learn from decomposition |
| 15:00 - 15:30 |
Matteo Acclavio - Combinatorial Proofs for Modal Logic K |
| 15:30 - 16:00 |
break |
| 16:00 - 16:30 |
Kees van Berkel - Cut-free Calculi and Relational Semantics for temporal STIT logics |
| 16:30 - 17:00 |
Jan Bydzovsky - Unprovability of circuit upper bounds in the Cook's theory PV |
| 17:00 - 17:30 |
Delia Kesner - Refined Quantitative Type Systems |
17:30 - 18:00 |
Sonia Marin - Justification logic for constructive modal logics |
|
| Saturday 8 December 2018 |
| 9:00 - 10:00 |
George Metcalfe - Uniform Interpolation and Coherence |
| 10:00 - 10:30 |
break |
| 10:30 - 11:00 |
Roman Kuznets - Nesting multi-conclusions: the Maehara conundrum |
| 11:00 - 11:30 |
Chris Fermüller - A cost conscious game model for intutionistic linear logic with subexponentials |
| 11:30 - 12:00 |
Revantha Ramanayake - Sequent calculi for substructural logics via bounded proofs |
| 12:00 - 14:00 |
break |
| 14:00 - 14:30 |
Stefan Hetzl - A simplified proof of the epsilon-theorems |
| 14:30 - 15:00 |
Kenji Miyamoto - The epsilon calculus with equality and Herbrand complexity |
| 15:00 - 15:30 |
Gabriel Ebner - Herbrand constructivization for automated intuitionistic theorem proving |
| 15:30 - 16:00 |
break |
| 16:00 - 16:30 |
Juan P. Aguilera - Systems of determinacy in third-order arithmetic |
| 16:30 - 17:00 |
Jannik Vierling - Clause Set Cycles and Induction |
| 17:00 - 17:30 |
David Cerna - A Structural Semantics for Recursive Proof Calculi |
| 17:30 - 18:00 |
Dino Rossegger - The complexity of scattered linear orderings |
Venue
Friday 7 December 2018: "Konferenzraum" (room number DA09 E10) 9th floor green area, Freihaus, TU Wien, Wiedner Hauptstrasse 8-10, 1040 Wien (take the elevator in the green area to the 8th floor and follow the signs to the staircase to get to the 9th floor)
Saturday 8 December 2018: "Seminarraum" (room number DA05E10) 5th floor green area, Freihaus, TU Wien, Wiedner Hauptstrasse 8-10, 1040 Wien
Contact information: Matthias Baaz +43 699 11215168