Rencontre, 17 September 2026

Programme

10:30 – 11:45
Thibaut Balabonski (LMF, Univ. Paris Saclay)
Invited talk: Lambda-calculus as a model of complexity

Complexity theory refines computability theory by characterizing classes of algorithmic problems that can be solved under some time or memory constraints. Such classes are for instance PTIME (problems solvable in a polynomial number of elementary steps with respect to the size of the input) or LOGSPACE (problems solvable with memory usage logarithmic in the size of the input).

From its inception in the 1960s, complexity theory has generally been studied through Turing or RAM machines. Indeed, while the λ-calculus is historically recognized as a model of computation, equivalent to Turing and other machines, its relevance for the study of complexity has long been unclear. Its central operation, β-reduction, seems at first sight too rich and complex to be considered as an appropriate, atomic unit of computation. Yet, starting in the 1990s it became progressively known that the natural complexity measures (number of β-reductions for time, size of terms for space) were actually ‘’reasonable’’ measures, defining the same complexity classes as the Turing standard.

In this talk I will address two of the problems that remain in a λ-calculus-based theory of algorithmic complexity.

  • The simple notion of space complexity based on the size of terms cannot measure any sublinear space, meaning it is adequate for characterizing PSPACE but not LOGSPACE. I will propose a refined —but still simple and natural— definition of space complexity for the λ-calculus solving this issue.
  • Many implementations of the λ-calculus are adequate either for time or for space, but not for both simultaneously. I will present an implementation model reconciling these two aspects.
13:45 – 14:45
Louise Leclerc (Institut Polytechnique de Paris)
Invited talk: A bunched approach to directed HoTT

The last two decades have seen the emergence of "homotopy" type theory (HoTT), in which intensional identity types can be interpreted as the space of paths connecting two points of a type. This new interpretation allows types in HoTT to be viewed as spaces up to homotopy, thereby providing a synthetic language well-suited to formalizing results specific to homotopy theory or to drawing parallels between mathematical logic and that field. More recently, we have seen the emergence of a variant of HoTT that allows us to work with a notion of "directed" spaces, up to homotopy — think of how directed graphs relate to undirected graphs. Within this setting, there is a concept of (directed) path types between two points of a given type, which in turn cannot yet be a directed space. We will explore an idea to remedy this shortcoming and enable the study of a higher version of directedness, where path types of directed types can themselves be directed (omega-groupoids). We will see along the way why it may be useful to consider an extension of the syntax where two kinds of context extensions coexist, akin to the Cartesian and linear pairing of contexts appearing in linear logic. The n​ew pairing operation is being thought about as the Gray tensor product of categories, and its adjoints are to be interpreted as the categories of functors together with lax (resp. oplax) transformations. Such a system is known as "bunched logic" or "bunched type theory". We will present a draft version of its rules and simple examples of its usefulness, for instance, in order to define the directed path type of a type.

15:15 – 16:15
Paul Brunet (LACL, Créteil)
Invited talk: Representations & beyond

In this talk I will show how techniques from relation algebra can be used to discuss various properties of model-checking problems. Such problems will be viewed as arbitrary binary relations, between an abstract set of models, and one of specifications. In particular I will discuss expressivity (are there enough specifications to describe each model) and axiomatisability (can we reason about models using specifications). I will also investigate notions of reductions between problems. This is ongoing work, building on my RAMICS 2026 paper as well as joint work with Uli Fahrenberg (LMF).