Paul Blain Levy (University of Birmingham), Call-by-push-value: the fine-grained structure of call-by-value and call-by-name


  • Feb. 17, 2012, 15:00 - 15:45


Call-by-push-value is a calculus of computational effects that emerges, quite automatically, from an experiment: take simply typed lambda-calculus with either call-by-value (CBV) or call-by-name (CBN) operational semantics, and add a variety of effects. Construct denotational semantics for each of the resulting languages, and see what correspondences exist between the various models. Then make the corresponding pieces into the primitives of a new language.

By this method, we firstly see that CBV has a decomposition into a "fine-grained CBV" calculus with primitives for returning and sequencing. Secondly, CBN and fine-grained CBV each have a decomposition into another calculus, viz. call-by-push-value.