Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unifying Framework
This talk explores how the (untyped and typed) theories of Call-by-Name (CBN)and Call-by-Value (CBV) can be unified in a more general framework provided by a Call-by-Push-Value (CBPV) like calculus. Indeed, we first present an untyped calculus, called lambda-bang, which encodes untyped CNB and CBV, both from a static and a dynamic point of view. We then explore these encodings in a typed framework, specified by quantitative (aka non-idempotent intersection) types. Three different (quantitative) properties are discussed. The first one is related to upper bounds for reduction lengths, the second one concerns exact measures for reduction lengths and sizes of normal forms, and the last one is about the inhabitation problem. In all these cases, explained and discussed in the talk, the (quantitative) property for CBN/CBV is inherited from the corresponding one in the lambda-bang calculus.
Sun 22 OctDisplayed time zone: Lisbon change
11:00 - 12:30
|Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unifying FrameworkKeynote|
Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France