{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:25:46Z","timestamp":1746001546542},"reference-count":8,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["BIT"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1007\/bf01995104","type":"journal-article","created":{"date-parts":[[2005,8,10]],"date-time":"2005-08-10T14:40:23Z","timestamp":1123684823000},"page":"10-14","source":"Crossref","is-referenced-by-count":5,"title":["The paradox of trees in type theory"],"prefix":"10.1007","volume":"32","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"BF01995104_CR1","unstructured":"Martin-L\u00f6f, P.,Intuitionistic Type Theory, Bibliopolis, 1984."},{"key":"BF01995104_CR2","unstructured":"Palmgren, E.,A construction of Type: Type in Martin-L\u00f6f's partial type theory with one universe, Unpublished manuscript."},{"key":"BF01995104_CR3","unstructured":"Palmgren, E. and Stoltenberg-Hansen, V.,Domain Interpretations of Intuitionistic Type Theory, Uppsala University. U.U.D. Report 1989: 1."},{"key":"BF01995104_CR4","doi-asserted-by":"crossref","unstructured":"Aczel, P.,The type theoretic interpretation of constructive set theory, Logic Colloquium '77 (1978), 55\u201366, A. Macintyre et al., editors.","DOI":"10.1016\/S0049-237X(08)71989-X"},{"key":"BF01995104_CR5","doi-asserted-by":"crossref","unstructured":"Meyer, A. and Reinhold, M. B.,\u201cType\u201d is not a type, Principles of Programming language, ACM, 1986.","DOI":"10.1145\/512644.512671"},{"key":"BF01995104_CR6","unstructured":"Howe, D.,The Computational Behaviour of Girard's Paradox, Symposium on Logic in Computer Science, Ithaca, New York, 1987."},{"key":"BF01995104_CR7","unstructured":"Hayashi, S. and Nakano, H.,Communication in the TYPES electronic forum (August 7, 1987), types theory. lcs. mit. edu."},{"key":"BF01995104_CR8","unstructured":"Girard, J. Y.,Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieure, Th\u00e8se d'Etat, Paris VII, 1972."}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995104.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01995104\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995104","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T20:25:00Z","timestamp":1586377500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01995104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":8,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01995104"],"URL":"https:\/\/doi.org\/10.1007\/bf01995104","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}