λμ-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.
Type de document :
Pré-publication, Document de travail
2009
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00524942
Contributeur : Hugo Herbelin <>
Soumis le : vendredi 29 octobre 2010 - 11:00:17
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 12:41:04

Fichier

apal-HerSau10-lambda-mu-Lambda...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00524942, version 1

Collections

INRIA | PPS | USPC

Citation

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

Partager

Métriques

Consultations de la notice

285

Téléchargements de fichiers

136