| CARVIEW |
Proof Society 2024
6th International School and Workshop on Proof Theory 9-13 September. Birmingham, UK.
General Information
The 6th Proof Society International School and Workshop will be organised by the University of Birmingham. The event takes place under the auspices of The Proof Society, a society formed to support the notion of proof in its broadest sense. The Proof Society has organised an annual school and workshop since 2018 (except 2020 due to the COVID19 pandemic).
The aim of the School is to cover basic and advanced topics in proof theory and related subjects. The School will be aimed at Master's and PhD students interested in proof theory, as well as more senior researchers from related areas in computer science, mathematics and philosophy. The workshop is aimed at all researchers, from students to professors, working around proof theory and its applications. It will consist of a mixture of invited and contributed talks.
Scope
The School and Workshop aim to promote proof theory and its related areas in the broadest sense. Topics include but are not limited to:- Applied proof theory, e.g. proof mining
- Formalised proofs
- Structural proof theory
- Linear logic
- Computational interpretations of proofs
- Computability and proofs, e.g. Reverse Mathematics
- Ordinal analysis
- Philosophy of proof theory
- Proof systems and proof search
- Proof complexity
- Automated theorem proving
Invited Lecturers and Speakers
The School will consist of the following courses:- The Curry-Howard correspondence journey. (Abstract) (Slides: lecture 1, lecture 2, lecture 3)
Silvia Ghilezan (University of Novi Sad & Mathematical Institute SASA) - Proof Mining: Foundations and Applications. (Abstract) (Lecture slides)
Ulrich Kohlenbach (TU Darmstadt) - Cut elimination, analytic cut property and interpolation property. (Abstract) (Slides: lecture 1, lecture 2, lecture 3)
Hiroakira Ono (JAIST) - An introduction to reverse mathematics. (Abstract) (References: Subsystems of Second Order Arithmetic (Simpson), Slicing the Truth (Hirschfeldt), Reverse Mathematics (Dzhafarov and Mummert))
Paul Shafer (University of Leeds)
The School originally consisted of a fifth course too, Deep Inference by Alessio Guglielmi. Alessio tragically died in April this year, after a short and devastating illness that took everyone by surprise. His contributions to our community, as a researcher, colleague, mentor and friend, were immense. He is missed dearly by all those that knew him, and his passing is a considerable loss to the proof theory community at large. A short memorial talk will be given by Paola Bruscoli after the talks on Thursday 12 September, just before the AGM.
The Workshop will include the following invited talks:- Effectful Realizability. (Abstract)
Liron Cohen (Ben-Gurion University) - Upon This Quote I Will Build My Church Thesis. (Abstract)
Pierre-Marie Pédrot (Inria Rennes) - A generalization of Beth definability, proof-theoretically. (Abstract)
Cécilia Pradic (Swansea University) - Towards combinatorial proof theory. (Abstract)
Lutz Strassburger (Inria Saclay)
Submissions
For the Workshop, we solicit submissions of short abstracts of up to 2 pages (not including references), to be presented as a short talk.
There are no formal published proceedings, but accepted abstracts will be made available for the workshop.
Please submit your abstracts via easychair:
https://easychair.org/conferences/?conf=ps24
Important Dates
-
Abstract deadline:
17 May 202424 May 2024 (extended) - Notification: 7 June 2024
- Final versions:
14 June 202418 June 2024 (extended) - Registration deadline:
2 August 202416 August 2024 (extended) - School: 9-11 September 2024
- Workshop: 12-13 September 2024
Best Student Presentation Award
As is traditional for the Proof Society workshop, there will be an award for the Best Student Presentation at the workshop. The award committee consists of Anupam Das, Marianna Girlando, Andreas Weiermann and Keita Yokoyama.
Colocation with BLC
PS24 will be colocated with the British Logic Colloquium meeting of 2024, taking place 5-7 September.
Registration
The registration prices are:- School & Workshop: £230
- School only: £130
- Workshop only: £130
The registration price includes all lunches, coffee breaks and social events.
Registration is now closed.
Student grants
A small number of registration fee waivers are available for students without access to funding to support their participation. Anyone who would like to request this should contact Anupam Das at the earliest opportunity.
Local Information
International travel by air. Birmingham Airport (BHX) is an international airport serving almost a hundred direct destinations around the world. There are direct trains to Birmingham New Street (about 15 minutes) and from there the University of Birmingham campus (30-40 minutes). The various London airports (Heathrow, Gatwick, Stansted, Luton) and other regional airports (Manchester, Bristol) are also reasonable choices, with train or coach connections from all of them.
International travel by train. It is also possible to travel to Birmingham by train from mainland Europe. There are frequent direct trains from central London to central Birmingham, about 1 hour 20 (or 2 hours for the slower train). Tickets may be bought at the station, or using 3rd party apps such as trainline. A good source for UK train information is National Rail.
Travel within Birmingham. The University train station is served from Birmingham centre by local trains via New Street station as well as several local buses. In general, Google Maps is reliable to find your way around, but not always reliable regarding bus timetables. Bus tickets may be purchased on board using contactless payment. Train tickets may be bought at the station, or using 3rd party apps such as trainline. A good source for UK train information is National Rail.
Accomodation. Edgbaston Park Hotel, the University of Birmingham's hotel, provides accomodation and dining on the Edgbaston campus. A range of alternative options are available either in Edgbaston, such as Edgbaston House and The High Field Town House, or in Birmingham's City Centre, including ibis Birmingham New Street Station, Travelodge Birmingham Central Broadway Plaza, and ibis budget Birmingham Centre. Many other options can also be found on the usual accommodation websites such as Booking, AirBnB, etc.
Tourism. Birmingham is the second largest city of the UK (behind London) and it and the surrounding West Midlands offers plenty of tourism opportunities for all. A good resource for finding things to do in the local area is Visit Birmingham. Closer to the conference, the University of Birmingham campus hosts several interesting places to visit, including the Lapworth Museum of Geology and the Winterbourne House and Garden.
Venue. Both the School and the Workshop will take place at University House, which hosts the Birmingham Business School. The venue is about a 10 minute walk from the University train station, and there are nearby direct buses to Birmingham centre (again, using Google Maps is recommended).
Booklet of Abstracts
A Booklet of Abstracts is available, containing abstracts of all invited lectures, invited talks and contributed talks. This may be updated before the event.
Program
The provisional program for the School and Workshop are given below. Note that this program is subject to change. Last updated 5/9/2024.
All talks for the School (Monday - Wednesday) will take place in room 108. Talks for the Workshop will take place in rooms 108 and 110 as indicated.
| Monday 9 September | ||
| 09:00 - 09:30. | Arrival and registration. | |
| 09:30 - 10:30. | Ulrich Kohlenbach | Proof Mining: Foundations and Applications I (Chair: Anupam Das) |
| 10:30 - 11:00. | Coffee break | |
| 11:00 - 12:00. | Hiroakira Ono | Cut elimination, analytic cut property and interpolation
property I (Chair: Iris van der Giessen) |
| 12:00 - 14:00. | Lunch break (Cafe 1902) | |
| 14:00 - 15:00. | Ulrich Kohlenbach | Proof Mining: Foundations and Applications II (Chair: Anupam Das) |
| 15:00 - 15:30. | Coffee break | |
| 15:30 - 16:30. | Hiroakira Ono | Cut elimination, analytic cut property and interpolation
property II (Chair: Iris van der Giessen) |
| 18:30 - . | Welcome social for School (at Cherry Reds) | |
| Tuesday 10 September | ||
| 09:30 - 10:30. | Ulrich Kohlenbach | Proof Mining: Foundations and Applications III (Chair: Anupam Das) |
| 10:30 - 11:00. | Coffee break | |
| 11:00 - 12:00. | Hiroakira Ono | Cut elimination, analytic cut property and interpolation
property III (Chair: Iris van der Giessen) |
| 12:00 - 14:00. | Lunch break (Cafe 1902) | |
| 14:00 - 15:00. | Paul Shafer | An introduction to reverse mathematics (Chair: Andreas Weiermann) |
| 15:00 - 15:30. | Coffee break | |
| 15:30 - 16:30. | Silvia Ghilezan | The Curry-Howard correspondence journey I (Chair: Abhishek De) |
| Wednesday 11 September | ||
| 09:30 - 10:30. | Paul Shafer | An introduction to reverse mathematics II (Chair: Andreas Weiermann) |
| 10:30 - 11:00. | Coffee break | |
| 11:00 - 12:00. | Silvia Ghilezan | The Curry-Howard correspondence journey II (Chair: Abhishek De) |
| 12:00 - 14:00. | Lunch break (Cafe 1902) | |
| 14:00 - 15:00. | Paul Shafer | An introduction to reverse mathematics III (Chair: Andreas Weiermann) |
| 15:00 - 15:30. | Coffee break | |
| 15:30 - 16:30. | Silvia Ghilezan | The Curry-Howard correspondence journey III (Chair: Abhishek De) |
| 18:30 - . | Welcome reception for Workshop / Closing of School (at Aluna) | |
| Thursday 12 September | ||||
| 09:00 - 09:30. | Arrival and registration | |||
| Invited talk (108) (Session and Local Chair: Paul Levy) | ||||
| 09:30 - 10:30. | Pierre-Marie Pédrot | Upon This Quote I Will Build My Church Thesis | ||
| 10:30 - 11:00. | Coffee break | |||
| Contributed talks (108): | Structural proof theory (Session Chair: Revantha Ramanayake) (Local Chair: Abhishek De) |
Contributed talks (110): | Reverse mathematics (Session Chair: Paul Shafer) (Local Chair: Iris van der Giessen) |
|
| 11:00 - 11:20. | Dale Miller and Elaine Pimentel | Higher-level rules for sequent calculus | Giorgio Genovesi | Reverse Mathematics of Regular CSCS and some Topological Characterizations of ATR0 |
| 11:20 - 11:40. | Borja Sierra Miranda | Coalgebraic proof translations for non-wellfounded proofs | Giovanni Solda | Versions of the minimax theorem in reverse mathematics |
| Mini-break | Mini-break | |||
| 11:50 - 12:10. | Robbe Van den Eede, Robbe Van Biervliet and Marc Denecker | A Sequent Calculus for Generalized Inductive Definitions | Oriola Gjetaj, Lorenzo Carlucci and Andrea Vivi | Free sets and rainbows for colorings of exactly large sets and barriers |
| 12:10 - 12:30. | Stella Mahler | Proof Schemata and Primitive Recursive Arithmetic | Alakh Dhruv Chopra | Strength of the hyperated finitary powerset operator |
| 12:30 - 14:00. | Lunch break (Cafe 1902) | |||
| Invited talk (108) (Session Chair: Pierre-Marie Pédrot) (Local Chair: Iris van der Giessen) | ||||
| 14:00 - 15:00. | Liron Cohen | From Program Logic to Realizability Models | ||
| 15:00 - 15:30. | Coffee break | |||
| Contributed talks (108): | Modal logic (Session Chair: Raheleh Jalali) (Local Chair: Iris van der Giessen) |
Contributed talks (110): | First-order arithmetic (Session Chair: Reinhard Kahle) (Local Chair: Abhishek De) |
|
| 15:30 - 15:50. | Robert Freiman, Carlos Olarte, Elaine Pimentel and Chris Fermüller | Reasoning About Group Polarization: From Semantic Games to Sequent Systems | Eduardo Skapinakis and Marcel Ertel | Logical theories for querying NP |
| 15:50 - 16:10. | Mojtaba Mojtahedi | Polymodal Sigma-provability logic | Eitetsu Ken | Games with backtracking options corresponding to ISigma_k (X) |
| Mini-break | Mini-break | |||
| 16:20 - 16:40. | Joost J. Joosten | Münchhausen provability and applications | Pietro Brocci | Proof-theoretic remarks on extensions of the Kripke-Feferman theory of truth |
| 16:40 - 17:00. | Sonia Marin and Paaras Padhiar | Nested sequents for quasi-transitive modal logics | ||
| Memorial talk (108) (Session and Local Chair: Anupam Das) | ||||
| 17:15 - 17:30. | Paola Bruscoli | Remembering Alessio Guglielmi | ||
| 17:30 - 18:30. | Proof Society Annual General Meeting (108) | |||
| 19:30 - . | Workshop dinner (at The Botanist Gas Street Basin) | |||
| Friday 13 September | ||||
| Invited talk (108) (Session Chair: Stepan Kuznetsov) (Local Chair: Iris van der Giessen) | ||||
| 09:30 - 10:30. | Cécilia Pradic | A generalization of Beth definability, proof-theoretically | ||
| 10:30 - 11:00. | Coffee break | |||
| Contributed talks (108): | Metalogic (Session Chair: Lutz Strassburger) (Local Chair: Iris van der Giessen) |
Contributed talks (110): | Computability and
constructivity (Session Chair: Giovanni Solda) (Local chair: Abhishek De) |
|
| 11:00 - 11:20. | Raheleh Jalali and Stefan Hetzl | On the Completeness of Interpolation Algorithms | ||
| 11:20 - 11:40. | Iris van der Giessen | Uniform Interpolants and Bisimulation Quantifiers: Verified Constructions via Proof Systems | Yudai Suzuki and Keita Yokoyama | Approximating Pi^1_2 consequences of Pi^1_1-CA_0 |
| Mini-break | Mini-break | |||
| 11:50 - 12:10. | Zoltan A. Kocsis | A structural approach to higher-order connectives | Shuwei Wang | The global well-ordering on Weaver's third-order conceptual mathematics |
| 12:10 - 12:30. | Amirhossein Akbar Tabatabai | Universal Proof Theory: Disjunction Property in First-order Theories (v) | Stephen Mackereth | How constructive is Gödel's Dialectica translation? (v) |
| 12:30 - 14:00. | Lunch break (Cafe 1902) | |||
| Invited talk (108) (Session Chair: Isabel Oitavem) (Local Chair: Iris van der Giessen) | ||||
| 14:00 - 15:00. | Lutz Strassburger | Towards combinatorial proof theory | ||
| 15:00 - 15:30. | Coffee break | |||
| Contributed talks (108): | Philosophy (Session Chair: Joost Joosten) (Local chair: Iris van der Giessen) |
Contributed talks (110): | Substructural logic (Session Chair: Dale Miller) (Local Chair: Abhishek De) |
|
| 15:30 - 15:50. | Will Stafford and Mike Schneider | Pure Folding; Making sense of paper folding evangalism | Swapnil Ghosh, Lev Beklemishev and Daniyar Shamkanov | Provably recursive functions of contraction free arithmetic. |
| 15:50 - 16:10. | Robin Martinot | Proof-theoretic syntax as 'semantic' and as 'structural' | Tikhon Pshenitsyn | Complexity of Depth-Bounded Infinitary Action Logic with Multiplexing |
| Mini-break | Mini-break | |||
| 16:20 - 16:40. | Alexander Victor Gheorghiu | From Proof Theory to Argumentation Theory via Proof-theoretic Semantics | Niccolò Veltri and Cheng-Syuan Wan | Craig Interpolation for Semi-Substructural Logics |
| 16:40 - 17:00. | Sophie Nagler | Behavioural Inferentialist Semantics for the Connectives in 2-Sided Sequent Calculi | Stepan Kuznetsov | A Decidable Fragment of the Lambek Calculus with Exponential |
| 17:15 - 17:30. | Best Student Presentation Award (108) | |||
Program Committee
Juan Aguilera (Vienna University of Technology & Ghent University)
Gianluca Curzi (University of Gothenburg & University of Birmingham)
Anupam Das (University of Birmingham) [PC Chair]
Anton Freund (University of Würzburg)
Marianna Girlando (University of Amsterdam)
Raheleh Jalali (Czech Academy of Sciences)
Leszek Kolodziejczyk (University of Warsaw)
Stepan Kuznetsov (Steklov Mathematical Institute)
Sonia Marin (University of Birmingham)
Sara Negri (University of Genoa)
Isabel Oitavem (CMA and DM, FCT, Universidade NOVA de Lisboa)
Fedor Pakhomov (Ghent University)
Frank Pfenning (Carnegie Mellon University)
Thomas Powell (University of Bath)
Revantha Ramanayake (University of Groningen)
Alexis Saurin (CNRS)
Keita Yokoyama (Tohoku University)
Local Organisation
Anupam Das [Conference Chair]
Abhishek De
Iris van der Giessen
Jamie Hough
Paul Levy
Sonia Marin
Lukas Melgaard
Paaras Padhiar
Contact
Any queries should be sent by email to ps24@easychair.org.
Sponsorship and support
Social events
On Monday 9 September, there will be a welcome social for the School at Cherry Reds Cafe Bar. There will be a simple food buffet and a bar for drinks.
On Wednesday 11 September, there will be a welcome reception for the Workshop at Aluna in the Mailbox. There will be some appetisers and one free drink (further drinks must be bought at the bar).
On Thursday 12 September the Workshop social dinner will take place at The Botanist (Gas Street Basin) which overlooks the iconic Birmingham canals. NB: there are two 'The Botanist' establishments in Birmingham, so ensure you come to the 'Gas Street Basin' one!
Here is a map of the various social events during the week: