Continuation-Passing Style, Defunctionalization, Accumulations, and Associativity
Jeremy Gibbons (University of Oxford, UK)

TL;DR
This paper explores how continuation-passing style and defunctionalization techniques rely on the algebraic property of associativity, clarifying their applications through program transformations and data refinements.
Contribution
It highlights the role of associativity in continuation-passing style and defunctionalization, providing a clearer understanding of their applicability and limitations.
Findings
Associativity underpins many programming transformations.
Revisiting classic programs shows dependence on associativity.
Transformations justified by equational reasoning clarify technique applicability.
Abstract
Context: Reynolds showed us how to use continuation-passing style and defunctionalization to transform a recursive interpreter for a language into an abstract machine for programs in that language. The same techniques explain other programming tricks, including zippers and accumulating parameters. Inquiry: Buried within all those applications there is usually a hidden appeal to the algebraic property of associativity. Approach: Our purpose in this paper is to entice associativity out of the shadows and into the limelight. Knowledge: We revisit some well-known applications (factorial, fast reverse, tree flattening, and a compiler for a simple expression language) to spotlight their dependence on associativity. Grounding: We replay developments of these programs through a series of program transformations and data refinements, justified by equational reasoning. Importance: Understanding…
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.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Formal Methods in Verification
