HackerPapers

arXiv:1309.1257cs.LO

Continuation calculus

Bram Geron, Herman Geuvers

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
In Proceedings COS 2013, arXiv:1309.0924
Journal reference
EPTCS 127, 2013, pp. 66-85
DOI
doi:10.4204/EPTCS.127.5
Subjects
cs.LOLogic in Computer Science cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Apr 2024 to Apr 2024.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. The Essence of Compiling with Continuations (1993) [pdf] 1 comment

    • The problem with typing continuations -in my opinion - stems from the fact that nearly all discussion of continuation starts from a functional context/view/programming language and often also in an untyped language/formalism. Additionally, CPS ends with "style" suggesting that…

      k_g_b_View on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.