A 2½-day workshop dedicated to current and future trends in cyclic and illfounded forms of provability and justification. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity, the Swedish Research Council through the research project Proofs with Cycles and Computation, and the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg.

Speakers

  • Henning Basold (Leiden University)
  • Anupam Das (University of Birmingham)
  • Sebastian Enqvist (Stockholm University)
  • Zeinab Galal (RIMS, Kyoto)
  • Iris van der Giessen (University of Amsterdam)
  • Marianna Girlando (University of Amsterdam)
  • Helle Hvid Hansen (University of Groningen)
  • Stefan Hetzl (TU Wien)
  • Alex Leitsch (TU Wien)
  • Reuben Rowe (Royal Holloway)
  • Alexis Saurin (IRIF)
  • Takeshi Tsukada (Chiba University)

Workshop photo

Location

The workshop will be held at the Faculty of Humanities of the University of Gothenburg, address Renströmsgatan 6, Gothenburg. It is adjacent to the Korsvägen transport hub and within walking distance from the city centre.

Registration

Attendence is free but registration is required. The deadline for registration has passed. In case of questions, contact Gianluca Curzi.

Schedule

The workshop starts at 9am on Wednesday, 24 September and closes at 12.30 on of Friday, 26 September 2025. All talks will be in room J439 in the Humanisten building of Gothenburg University.

Wednesday, 24 September

  • 9.00 Registration
  • 9.30 Alexis Saurin – Čubrić’ interpolation for sequent proofs: What it takes to interpolate in a proof-relevant way

    Abstract: After Craig’s seminal results on interpolation theorem, a number and variety of proof-techniques have been designed to establish interpolation theorems. Among them, one can single out Maehara’s method for its applicability to a wide range of logics admitting cut-free complete proof systems.

    By reconsidering Maehara’s method, I will show how one can extract a “proof-relevant” interpolation theorem (that I will refer to as Čubrić’ interpolation) for first-order linear-logic. This proof-relevant approach to interpolation will be referred to as Čubrić’ interpolation after Djordje Čubrić, a PhD student of Makkai who was the first to consider this kind of results in the 90’s

    Interpolation can be organized in two successive phases, bottom-up and top-down, the top-down phase synthesizing the interpolant by introducing cuts. The flexibility of the approach is exploited to carry the interpolation-as-cut-introduction to classical and intuitionistic logics, satisfying Craig as well as Lyndon’s constraints on the vocabulary of the interpolant. Moving to Curien & Herbelin’s “duality of computation” framework (system L) I will then show a computational version of the above result in System L.

    In a second part of the talk, I will consider the question of how one can weaken some of the assumptions on which Čubrić’ interpolation lies. More precisely, while Maehara’s method relies strongly both on (i) the tree structure of sequent proofs (ii) their wellfoundedness and (iii) their cut-freeness, I will outline how the cut-introduction method can be extended: (i) to proof nets, that are graphs where the order of inference rules has been forgotten, exploiting their correctness criteria, as well as (ii) to circular proofs in logics with fixed-points, where proofs contain cycles and wellfounded of proof objects is relaxed and (iii) proofs with some forms of cuts.

  • 10.30 Break
  • 11.00 Alex Leitsch – Proof Schemata and Herbrand systems

    Abstract: A proof schema is an expression (recursively) representing an infinite sequence of proofs. Proof schemata depend on parameters (variables over natural numbers) and evaluate to proofs when the parameters are replaced by numerals. These schemata provide a formalism to express induction without induction rules. The main application of proof schemata lies in the (automated) analysis of mathematical proofs using induction. While Herbrand’s theorem fails in presence of induction it can be realized in proof schemata. Instead of a single Herbrand sequent (we work in sequent calculus) we obtain an infinite sequence of Herbrand sequents. A Herbrand system is the corresponding (recursively defined) infinite sequence of Herbrand substitutions defining the Herbrand sequents. As, in general, the computation of a Herbrand sequent requires cut-elimination, a cut-elimination method for schemata is needed. Schematic CERES (Cut-elimination by RESolution) is such a method which will be presented in brief. By their potential in extracting relevant information from mathematical proofs, Herbrand systems provide a powerful tool in automated proof analysis.

  • 12.00 Lunch
  • 13.30 Helle Hvid Hansen – Craig Interpolation for PDL via Cyclic Tableaux

    Abstract: The question of whether Propositional Dynamic Logic (PDL) has Craig interpolation was disputed for several years, with three proof attempts being published but later criticized or retracted. In this talk, I will present a proof based on the ideas of Borzechowski (1988). The proof uses a cyclic tableau system for PDL and an adaptation of Maehara’s method. In this approach, interpolants for cycles are obtained as the solutions to fixpoint equations, and the challenge is to ensure that these fixpoint equations have solutions in PDL. To achieve this, the construction of interpolants for clusters (strongly connected components) employs an auxiliary structure called a quasi-tableau.

    This is joint work with Malvin Gattinger, Revantha Ramanayake, Valentina Trucco Dalmas and Yde Venema.

  • 14.30 Marianna Girlando – Propositional Dynamic Logic to Transitive Closure Logic: Cyclic Proofs via Hypersequents

    Abstract: Propositional Dynamic Logic (PDL) is a modal logic for reasoning about the iterative execution of programs. Via the standard translation, PDL can be embedded into Transitive Closure Logic (TCL), an extension of first-order logic with a recursive operator expressing the transitive closure of binary relations. Cyclic proof systems based on Gentzen-style sequents have been developed for both PDL and TCL in the literature, but cyclic proofs for PDL do not directly translate into cyclic proofs for TCL. Therefore, the standard translation does not lift to the level of Gentzen-style cyclic proofs. Motivated by this observation, we introduce a hypersequent-style cyclic proof system for TCL, which enriches Gentzen-style sequents with additional structural connectives. We prove that this system is sound and that it simulates cyclic proofs for PDL, thereby establishing cut-free completeness for a fragment of TCL.

    This talk is based on joint work with Anupam Das, published in the Journal of Automated Reasoning: https://link.springer.com/article/10.1007/s10817-023-09675-1. A preprint is available here: https://arxiv.org/abs/2205.08616

  • 15.30 Break
  • 16.00 Graham E Leigh – Cyclic interpolation and all the rest

Thursday 25 September

  • 9.00 Takeshi Tsukada – Software model checking and cyclic proof search

    Abstract: The software model-checking community have developed many procedure to efficiently find an inductive invariant of a given program. By a well-known connection between software model checking and fixed-point logics, what these procedures seek can be seen as an appropriate cut. In this talk, I will present how software model-checking procedure can naturally seen as a proof-search procedure in a cyclic proof system. Interestingly, the cyclic proof perspective allows us to compare seemingly different procedures, such as IC3/PDR and Furzan-Kincaid procedure for game solving, and I expect this perspective would also be useful in developing new procedures.

    This talk is based on joint work with Hiroshi Unno published in POPL 2022 and PLDI 2023.

  • 10.00 Break
  • 10.30 Reuben Rowe – Algorithms for Checking Infinite Descent

    Abstract: The (PSPACE-complete) Infinite Descent property underpins the trace-based validation of cyclic derivations that capture inductive and coinductive reasoning, as well as the size-change approach to proving program termination. In the literature, we find a couple of different algorithms described for deciding Infinite Descent: a dynamic programming algorithm incorporating a fixed-point saturation (e.g. as suggested in the size-change termination paper by Lee, Jones, and Ben-Amram), and an encoding via containment of omega automata (e.g. in Brotherston’s thesis).

    In this talk I will describe work in which we have developed an alternative automata-theoretic encoding (with some connections to a construction described by Dax, Hoffman and Lange) and an optimisation of the dynamic programming algorithm that takes into account some specific symmetries present in the Infinite Descent problem. I will also describe some more efficient, but approximate (i.e. incomplete) approaches for checking Infinite Descent that we have developed. I will comment on the relative tradeoffs in the (runtime) complexity of the decision procedures, and report on an experimental evaluation of our implementations of these algorithms within the Cyclist theorem prover framework. Interestingly, we found the approximate methods to provide good coverage in practice.

  • 11.30 Stefan Hetzl – Clause set cycles

    Abstract: The notion of clause set cycle abstracts a family of methods for automated inductive theorem proving based on the detection of cyclic dependencies between clause sets. A clause set cycle closely corresponds to a proof by infinite descent. The strength of clause set cycles can be characterised by a theory. This characterisation paves the way to showing independence results of practical relevance for automated deduction. In this talk, I will present this characterisation and several practically relevant independence results based on different features of clause set cycles.

    This is joint work with Jannik Vierling.

  • 12.30 Lunch
  • 14.00 Anupam Das – Right-linear algebras: decomposing the theory of regular languages via cyclic proofs

    Abstract: In the second half of the 20th century various theories of regular expressions were proposed, eventually leading to the notion of a Kleene Algebra (KA). Kozen and Krob independently proved the completeness of KA for the model of regular languages, a now celebrated result that has been refined and generalised over the years. In recent years proof theoretic approaches to regular languages have been studied, providing alternative routes to metalogical results like completeness and decidability.

    In this talk I will present a new approach from a different starting point: finite state automata. A notation for non-deterministic finite automata is readily obtained via expressions with least fixed points, leading to a theory of right-linear algebras (RLA). RLA is strictly more general than KA, e.g. admitting ω-regular languages as a model too, and enjoys a simpler proof theory than KA. This allows us to recover (more general) metalogical results in a robust way, combining techniques from automata, games, and cyclic proofs. In particular, our development exposes a novel factorisation of the completeness for KA, controlling the use of multiplication.

    This talk is based on joint works with Abhishek De.

  • 15.00 Break 
  • 15.30 Sebastian Enqvist – Computation by infinite descent made explicit

    Abstract: I will present a non-wellfounded proof system for intuitionistic logic extended with ordinary inductive and co-inductive definitions, based on a syntax in which fixpoint formulas are annotated with explicit variables for ordinals. My main motivation for studying this system was to get a better understanding of the recently introduced validity criterion for non-wellfounded proofs in terms of so called “bouncing threads”. I will describe the computational content of this system via a notion of computability and show that every valid proof is computable. A consequence of this result is that every proof of a sequent of the appropriate form represents a unique function on natural numbers. Finally, we derive a categorical model from the proof system and show that least and greatest fixpoint formulas correspond to initial algebras and final coalgebras respectively.

Friday 26 September

  • 9.30 Zeinab Galal – A categorical viewpoint on systems of fixpoint equations

    Abstract: Fixpoints play an important role in both denotational semantics where they are used to represent recursively defined programs and data types as well as in operational semantics where many behavioral equivalences are obtained as fixpoints of some relation transformers.

    In the categorical theory of fixpoint operators, we usually consider one fixpoint operator at a time and little attention is given to the study of mixed fixpoint operators where we take a different fixpoint operator for each variable. Systems combining least and greatest fixpoints over lattices are an important example as they are the basis of many static analysis and model checking methods.

    I will present in this talk an axiomatization of mixed fixpoint operators first in the 1-categorical setting and then briefly mention how to extend to 2-categories in order to capture the examples of (parametrized) initial algebras and coalgebras of accessible functors, analytic and polynomial

  • 10.30 Break
  • 11.00 Hening Basold – Invariants in Cyclic Proofs

    Abstract: In this talk, I will present general category theoretical approaches to recursive computations and proofs, which are ensured to be well-defined by local invariants. That is, it is not necessary to check programs and proofs as a whole to guarantee that they have productive operational semantics, rather the conditions are checked at each step of their composition. A well-known instance is guarded recursion in the so-called topos of trees and the resulting type systems with the so-called later modality. We will discuss how the approach of guarded recursion can be extended to other categories than that of sets and maps, which is where the topos of trees originates, and even to situations that are not Cartesian. This allows us to construct recursive proof systems for non-classical, modal and quantitative logic. However, from the coalgebraic perspective, we can only construct causal computations and proofs in the topos of trees, which means that each approximation step of a recursion only depends on previous steps. We will see in the talk how to move beyond this and devise a category theoretical approach to guarded recursion that captures uniform continuity. This enables a much broader class of recursive computations and proofs that are guaranteed to be well-defined by local invariants.

  • 12.00 Closing

Organisers

  • Graham E Leigh
  • Gianluca Curzi
  • Bahareh Afshari
  • Ivan Di Liberti
  • Dominik Wehr
  • Giacomo Barlucchi

In case of questions, contact Graham Leigh