HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

The duality of computation

Abstract : We present the lambda-bar-mu-mu-tilde-calculus, a syntax for lambda-calculus + control operators exhibiting symmetries such as program/context and call-by-name/call-by-value. This calculus is derived from implicational Gentzen's sequent calculus LK, a key classical logical system in proof theory. Under the Curry-Howard correspondence between proofs and programs, we can see LK, or more precisely a formulation called LK-mu-mu-tilde, as a syntax-directed system of simple types for lambda-bar-mu-mu-tilde-calculus. For lambda-bar-mu-mu-tilde-calculus, choosing a call-by-name or call-by-value discipline for reduction amounts to choosing one of the two possible symmetric orientations of a critical pair. Our analysis leads us to revisit the question of what is a natural syntax for call-by-value functional computation. We define a translation of lambda-mu-calculus into lambda-bar-mu-mu-tilde-calculus and two dual translations back to lambda-calculus, and we recover known CPS translations by composing these translations.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

Contributor : Hugo Herbelin Connect in order to contact the contributor
Submitted on : Wednesday, June 20, 2007 - 8:31:50 PM
Last modification on : Friday, February 4, 2022 - 3:07:41 AM
Long-term archiving on: : Thursday, April 8, 2010 - 8:57:00 PM


Files produced by the author(s)


  • HAL Id : inria-00156377, version 1



Hugo Herbelin, Pierre-Louis Curien. The duality of computation. Fifth ACM SIGPLAN International Conference on Functional Programming : ICFP '00, Sep 2000, Montréal, Canada. pp.233-243. ⟨inria-00156377⟩



Record views


Files downloads