The duality of computationReportar como inadecuado

The duality of computation - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 COQ - Formal Specifications and Program Validation Inria Paris-Rocquencourt 2 PPS - Preuves, Programmes et Systèmes

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.

Keywords : call-by-name call-by-value sequent calculus CPS-translations Curry-Howard-de Bruijn proof-as-program correspondence duality lambda-calculus

Autor: Hugo Herbelin - Pierre-Louis Curien -



Documentos relacionados