{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:45Z","timestamp":1725664005858},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540555117"},{"type":"electronic","value":"9783540471943"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55511-0_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T05:09:36Z","timestamp":1330232976000},"page":"125-143","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Primitive recursive functional with dependent types"],"prefix":"10.1007","author":[{"given":"Neal","family":"Nelson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, pages 207\u2013212. ACM, January 1982.","DOI":"10.1145\/582153.582176"},{"key":"6_CR2","first-page":"29","volume":"146","author":"R. Hindley","year":"1969","unstructured":"R. Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29\u201360, December 1969.","journal-title":"Transactions of the American Mathematical Society"},{"key":"6_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","volume":"22","author":"R. Hindley","year":"1983","unstructured":"R. Hindley. The completeness theorem for typing lambda terms. Theoretical Computer Science, 22:1\u201317, January 1983.","journal-title":"Theoretical Computer Science"},{"key":"6_CR4","unstructured":"Per Martin-L\u00f6f. Infinite terms and a system of natural deduction. In Compositio Mathematical pages 93\u2013103. Wolters-Noordhoof, 1972."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium '73, pages 73\u2013118. North Holland, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"Albert R. R. Meyer","year":"1982","unstructured":"Albert R. Meyer. What is a model of the lambda calculus? Information and Control, 52:87\u2013122, 1982.","journal-title":"Information and Control"},{"key":"6_CR7","volume-title":"Programming in Martin-L\u00f6f's Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f's Type Theory. Oxford University Press, New York, NY, 1990."},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Atsushi Ohori. A simple semantics for ML polymorphism. In Functional Programming and Computer Architecture, 1989.","DOI":"10.1145\/99370.99393"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"W. W. Tait. Infinitely long terms of transfinite type. In Crossley and Dummett, editors, Formal Systems and Recursive Functions, pages 177\u2013185. North Holland, 1965.","DOI":"10.1016\/S0049-237X(08)71689-6"},{"key":"6_CR10","unstructured":"David A. Turner. Sasl language manual. Technical report, University of St. Andrews, 1976."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Programming Semantics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55511-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:35:48Z","timestamp":1558254948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55511-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540555117","9783540471943"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-55511-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]},"assertion":[{"value":"30 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}