The FLAPS workshop will take place on the 12th of March 2026 in Amsterdam. It aims to connect researchers and students interested in fixpoint logics, (cyclic) proof theory and related topics. Participation is free and no registration is required.
The workshop is co-located with the PhD defense of Johannes Kloibhofer. The defense is public and will be held on the 13th of March at 11 am at the Aula of the University of Amsterdam (Singel 411, Amsterdam).
| Time | Speaker | Title |
|---|---|---|
| 09:30–10:20 | Thomas Studer | Provability via non-wellfounded proofs. |
| 10:20–10:50 | Coffee | |
| 10:50–11:40 | Iris van der Giessen | Uniform interpolation for intuitionistic Gödel-Löb logic iGL. |
| 11:40–12:30 | Marianna Girlando | Cyclic proofs for transitive closure logic via hypersequents. |
| 12:30–14:00 | Lunch | |
| 14:00–14:50 | Sebastian Enqvist | Computation by infinite descent made explicit. |
| 14:50–15:20 | Coffee | |
| 15:20–16:10 | Balder ten Cate | Craig interpolation within the landscape of decidable fragments of first-order logic. |
| 16:10–17:00 | Dominik Wehr | How (un-)constructive is cyclic proof theory? |
| 19:00- | Dinner |
Thomas Studer: Provability via non-wellfounded proofs.
We study provability logics from the perspective of non-wellfounded proofs. After introducing local progress sequent calculi, we establish syntactic cut-elimination. The cut-free calculi are then used to prove arithmetical completeness and interpolation results.
Iris van der Giessen: Uniform interpolation for intuitionistic Gödel-Löb logic iGL.
Logic iGL can be considered as a member of the provability logic family. It is an intuitionistic version of the well-known Gödel-Löb GL that describes the behavior of the provability predicate in Peano Arithmetic. Many provability logics, including GL, are known to have the very nice uniform interpolation property; this is a strong form of Craig interpolation that enables to define propositional quantifiers inside the logic. However, the uniform interpolation problem for iGL remained open! Together with Borja Sierra Miranda and Guillermo Menéndez Turata we solve the problem by using non-wellfounded proof theory. In the talk I would like to provide an overview of our proof idea including non-wellfounded proofs for iGL, the fixpoint theorem and interpolant constructions.
J.w.w. Borja Sierra Miranda and Guillermo Menéndez Turata.
Marianna Girlando: Cyclic proofs for transitive closure logic via hypersequents.
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.
Sebastian Enqvist: Computation by infinite descent made explicit.
Non-wellfounded proof systems have found interesting applications with respect to Curry-Howard correspondence. In this talk I will present a non-wellfounded proof system for intuitionistic logic extended with 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.
Balder ten Cate: Craig interpolation within the landscape of decidable fragments of first-order logic.
Motivated by applications of Craig interpolation in computer science, I will discuss some recent work pertaining to the Craig interpolation property (CIP) for various important decidable fragment of first-order logic, including guarded fragments, finite-variable fragments, and ordered fragments. Most of these fragments lack the CIP. We will discuss strategies that have been proposed to deal with this lack of CIP, as well as recent results that shed light on where, within the landscape of decidable fragment of first-order logic, one may find logics that enjoy CIP. Time permitting, I will also touch on recent results regarding size bound for Craig interpolants and uniform interpolants in modal logics.
Dominik Wehr: How (un-)constructive is cyclic proof theory?
Many arguments in cyclic proof theory deal with infinite branches of finite proof objects. Typically, these branches are ‘tamed’ by means of classical principles. I will present joint work with Dominik Kirst which shows that the usual global trace condition ‘forces’ this classicality upon us and offer an alternative notion which is classically equivalent but constructively better behaved.
The workshop will take place in L1.12 at Lab42 in Science Park Amsterdam. Click here for the address.
There will be a workshop dinner after the workshop at Restaurant Elixer. The restaurant is within walking distance of Science Park. Note that the dinner is only covered for the speakers, others need to pay themselves. If you want to join the dinner, please fill in the form here so that we can make a reservation.
For any questions please contact Daniël Otten at daniel@otten.co or Johannes Kloibhofer at j.kloibhofer@proton.me.