FICS 2024 - Fixed Points in Computer Science

12th International Workshop on Fixed Points in Computer Science

Naples, 19th and 20th February 2024

Workshop Program

Back to FICS'24 main webpage

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
  • 12:45-14:00: Lunch
Session 3 (14:00-16:00) Chair: Benedikt Ahrens
  • 16:00-16:30: Coffee break
Session 4 (16:30-18:30) Chair: Zeinab Galal
  • 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
  • 13:00-13:05: Workshop conclusion