Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073982
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 2:13:58 PM
Last modification on : Friday, May 25, 2018 - 12:02:05 PM
Long-term archiving on: : Monday, April 5, 2010 - 12:03:14 AM

Identifiers

  • HAL Id : inria-00073982, version 1

Collections

Citation

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

Share

Metrics

Record views

199

Files downloads

306