Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order
View / Open Files
Publication Date
2019Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name
ESOP 2019
ISSN
0302-9743
ISBN
9783030171834
Publisher
Springer International Publishing
Volume
11423 LNCS
Pages
235-262
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
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
Abstract
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.
Sponsorship
EPSRC (1789520)
Identifiers
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
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.