Lambda-Calculus, Combinators and the Comprehension Scheme

Abstract : The presentations of type theory based on a comprehension scheme and on $\lambda$-calculus are equivalent, both in the sense that the latter is a conservative extension of the former and that it can be encoded into it preserving provability. A similar result holds for set theory. A short version of this paper appeared in the proceedings of the conference {\it Typed Lambda-calculi and Applications (1995)}.}
Type de document :
Rapport
[Research Report] RR-2565, INRIA. 1995
Liste complète des métadonnées

https://hal.inria.fr/inria-00074116
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:33:19
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : lundi 5 avril 2010 - 00:05:25

Fichiers

Identifiants

  • HAL Id : inria-00074116, version 1

Collections

Citation

Gilles Dowek. Lambda-Calculus, Combinators and the Comprehension Scheme. [Research Report] RR-2565, INRIA. 1995. 〈inria-00074116〉

Partager

Métriques

Consultations de la notice

169

Téléchargements de fichiers

118