Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

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

CPP-2019
11:00 - 12:30: CPP 2019 - Research Papers: Proof Theory, Theory of Programming Languages at Sala XII
Chair(s): Assia MahboubiINRIA
CPP-201911:00 - 11:30
Research paper
Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MilerINRIA Saclay and LIX
DOI
CPP-201911:30 - 12:00
Research paper
Yannick ForsterSaarland University, Steven SchäferSaarland University, Simon SpiesSaarland University, Kathrin StarkSaarland University, Germany
DOI
CPP-201912:00 - 12:30
Research paper
Theo WinterhalterGallinette / Inria / LS2N, Nicolas TabareauInria, Matthieu SozeauInria
DOI