{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T15:40:25Z","timestamp":1648568425905},"reference-count":13,"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\/bf01995109","type":"journal-article","created":{"date-parts":[[2005,8,10]],"date-time":"2005-08-10T14:40:23Z","timestamp":1123684823000},"page":"70-83","source":"Crossref","is-referenced-by-count":1,"title":["Remarks on Martin-L\u00f6f's partial type theory"],"prefix":"10.1007","volume":"32","author":[{"given":"Erik","family":"Palmgren","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viggo","family":"Stoltenberg-Hansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF01995109_CR1","doi-asserted-by":"crossref","unstructured":"Constable, R. and N. P. Mendler,Recursive definitions in type theory, in:Logics of Programs, Brooklyn 1985, (ed. R. Parikh), Springer Lecture Notes in Computer Science vol. 193, Springer, 1985.","DOI":"10.1007\/3-540-15648-8_5"},{"key":"BF01995109_CR2","unstructured":"Dybjer, P.,Inductively defined sets in Martin-L\u00f6f's set theory, manuscript, 1988."},{"key":"BF01995109_CR3","unstructured":"Griffor, E. R., I. Lindstr\u00f6m and V. Stoltenberg-Hansen,Mathematical Theory of Domains, Cambridge University Press, to appear."},{"key":"BF01995109_CR4","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.,An intuitionistic theory of types: predicative part, in:Logic Colloquium '73, (eds. E. H. Rose, J. C. Shepherdson), North-Holland, 1975, pp. 73\u2013118.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"BF01995109_CR5","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.,Constructive mathematics and computer programming, in:Logic, Methodology and Philosophy of Science VI (eds. L. J. Cohen, et al.), North-Holland, 1982, pp. 153\u2013175.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"BF01995109_CR6","unstructured":"Martin-L\u00f6f, P.,The domain interpretation of type theory, in:Workshop on Semantics of Programming Languages, Abstracts and Notes (eds. K. Karlsson and K. Petterson), Programing Methodology Group, Chalmer's University of Technology and University of G\u00f6teborg, 1983."},{"key":"BF01995109_CR7","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.,Mathematics of infinity, in: Proceedings of the COLOG 88 conference, Tallinn (eds. P. Martin-L\u00f6f and G. E. Mints), Springer Lecture Notes in Computer Science, Springer 1989.","DOI":"10.1007\/3-540-52335-9"},{"key":"BF01995109_CR8","unstructured":"Nordstr\u00f6m, B., K. Petterson and J. M. Smith,Programming in Martin-L\u00f6f's Type Theory. An Introduction, Oxford University Press, 1990."},{"key":"BF01995109_CR9","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0168-0072(90)90044-3","volume":"48","author":"E. Palmgren","year":"1990","unstructured":"Palmgren, E. and V. Stoltenberg-Hansen,Domain interpretations of Martin-L\u00f6f's partial type theory, Annals of Pure and Applied Logic 48 (1990), pp. 135\u2013196.","journal-title":"Annals of Pure and Applied Logic"},{"key":"BF01995109_CR10","doi-asserted-by":"crossref","unstructured":"Palmgren, E.,An information system interpretation of Martin-L\u00f6f's partial type theory with universes, Information and Computation, to appear.","DOI":"10.1006\/inco.1993.1048"},{"key":"BF01995109_CR11","unstructured":"Palmgren, E.,A construction of Type: Type in Martin-L\u00f6f's partial type theory with one universe, Journal of Symbolic Logic, to appear."},{"key":"BF01995109_CR12","unstructured":"Palmgren, E. and V. Stoltenberg-Hansen,Martin-L\u00f6f's partial type theory, U.U.D.M. Report 1990: 3, Uppsala, 1990."},{"key":"BF01995109_CR13","doi-asserted-by":"crossref","first-page":"840","DOI":"10.2307\/2274575","volume":"53","author":"J. M. Smith","year":"1988","unstructured":"Smith, J. M.,The independence of Peano's fourth axiom from Martin-L\u00f6f's type theory without universes, Journal of Symbolic Logic 53 (1988), pp. 840\u2013845.","journal-title":"Journal of Symbolic Logic"}],"container-title":["BIT"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995109.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01995109\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01995109","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T20:25:40Z","timestamp":1586377540000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01995109"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["BF01995109"],"URL":"https:\/\/doi.org\/10.1007\/bf01995109","relation":{},"ISSN":["0006-3835","1572-9125"],"issn-type":[{"value":"0006-3835","type":"print"},{"value":"1572-9125","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,3]]}}}