Call-By-Name Is Just Call-By-Value with Delimited Control
Mateusz Pyzik

TL;DR
This paper introduces a lambda calculus extended with delimited control operators, demonstrating it can express both lambda calculus and effects, bridging call-by-name and call-by-value paradigms through a novel reduction theory.
Contribution
It presents a new lambda calculus with shift0 and control delimiter, showing it can embed lambda calculus with beta and eta reductions and unify various calculi.
Findings
Delimited control operators can express lambda calculus and effects
The calculus $\Lambda_\$ $ can embed lambda calculus with beta and eta reductions
Call-by-name can simulate call-by-value with delimited control
Abstract
Delimited control operator shift0 exhibits versatile capabilities: it can express layered monadic effects, or equivalently, algebraic effects. Little did we know it can express lambda calculus too! We present \Lambda_\ $ \Lambda_$ $ \Lambda\mu_v \lambda_$ \Lambda_$ \lambda $ all correspond…
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 · Security and Verification in Computing · Formal Methods in Verification
