Charla: "Reasoning about Properties of Call-by-Name and Call-by-Value in a Subsuming Framework"

Expone: Delia Kesner, Université Paris Cité - CNRS - IRIF, France

Abstract: This talk explores how the well-established models of computation given by Call-by-Name (CBN) and Call-by-Value (CBV) can be encoded within a broader setting provided by a unifying framework called the dBang calculus.

We first introduce the dBang calculus, which subsumes (untyped and typed) CBN and CBV, both from a static and a dynamic perspective. We then explore various properties of these computational models, including confluence, factorization, type inhabitation, upper bounds and exact measures for evaluation lengths, meaningfulness and genericity.  In all these cases, explained and discussed in the talk, the properties of CBN and CBV are subsumed/inherited from the corresponding counterparts within the dBang calculus.