λμ-calculus and duality: Call-by-name and call-by-value

Abstract

Under the extension of Curry-Howard's correspondence to classical logic, Gentzen's NK and LK systems can be seen as syntaxdirected systems of simple types respectively for Parigot's λμ-calculus and Curien-Herbelin's λ̄μμ̃-calculus. We aim at showing their computational equivalence. We define translations between these calculi. We prove simulation theorems for an undirected evaluation as well as for call-by-name and call-by-value evaluations. © Springer-Verlag Berlin Heidelberg 2005.