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:

Invited Lecturers and Speakers

The School will consist of the following courses: The Workshop will include the following invited talks:

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

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.

Colocation with BLC

PS24 will be colocated with the British Logic Colloquium meeting of 2024, taking place 5-7 September.

Registration

Registration is now open via the online shop until 2 August 2024:
https://shop.bham.ac.uk/conferences-and-events/college-of-engineering-physical-sciences/school-of-computer-science/computer-science-courses-events/proof-society

The registration prices are:

The registration price includes all lunches, coffee breaks and social events.

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.

Social events

On Monday 9 September, there will be a welcome social for the School at Cherry Red's Cafe Bar.

On Wednesday 11 September, there will be a welcome reception for the Workshop at Aluna in the Mailbox.
The Workshop social dinner will take place on Thursday 12 September at The Botanist (Gas Street Basin) which overlooks the iconic Birmingham canals.

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.

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).

Program

The tentative programs for the School and Workshop are given below. More details will be added over time.

Monday 9 September
09:00 - 09:30. Welcome and Registration.
09:30 - 10:30. Ulrich Kohlenbach Proof Mining: Foundations and Applications I
10:30 - 11:00. Coffee break
11:00 - 12:00. Hiroakira Ono Cut elimination, analytic cut property and interpolation property I
12:00 - 14:00. Lunch break
14:00 - 15:00. Ulrich Kohlenbach Proof Mining: Foundations and Applications II
15:00 - 15:30. Coffee break
15:30 - 16:30. Hiroakira Ono Cut elimination, analytic cut property and interpolation property II
Evening. Welcome social for School
Tuesday 10 September
09:30 - 10:30. Ulrich Kohlenbach Proof Mining: Foundations and Applications (III)
10:30 - 11:00. Coffee break
11:00 - 12:00. Hiroakira Ono Cut elimination, analytic cut property and interpolation property III
12:00 - 14:00. Lunch break
14:00 - 15:00. Paul Shafer An introduction to reverse mathematics I
15:00 - 15:30. Coffee break
15:30 - 16:30. Silvia Ghilezan The Curry-Howard correspondence journey I
Wednesday 11 September
09:30 - 10:30. Paul Shafer An introduction to reverse mathematics II
10:30 - 11:00. Coffee break
11:00 - 12:00. Silvia Ghilezan The Curry-Howard correspondence journey II
12:00 - 14:00. Lunch break
14:00 - 15:00. Paul Shafer An introduction to reverse mathematics III
15:00 - 15:30. Coffee break
15:30 - 16:30. Silvia Ghilezan The Curry-Howard correspondence journey III
Evening. Welcome reception for Workshop / Closing of School
Thursday 12 September
  Invited talk (I1)
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 (A1): Structural proof theory Contributed talks (B1): Reverse mathematics
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
  Invited talk (I2)
14:00 - 15:00. Liron Cohen From Program Logic to Realizability Models
15:00 - 15:30. Coffee break
  Contributed talks (A2): Modal logic Contributed talks (B2): Computability and constructivity
15:30 - 15:50. Robert Freiman, Carlos Olarte, Elaine Pimentel and Chris Fermüller Reasoning About Group Polarization: From Semantic Games to Sequent Systems Yudai Suzuki and Keita Yokoyama Approximating Pi^1_2 consequences of Pi^1_1-CA_0
15:50 - 16:10. Sonia Marin and Paaras Padhiar Nested sequents for quasi-transitive modal logics Jan Gronwald Problems of Representation of Ordinary Mathematics in Reverse Mathematics
  Mini-break Mini-break
16:20 - 16:40. Joost J. Joosten Münchhausen provability and applications Shuwei Wang The global well-ordering on Weaver's third-order conceptual mathematics
16:40 - 17:00. Mojtaba Mojtahedi Polymodal Sigma-provability logic Stephen Mackereth How constructive is Gödel's Dialectica translation?
Evening. Workshop dinner
Friday 13 September
  Invited talk (I3)
09:30 - 10:30. Cécilia Pradic A generalization of Beth definability, proof-theoretically
10:30 - 11:00. Coffee break
  Contributed talks (A3): Metalogic Contributed talks (B3): First-order arithmetic
11:00 - 11:20. Raheleh Jalali On the Completeness of Interpolation Algorithms Eduardo Skapinakis and Marcel Ertel Logical theories for querying NP
11:20 - 11:40. Iris van der Giessen Uniform Interpolants and Bisimulation Quantifiers: Verified Constructions via Proof Systems Eitetsu Ken Games with backtracking options corresponding to ISigma_k (X)
  Mini-break Mini-break
11:50 - 12:10. Zoltan A. Kocsis A structural approach to higher-order connectives Piotr Gruza Tightness and solidity in fragments of Peano Arithmetic
12:10 - 12:30. Amirhossein Akbar Tabatabai Universal Proof Theory: Disjunction Property in First-order Theories Pietro Brocci Proof-theoretic remarks on extensions of the Kripke-Feferman theory of truth
12:30 - 14:00. Lunch break
  Invited talk (I4)
14:00 - 15:00. Lutz Strassburger Towards combinatorial proof theory
15:00 - 15:30. Coffee break
  Contributed talks (A4): Philosophy Contributed talks (B4): Substructural logic
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

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



Maintained by Anupam Das. Last updated