# 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)}.}
Keywords :
Type de document :
Rapport
[Research Report] RR-2565, INRIA. 1995
Domaine :

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

### Identifiants

• HAL Id : inria-00074116, version 1

### Citation

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

### Métriques

Consultations de la notice

## 170

Téléchargements de fichiers