{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:36Z","timestamp":1749124056953},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590484"},{"type":"electronic","value":"9783540491781"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014056","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T02:50:31Z","timestamp":1132714231000},"page":"235-248","source":"Crossref","is-referenced-by-count":2,"title":["Untyped \u03bb-calculus with relative typing"],"prefix":"10.1007","author":[{"given":"M. Randall","family":"Holmes","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"unstructured":"Boffa, M. \u201cZFJ and the consistency problem for NF\u201d, in Jahrbuch der Kurt G\u00f6del Gesellschaft, 1988, pp. 102\u20136.","key":"16_CR1"},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1305\/ndjfl\/1093636013","volume":"33","author":"M. Crabb\u00e9","year":"1992","unstructured":"Crabb\u00e9, M. On NFU. Notre Dame Journal of Formal Logic, vol. 33 (1992), pp. 112\u2013119.","journal-title":"On NFU. Notre Dame Journal of Formal Logic"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1016\/0304-3975(93)90014-K","volume":"110","author":"T. E. Forster","year":"1993","unstructured":"Forster, T. E. \u201cA semantic characterization of the well-typed formulae of \u03bb-calculus\u201d. Theoretical Computer Science, vol. 110 (1993), pp. 405\u2013418.","journal-title":"Theoretical Computer Science"},{"key":"16_CR4","volume-title":"Oxford logic guides no. 20","author":"T. E. Forster","year":"1992","unstructured":"Forster, T. E. Set theory with a universal set, Oxford logic guides no. 20. Clarendon Press, Oxford, 1992."},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2267307","volume":"9","author":"T. Hailperin","year":"1944","unstructured":"Hailperin, T. \u201cA set of axioms for logic\u201d. Journal of Symbolic Logic, vol. 9 (1944), pp. 1\u201319.","journal-title":"Journal of Symbolic Logic"},{"key":"16_CR6","volume-title":"Ph.D. thesis","author":"M. R. Holmes","year":"1990","unstructured":"Holmes, M. R. \u201cSystems of combinatory logic related to Quine's \u2018New Foundations'\u201d, Ph.D. thesis, State University of New York at Binghamton, 1990."},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0168-0072(91)90052-N","volume":"53","author":"M. R. Holmes","year":"1991","unstructured":"Holmes, M. R. \u201cSystems of combinatory logic related to Quine's \u2018New Foundations'\u201d. Annals of Pure and Applied Logic, vol. 53 (1991), pp. 103\u2013133.","journal-title":"Annals of Pure and Applied Logic"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0168-0072(93)90230-B","volume":"59","author":"M. R. Holmes","year":"1993","unstructured":"Holmes, M. R. \u201cSystems of combinatory logic related to predicative and \u2018mildly impredicative\u2019 fragments of Quine's \u2018New Foundations'\u201d. Annals of Pure and Applied Logic, vol. 59 (1993), pp. 45\u201353.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"no.1","key":"16_CR9","first-page":"1","volume":"4","author":"M. R. Holmes","year":"1994","unstructured":"Holmes, M. R. \u201cThe set-theoretical program of Quine succeeded, but nobody noticed\u201d. Modern Logic, vol. 4, no. 1 (1994), pp. 1\u201347.","journal-title":"Modern Logic"},{"unstructured":"Holmes, M. R. \u201cStrong axioms of infinity in NFU\u201d, preprint.","key":"16_CR10"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/BF00568059","volume":"19","author":"R. B. Jensen","year":"1969","unstructured":"Jensen, R. B. \u201cOn the consistency of a slight (?) modification of Quine's NF\u201d. Synthese, vol. 19 (1969), pp. 250\u201363.","journal-title":"Synthese"},{"key":"16_CR12","volume-title":"Logic for Mathematicians","author":"J. B. Rosser","year":"1978","unstructured":"Rosser, J. B. Logic for Mathematicians. McGraw-Hill, reprinted (with appendices) by Chelsea, New York, 1978."},{"doi-asserted-by":"crossref","unstructured":"Scott, Dana. \u201cContinuous lattices\u201d, in Springer Lecture Notes in Mathematics, no. 274, pp. 97\u2013136.","key":"16_CR13","DOI":"10.1007\/BFb0073967"},{"key":"16_CR14","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1093\/mind\/LXI.243.366","volume":"61","author":"H. Wang","year":"1952","unstructured":"Wang, H. \u201cNegative types\u201d. Mind, vol. 61 (1952), pp. 366\u20138.","journal-title":"Mind"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T00:37:34Z","timestamp":1586565454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0014056","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}