Évènement

Adrienne Lancelot
Università di Bologna
https://www.irif.fr/users/lancelot/index

Date(s) : 21/05/2026   iCal
11h00 - 12h30

The study of program preorders leads to more structure than that of program
equivalences. Is it actually interesting in the case of the uneffectful
lambda-calculus? I will explain why order properties are relevant, as they may
reformulate cornerstone results, such as the genericity lemma. The genericity
lemma, indeed, states the existence of minimum lambda-terms for a contextual
preorder. One can dualize this lemma to a co-genericity principle, discussing
maximum terms. Maximum terms may feel intriguing, but in a distributed setting
they represent a happy client, which can no longer be used by a context in any
other way than being happy.

I will discuss contextual preorders, genericity and co-genericity principles,
in both call-by-name and call-by-value. The application of these principles
leads to a proof of the naturality of contextual equivalence (or its preorder
variant) by giving sufficient conditions for it to be maximal amongst
(in)equational theories. The results about call-by-name are formalized in the
Abella proof assistant.
The end of the talk will hopefully mention open questions and future work on
the topic.

Based on: Light Genericity FoSSaCS 2024
[https://link.springer.com/chapter/10.1007/978-3-031-57231-9_2], Barendregt’s
Theory of the lambda-calculus, Refreshed and Formalized ITP 2025
[https://doi.org/10.4230/LIPIcs.ITP.2025.13] and my PhD thesis 2025
[https://theses.hal.science/tel-05407883]

Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)

Catégories

• Séminaire