The paradox of trees in type theory |
| |
| Authors: | Thierry Coquand |
| |
| Affiliation: | (1) INRIA, Domaine de Voluceau-Rocquencourt, B.P. 105, 78153 Le Chesnay-Cedex, France;(2) University of Göteborg/Chalmers, S-41296 Göteborg, Sweden |
| |
| Abstract: | We show how to represent a paradox similar to Russell's paradox in Type Theory withW-types and a type of all types, and how to use this in order to represent a fixed-point operator in such a theory. It is still open whether such a construction is possible without theW-type.This research was partly supported by ESPIRIT Basic Research Action  Logical Frameworks . |
| |
| Keywords: | D.2.1 D.2.4 D.3.1 F.3.1 F.3.3 |
| 本文献已被 SpringerLink 等数据库收录！ |
|
