# FICS 2024 - Fixed Points in Computer Science

### 12th International Workshop on Fixed Points in Computer Science

##### Naples, 19th and 20th February 2024

## Workshop Program

Names of presenters for contributed talks are underlined. Note that two talks of session 4 have been swapped due to a presentation constraint.

### Monday 19 February

##### Session 1 (8:50-10:20) Chair: Alexis Saurin

**08:50-09:00:****Workshop opening.****09:00-9:50:****Invited talk by Anupam Das.***On the Computational Strength of Circular Proofs*(slides)

The last 10 years has seen a surge of renewed interest in non-wellfounded proofs, from modal and predicate logics to more structural proof theoretic endeavours. A particularly fascinating direction, pioneered by the French school, is to construe circular proofs as a typing discipline for functional programs, à la Curry-Howard. Circular typing has a notable advantage against traditional (co)recursors: the operational semantics are more explicit, closer to low-level machine models with loops while nonetheless enjoying excellent metalogical properties. After foundational work of Santocanale, Baelde and Clairambault in the 2000s, the subject was considerably advanced in the 2010s by several researchers in the Paris circle.

A recurring question running through these works has been to gauge the precise computational strength of circular proofs. The obvious problem here is the non-constructive character of totality/soundness arguments for non-wellfounded proofs, a barrier to traditional approaches. In this talk I will survey a recent line of work building up a general methodology for answering such questions via a metamathematics. In particular, we manage to pin down the precise computational strengths of a circular version of system T and its extension by least and greatest fixed points.

This talk is partly based on joint work with Gianluca Curzi.**9:50-10:20:****Bahareh Afshari,***Giacomo Barlucchi*and Graham E. Leigh.*The Limit of Recursion in State-based Systems*(slides)

**10:20-10:45: Coffee break**

##### Session 2 (10:45-12:45) Chair: Anupam Das

**10:45-11:15:***Gianluca Curzi*, Matteo Acclavio and Giulio Guerrieri.*Non-Uniform Polynomial Time and Non-Wellfounded Parsimonious Proofs*(slides)**11:45-12:15:****Bahareh Afshari and***Johannes Kloibhofer*.*Cut Elimination for Cyclic Proofs: A Case Study in Temporal Logic*(slides)**12:15-12:45:***Esaïe Bauer*and Alexis Saurin.*Cut-Elimination for the Circular Modal $\mu$-Calculus: the Benefits of Linearity*(slides)

**12:45-14:00: Lunch**

##### Session 3 (14:00-16:00) Chair: Benedikt Ahrens

**14:00-14:30:***Zeinab Galal*and Jean-Simon Pacaud Lemay.*Combining Fixpoint and Differentiation Theory*(slides)**14:30-15:00:****Luigi Santocanale and***Gregory Chichery*.*Lifting Final Coalgebras and Initial Algebras, a Reconstruction*(slides)**15:00-15:30:***Paige Randall North*and Maximilien Peroux.*Coinductive Control of Inductive Data Types*(slides)

**16:00-16:30: Coffee break**

##### Session 4 (16:30-18:30) Chair: Zeinab Galal

**16:30-17:00:***Farzad Jafarrahmani*and Noam Zeilberger.*A Fibrational Characterization for Unicity of Solutions to Generalized Context-Free Systems*(slides)**17:00-17:30:***Rémy Cerda*.*Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary $\lambda$-Calculi*(slides)**17:30-18:00:****Ralph Matthes, Kobe Wullaert and***Benedikt Ahrens**Substitution for Non-Wellfounded Syntax with Binders through Monoidal Categories*(slides)**18:00-18:30:***Mohamed Hamza Bandukara*and Nikos Tzevelekos.*Nominal Logics for Fresh Register Automata*(slides)

**18:30-20:00: CSL welcome reception**

#### Tuesday 20 February

**09:00-09:30 CSL’24 Opening**

##### Session 5 (09:30-10-30) Chair: Bahareh Afshari

**09:30-10:30****Invited talk (joint with CSL’24) by Barbara König.***Approximating Fixpoints of Approximated Functions*(slides and handout)

There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration.

It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions.

After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated.

We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions.

We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints.

This is joint work with Paolo Baldan, Sebastian Gurke, Tommaso Padoan and Florian Wittbold.

**10:30-11:00: Coffee break**

##### Session 6 (11:00-13:05) Chair: Abhishek De

**11:30-12:00:***Florian Bruse*, David Kronenberger and Martin Lange.*Characterizing the Exponential-Space Hierarchy Via Partial Fixpoints (slides)***12:00-12:30:***Leonardo Pacheco*.*The $\mu$-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics*(slides)**12:30-13:00:****Daniel Hausmann, Nir Piterman,***Irmak Saglam*and Anne-Kathrin Schmuck.*Fixpoints for Fair Parity/$\bot$ Games*

**13:00-13:05: Workshop conclusion**