*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:

- Interactions between proof theory and automaton theory, e.g. relating forms of 'deep inference' to richer features in automata, or using automaton models as targets of computational interpretations of proofs..
- 'Cyclic' proof interpretations, e.g. lifting correspondences between modal logic and predicate logic, or between type systems and predicate logic, to the circular setting.
- Expanding the scope of structural proof theoretic methods for addressing metalogical questions, e.g. via richer calculi such as deep inference or labelled sequents.

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.

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.

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.

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.

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

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 |

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 |

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 |

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 |

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 |

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) | 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) | Yde Venema (University of Amsterdam) | |

Yury Savateev (Birkbeck, University of London) |

Anupam Das

Suman Khan

Any queries should be addressed to Anupam Das.