Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory
Call-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) CBPV, define a simple equational theory, and verify adequacy for the standard set/algebra denotational semantics. Furthermore, we prove normalisation of the standard reduction, confluence of strong reduction, strong normalisation using Kripke logical relations, and soundness of the equational theory using logical equivalence. We adapt and verify the known translations from CBV and CBN into CBPV for strong reduction. This yields, for instance, proofs of strong normalisation and confluence for the full lambda-calculus with sums and products. Thanks to the automation provided by Coq and the Autosubst 2 framework, there is little formalisation overhead compared to detailed paper proofs.
Mon 14 Jan
|11:00 - 11:30|
Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MilerINRIA Saclay and LIXDOI
|11:30 - 12:00|
Yannick ForsterSaarland University, Steven SchäferSaarland University, Simon SpiesSaarland University, Kathrin StarkSaarland University, GermanyDOI
|12:00 - 12:30|