Sun 22 - Fri 27 October 2023 Cascais, Portugal
Sun 22 Oct 2023 11:00 - 12:30 at Oceanus - Session 2 Chair(s): Santiago Escobar

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 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
Session 2PPDP at Oceanus
Chair(s): Santiago Escobar
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