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)
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