Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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

Hugo Herbelin 1, 2 Alexis Saurin 3 
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download
Contributor : Hugo Herbelin Connect in order to contact the contributor
Submitted on : Friday, October 29, 2010 - 11:00:17 AM
Last modification on : Monday, February 7, 2022 - 4:06:03 PM
Long-term archiving on: : Friday, October 26, 2012 - 12:41:04 PM


Files produced by the author(s)


  • HAL Id : inria-00524942, version 1



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



Record views


Files downloads