This talk explores different quantitative properties of Call-by-Name (CBN) and Call-by-Value (CBV) that are inherited from the corresponding properties of Call-by-Push-Value (CBPV).
More precisely, we first present an untyped CBPV-like calculus, called lambda-bang, which encodes untyped CNB and CBV, both from a static and a dynamic point of view. We then explore these same encodings, but in a typed framework, specified by quantitative (aka non-idempotent intersection) types. Three different quantitative properties are discussed in this setting. In all the cases, explained and discussed in the talk, the quantitative property for CBN/CBV is inherited from the corresponding property in the unified general framework provided by the typed lambda-bang calculus.
Program Display Configuration
Tue 13 Sep
Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Praguechange