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 Times are displayed in time zone: Greenwich Mean Time : Belfast change
11:00 - 12:30: Research Papers: Proof Theory, Theory of Programming LanguagesCPP at Sala XII Chair(s): Assia MahboubiINRIA | |||
11:00 - 11:30 Research paper | A Proof-Theoretic Approach to Certifying Skolemization CPP Kaustuv ChaudhuriInria, France, Matteo ManighettiInria & École Polytechnique, Dale MillerINRIA Saclay and LIX DOI | ||
11:30 - 12:00 Research paper | Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory CPP Yannick ForsterSaarland University, Steven SchäferSaarland University, Simon SpiesSaarland University, Kathrin StarkSaarland University, Germany DOI | ||
12:00 - 12:30 Research paper | Eliminating Reflection from Type Theory CPP DOI |