Galois connecting call-by-value and call-by-name
Dylan McDermott, Alan Mycroft

TL;DR
This paper develops a general framework using Levy's call-by-push-value calculus to relate call-by-value and call-by-name semantics, especially in the presence of computational effects, establishing conditions for their observable equivalence and Galois connections.
Contribution
It introduces a novel technique for reasoning about the relationship between call-by-value and call-by-name, leveraging call-by-push-value to analyze effects and establish Galois connections.
Findings
Identifies conditions under which call-by-value and call-by-name have related observable behaviors.
Shows that certain effects like divergence satisfy the Galois connection properties.
Demonstrates the applicability of the framework to effects such as nondeterminism.
Abstract
We establish a general framework for reasoning about the relationship between call-by-value and call-by-name. In languages with computational effects, call-by-value and call-by-name executions of programs often have different, but related, observable behaviours. For example, if a program might diverge but otherwise has no effects, then whenever it terminates under call-by-value, it terminates with the same result under call-by-name. We propose a technique for stating and proving properties like these. The key ingredient is Levy's call-by-push-value calculus, which we use as a framework for reasoning about evaluation orders. We show that the call-by-value and call-by-name translations of expressions into call-by-push-value have related observable behaviour under certain conditions on computational effects, which we identify. We then use this fact to construct maps between the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
