HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information

# Collections, Sets and Types

Abstract : We give a first order formulation of Church's type theory in which types are mere sets. This formulation is obtained by replacing $\lambda$-calculus by a language of combinators (skolemized comprehension scheme), introducing a distinction between propositions and their contents, relativizing quantifiers and at last replacing typing predicates by membership to some sets. The theory obtained this way has both a type theoretical flavor and a set theoretical one. Like set theory, it is a first order theory, and it uses only one notion of collection. Like type theory, it gives an explicit notation for objects, a primitive notion of function and propositions are objects.
Keywords :
Document type :
Reports
Domain :

https://hal.inria.fr/inria-00073982
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 2:13:58 PM
Last modification on : Thursday, February 3, 2022 - 11:17:13 AM
Long-term archiving on: : Monday, April 5, 2010 - 12:03:14 AM

### Identifiers

• HAL Id : inria-00073982, version 1

### Citation

Gilles Dowek. Collections, Sets and Types. [Research Report] RR-2708, INRIA. 1995. ⟨inria-00073982⟩

Record views