StrIP Kick-Off Workshop

University of Birmingham, June 7-10, 2022.

Structure vs Invariants in Proofs (StrIP) is a UKRI-funded project that began in 2020. After more than two years of pandemic-interrupted scientific activity, we are finally able to put together a 'kick-off' workshop (now over halfway into the initial phase of the project)!

StrIP aims to bring together techniques from structural proof theory, automaton theory, and metamathematics in order to advance the state of (cyclic) proof theory at large. Particular themes that prevail throughout the project are:

StrIP has been funded for £1.46 million for the first 4 years, with a 3 year extension envisioned too. This funding will cover the recruitment of 8 person-years of postdoctoral research and support regular research visits. This is supported by several PhD studentships financed by the University of Birmingham.

Venue

Talks will take place in the G35 lecture theatre in the School of Chemical Engineering. It is a 3 minute walk from the University train station and closest bus stop.

All breaks and lunches will take place in the Atrium (entrance) of the School of Computer Science, where there are also a number of meeting rooms available for collaboration etc. It is about a 2 minute walk from the School of Chemical Engineering and a 1 minute walk from the University train station and closest bus stop.

Workshop dinner

The workshop dinner will take place at Estado da Índia, a Portuguese-Indian fusion restaurant in Harborne. It is about 20 minutes walk from the School of Computer Science.

COVID-19

The United Kingdom no longer has any legal restrictions pertaining to COVID-19. In particular, there is no mask mandate on public transport or in public places. Such matters are left to personal judgement, but all participants should be respectful towards others' preferences.

Program

Abstracts can be accessed by clicking on the title of a talk.

Note that the timings from Wednesday afternoon onwards are different from those earlier, namely in that the short breaks have been made 15 minutes longer.

Tuesday 7 June

12:00 - 13:45 Lunch
13:45 - 14:00 Welcome
Modal and relational fixed point logics. Chair: Reuben Rowe.
14:00 - 15:00 Yde Venema Games and automata in the proof theory of modal fixpoint logics
15:00 - 15:30 Break
15:30 - 15:50 Johannes Marti A focus-style proof system for the alternation-free mu-calculus
15:50 - 16:10 Gullermo Menéndez Turata A cyclic proof system for CTL*
16:10 - 16:30 Emile Hazard Cyclic proofs for transfinite expressions
16:30 - 16:45 Overflow and discussion

Wednesday 8 June

Structural proof theory. Chair: Sonia Marin.
09:30 - 10:30 Revantha Ramanayake Restrict what you can't eliminate
10:30 - 11:00 Break
11:00 - 11:20 Vitor Greati Finite and analytic two-dimensional proof systems for non-finitely axiomatizable logics
11:20 - 11:40 Marianna Girlando Cyclic Proofs, Hypersequents, and Transitive Closure Logic
11:40 - 12:00 Iris van der Giessen Rules that reason about rules
12:00 - 12:15 Overflow and discussion
12:15 - 14:00 Lunch
Linear logic and type systems with fixed points. Chair: Graham Leigh.
14:00 - 15:00 Alexis Saurin Cuts all the way up
15:00 - 15:45 Break
15:45 - 16:05 Dale Miller Peano Arithmetic and muMALL
16:05 - 16:25 Farzad Jafarrahmani A concrete model of finitary/infinitary linear logic with fixed-points
16:25 - 16:45 Gianluca Curzi On the computational strength of logics with fixed points
16:45 - 17:00 Overflow and discussion

Thursday 9 June

Deep inference. Chair: Lutz Strassburger.
09:30 - 10:30 Alessio Guglielmi Substitutions and U-Turns
10:30 - 11:15 Break
11:15 - 11:35 Torie Barrett Strictly Linear Proofs and Substitution
11:35 - 11:55 Tom Powell How Deep is the Dialectica?
11:55 - 12:15 Anupam Das Towards cyclic deep inference: Formalism F
12:15 - 12:30 Overflow and discussion
12:30 - 14:00 Lunch
Logic and circularity. Chair: Anupam Das.
14:00 - 15:00 Graham Leigh Fixpoints, truth and conservation
15:00 - 15:45 Break
15:45 - 16:05 Giacomo Barlucchi A new attempt on closure ordinals in the mu-calculus
16:05 - 16:25 Dominik Wehr Cyclic Reset Proofs
16:25 - 16:45 Colin Riba LMSO: A linear monadic second-order logic over omega-words
16:45 - 17:00 Overflow and discussion
19:00 - late Workshop dinner

Friday 10 June

Graphical representations of proofs. Chair: Gianluca Curzi.
09:30 - 10:30 Lutz Strassburger A gentle introduction to combinatorial proofs
10:30 - 11:15 Break
11:15 - 11:35 Giti Omidvar From atomic flows to combinatorial flows
11:35 - 11:55 Willem Heijltjes Normalization Without Syntax
11:55 - 12:15 Matteo Acclavio On Game Semantics and Combinatorial Proofs
12:15 - 12:30 Overflow and discussion
12:30 - 14:00 Closing and lunch

Meeting rooms

Several meeting rooms are available for scientific discussion and collaboration during the week. Availability is detailed in the table below. All rooms are located on the second floor of the School of Computer Science (no card or key required), except LG23 which is located on floor -1.

Room: 217 222 225 245 LG23

Tuesday 7 June
11am-6pm
9am-12pm
2pm-6pm
9am-6pm
-

-

Wednesday 8 June

-

9am-12pm
2pm-6pm
9am-6pm 9am-6pm
-

Thursday 9 June
9am-6pm
-
9am-6pm 11am-6pm
-

Friday 10 June
9am-2pm
-

-

-
9am-2pm

Participants

Adrián Puerto Aubel (University of Groningen) Francisco Trucco Dalmas (University of Groningen) Lukas Melgaard (University of Copenhagen)
Alessio Guglielmi (University of Bath) Giacomo Barlucchi (University of Gothenburg) Lutz Strassburger (Inria Saclay)
Alexis Saurin (CNRS, IRIF) Gianluca Curzi (University of Birmingham) Marianela Morales (Inria Saclay)
Anupam Das (University of Birmingham) Giti Omidvar (Inria Saclay) Marianna Girlando (University of Birmingham)
Avgerinos Delkos (University of Birmingham) Graham Leigh (University of Gothenburg) Matteo Acclavio (University of Luxembourg)
Cameron Allett (University of Bath) Guillermo Menéndez Turata (University of Amsterdam) Reuben Rowe (Royal Holloway)
Chris Barrett (University of Bath) Iris van der Giessen (Utrecht University) Revantha Ramanayake (University of Groningen)
Colin Riba (ENS Lyon) James Brotherston (University College London) Sonia Marin (University of Birmingham)
Dale Miller (Inria Saclay) Johannes Kloibhofer (University of Amsterdam) Tom Powell (University of Bath)
Dominik Wehr (University of Gothenburg) Johannes Marti (University of Amsterdam) Torie Barrett (University of Bath)
Emile Hazard (ENS Lyon) Jui-Hsuan Wu (Inria Saclay) Vitor Greati (University of Groningen)
Esaie Bauer (IRIF) Keji Neri (University of Bath) Willem Heijltjes (University of Bath)
Farzad Jafarrahmani (IRIF) Kostia Chardonnet (LRI) Yde Venema (University of Amsterdam)
Yury Savateev (Birkbeck, University of London)

Local organisers

Anupam Das
Suman Khan

Contact

Any queries should be addressed to Anupam Das.