FICS 2024 - Fixed Points in Computer Science

Naples, 19th and 20th February 2024

List of contributions / Invited speakers / FICS'24 Program / CFP / Program Committee / Steering Committee / FICS history


The 12th International Workshop on Fixed Points in Computer Science will take place in Naples as a satellite of the International Conference CSL 2024 (Computer Science Logic) on the 19th (8h50 — 18h30) and 20th (9h30 — 13h05) of February 2024 in CENTRO CONGRESSI FEDERICO II, Via Partenope, 36.

The call for contributions is online!

News

General description

The goal is to bring together people from different subfields such as algebra/coalgebra, verification, logic, around the thematic of fixed points. Fixed points play a fundamental role in several areas of computer science. They are used to justify (co)recursive definitions and associated reasoning techniques. The construction and properties of fixed points have been investigated in many different settings such as: design and implementation of programming languages, logics, verification, databases. Topics include, but are not restricted to:

  • fixed points in algebra and coalgebra
  • fixed points in formal languages and automata
  • fixed points in game theory
  • fixed points in programming language semantics
  • fixed points in proofs
  • fixed points in the mu-calculus and modal logics
  • fixed points in process algebras and process calculi
  • fixed points in functional programming and type theory
  • fixed points in relation to dataflow and circuits
  • fixed points in automated theorem proving, interactive theorem proving and logic programming
  • fixed points in finite model theory, descriptive complexity theory, and databases
  • fixed points in category theory for logic in computer science

Invited speakers

  • Anupam DAS (University of Birmingham): On the computational strength of circular proofs
    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.
  • Barbara KÖNIG (University of Duisburg-Essen): Approximating Fixpoints of Approximated Functions
    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.

Program committee

  • Zena Ariola (University of Oregon, USA)
  • Abhishek De (University of Birmingham, UK)
  • Zeinab Galal (Università degli sutdi di Bologna, Italy)
  • Guilhem Jaber (Université de Nantes, France)
  • Ekaterina Komendantskaya (Heriot-Watt University, UK)
  • Denis Kuperberg (CNRS & ENS Lyon, France)
  • Martin Lange (University of Kassel, Germany)
  • Christine Paulin (Université Paris Saclay, France)
  • Daniela Petrisan (Université Paris Cité, France)
  • Alexis Saurin (CNRS & Université Paris Cité, France), PC Chair
  • Thomas Studer (University of Bern, Switzerland)
  • Tarmo Uustalu (Reykjavik University, Iceland)
  • Yde Venema (University of Amsterdam, Netherland)

Steering committee of the FICS workshop series

  • Bahareh Afshari (University of Gothenburg)
  • Denis Kuperberg (CNRS & ENS Lyon)
  • Ralph Matthes (IRIT, CNRS & Université de Toulouse), chair of the steering committee
  • Damian Niwinski (University of Warsaw)
  • Luigi Santocanale (LIS, Université Aix-Marseille)
  • Alexis Saurin (IRIF, CNRS & Université Paris Cité & INRIA)
  • Tarmo Uustalu (Reykjavik University)
  • Igor Walukiewicz (LaBRI, Bordeaux)

FICS history