Upcoming paper: The Theory of Call-by-Value Solvability at ICFP 2022
The Theory of Call-by-Value Solvability
The denotational semantics of the untyped $\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 is instead still in its infancy, because of some inherent difficulties but also because call-by-value solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of call-by-value 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 call-by-value, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.
![Beniamino Accattoli](https://icfp22.sigplan.org/getProfileImage/beniaminoaccattoli/7b4a425c-dc5a-422b-82b8-cdb2cfec06d1/micro-avatar.jpg?1650175601000)
Beniamino Accattoli
Inria & Ecole Polytechnique
France
![Giulio Guerrieri](https://icfp22.sigplan.org/getProfileImage/giulioguerrieri/e7978d1f-b1b0-40ae-9ecb-072fa7aff827/micro-avatar.jpg?1618939728000)
Comments are closed
Comments to this thread have been closed by the post author or by an administrator.