Giulio Guerrieri
LIS, Aix-Marseille Université
https://www.irif.fr/~giuliog/
Date(s) : 01/12/2022 iCal
11 h 00 min - 12 h 30 min
The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.
L’exposé sera également retransmis ici : https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef
Emplacement
Site Sud, Luminy, Ancienne BU, Salle Séminaire2 (RdC)
Catégories