λμ-calculus and Λμ-calculus: a Capital Difference

Hugo Herbelin (1, 2) , Alexis Saurin (3)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs
3 UNITO - Università degli studi di Torino = University of Turin

Since Parigot designed the λμ-calculus to algorithmically interpret classical natural deduction, several variants of λμ-calculus have been proposed. Some of these variants derived from an alteration of the original syntax due to de Groote, leading in particular to the Λμ-calculus of the second author, a calculus truly different from λμ-calculus since, in the untyped case, it provides a Böhm separation theorem that the original calculus does not satisfy. In addition to a survey of some aspects of the history of λμ-calculus, we study connections between Parigot's calculus and the modified syntax by means of an additional toplevel continuation. This analysis is twofold: first we relate λμ-calculus and Λμ-calculus in the typed case using λμtp-calculus, which contains a toplevel continuation constant tp, and then we use calculi of the family of λμtp-calculi, containing a toplevel continuation variable tp, to study the untyped setting and in particular relate calculi in the modified syntax.

Mots clés: Classical logic; control operators; delimited control; lambda-calculus

Domaines: Logique en informatique [cs.LO]

Hugo Herbelin, Alexis Saurin. λμ-calculus and Λμ-calculus: a Capital Difference. 2009. ⟨inria-00524942⟩