@inproceedings{4e935feea34345ed863b63c57104af61,
title = "Untyped λ-calculus with relative typing",
abstract = "A system of untyped λ-calculus with a restriction on function abstraction using relative typing analogous to the restriction on set comprehension found in Quine's set theory “New Foundations” is discussed. The author has shown elsewhere that this system is equiconsistent with Jensen{\textquoteright}s NFU (“New Foundations” with urelements) + Infinity, which is in turn equiconsistent with the simple theory of types with infinity. The definition of the system is given and the construction of a model is described. A semantic motivation for the stratification criterion for function abstraction is given, based on an abstract model of computation. The same line of semantic argument is used to motivate an analogy between the notion of “strongly Cantorian set” found in “New Foundations” and the notion of “data type”; an implementation of absolute types as domains of retractions with strongly Cantorian ranges is described. The implementation of these concepts in a theorem prover developed by the author is sketched.",
author = "Holmes, {M. Randall}",
note = "Publisher Copyright: {\textcopyright} Springer-Vedag Berlin Heidelberg 1995.; 2nd International Conference on Typed Lambda Calculi and Applications, TLCA 1995 ; Conference date: 10-04-1995 Through 12-04-1995",
year = "1995",
doi = "10.1007/bfb0014056",
language = "English",
isbn = "354059048X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "235--248",
editor = "Mariangiola Dezani-Ciancaglini and Gordon Plotkin",
booktitle = "Typed Lambda Calculi and Applications - 2nd International Conference on Typed Lambda Calculi and Applications, TLCA 1995, Proceedings",
address = "Germany",
}