Rencontre, Sept. 17, 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

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).