Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Springer International Publishing
MetadataShow full item record
McDermott, D., & Mycroft, A. (2019). Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11423 LNCS 235-262. https://doi.org/10.1007/978-3-030-17184-1_9
Traditionally, reasoning about programs under varying evaluation regimes (call-by-value, call-by-name etc.) was done at the meta-level, treating them as term rewriting systems. Levy’s call-by-push-value (CBPV) calculus provides a more powerful approach for reasoning, by treating CBPV terms as a common intermediate language which captures both call-by-value and call-by-name, and by allowing equational reasoning about changes to evaluation order between or within programs. We extend CBPV to additionally deal with call-by-need, which is non-trivial because of shared reductions. This allows the equational reasoning to also support call-by-need. As an example, we then prove that call-by-need and call-by-name are equivalent if nontermination is the only side-effect in the source language. We then show how to incorporate an effect system. This enables us to exploit static knowledge of the potential effects of a given expression to augment equational reasoning; thus a program fragment might be invariant under change of evaluation regime only because of knowledge of its effects.
External DOI: https://doi.org/10.1007/978-3-030-17184-1_9
This record's URL: https://www.repository.cam.ac.uk/handle/1810/289870