As Pierre-Louis Curien was visiting, Keiko Nakata took the opportunity to tell us about reduction semantics and λ̄μμ̃-calculus.
Duality of Computation
Hugo Herbelin and Pierre-Louis Curien
ICFP ’00 Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pages 233–243, ACM
Abstract
We present the lambda-bar-mu-mu-tilde, 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. For lambda-bar-mu-mu-tilde, 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 into lambda-bar-mu-mu-tilde and two dual translations back to lambda-calculus, and we recover known CPS translations by composing these translations.
Theory Lunch 