TL;DR
Continuation calculus (CC) is a deterministic, head-reduction-based model of computation designed to effectively model control features in programs, allowing for program definition, specification, and correctness proofs.
Contribution
This paper introduces continuation calculus, a new deterministic model that handles control constructs without modifying lambda calculus, supporting both call-by-name and call-by-value evaluation strategies.
Findings
CC can model programs with control operators effectively.
A list multiplication program in CC demonstrates correctness and termination.
CC supports flexible evaluation strategies, including call-by-name and call-by-value.
Abstract
Programs with control are usually modeled using lambda calculus extended with control operators. Instead of modifying lambda calculus, we consider a different model of computation. We introduce continuation calculus, or CC, a deterministic model of computation that is evaluated using only head reduction, and argue that it is suitable for modeling programs with control. It is demonstrated how to define programs, specify them, and prove them correct. This is shown in detail by presenting in CC a list multiplication program that prematurely returns when it encounters a zero. The correctness proof includes termination of the program. In continuation calculus we can model both call-by-name and call-by-value. In addition, call-by-name functions can be applied to call-by-value results, and conversely.
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.