{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T10:14:10Z","timestamp":1783764850817,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540191292","type":"print"},{"value":"9783540391265","type":"electronic"}],"license":[{"start":{"date-parts":[[1988,1,1]],"date-time":"1988-01-01T00:00:00Z","timestamp":567993600000},"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":[[1988]]},"DOI":"10.1007\/3-540-19129-1_2","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:03:46Z","timestamp":1330200226000},"page":"45-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Typechecking dependent types and subtypes"],"prefix":"10.1007","author":[{"given":"Luca","family":"Cardelli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"3","key":"2_CR1","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1016\/0022-0000(81)90073-8","volume":"23","author":"L. Aiello","year":"1981","unstructured":"L. Aiello, G. Prini: An Efficient Interpreter for the Lambda-Calculus, Journal of Computer and System Sciences, 23,3 pp. 384\u2013424, 1981.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"R.Burstall, B.Lampson, A kernel language for abstract data types and modules, in Semantics of Data Types, Lecture Notes in Computer Science 173, Springer-Verlag, 1984.","DOI":"10.1007\/3-540-13346-1_1"},{"key":"2_CR3","unstructured":"L.Cardelli, P.Wegner: On understanding types, data abstraction and polymorphism, Technical Report No. CS-85-14, Brown University."},{"key":"2_CR4","unstructured":"L. Cardelli: A polymorphic \u03bb-calculus with Type:Type, Technical Report n.10, DEC Systems Research Center, May 1986."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"T.Coquand, G.Huet: Constructions: a higher order proof system for mechanizing mathematics, Technical report 401, INRIA, May 1985.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"J-Y.Girard: Une extension de l'interpr\u00e9tation de G\u00f6del a l'analyse, et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types, Proceedings of the second Scandinavian logic symposium, J.E.Fenstad Ed. pp. 63\u201392, North-Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"2_CR7","unstructured":"R.Harper, F.Honsell, G.Plotkin, A framework for defining logics, Proc. Symposium on Logic in Computer Science, Ithaca NY, June 22\u201325 1987, IEEE Computer Society Press, 1987."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"P.Martin-L\u00f6f, An intuitionistic theory of types: predicative part, in Logic Colloquium III, F.Rose, J.Sheperdson ed. pp 73\u2013118, North-Holland, 1973.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"2_CR9","unstructured":"P.Martin-L\u00f6f, The type structure of intuitionistic type theory, lecture at the workshop on Foundations of Logic and Functional Programming, Trento, Italy, Dec. 1986."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner: A theory of type polymorphism in programming, Journal of Computer and System Science 17, pp. 348\u2013375, 1978.","journal-title":"Journal of Computer and System Science"},{"key":"2_CR11","first-page":"184","volume-title":"Proc. Symposium on Lisp and Functional Programming","author":"R. Milner","year":"1984","unstructured":"R. Milner: A proposal for Standard ML, Proc. Symposium on Lisp and Functional Programming, Austin, Texas, August 6\u20138 1984, pp. 184\u2013197. ACM, New York."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"J.C.Mitchell, G.D. Plotkin: Abstract types have existential type, Proc. POPL 1985.","DOI":"10.1145\/318593.318606"},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-15198-2_7","volume-title":"Mathematical Foundations of Software Development","author":"J.C. Reynolds","year":"1985","unstructured":"J.C. Reynolds: Three approaches to type structure; Mathematical Foundations of Software Development, Lecture Notes in Computer Science 185, Springer-Verlag, Berlin 1985, pp. 97\u2013138."}],"container-title":["Lecture Notes in Computer Science","Foundations of Logic and Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19129-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:36:40Z","timestamp":1558269400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19129-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540191292","9783540391265"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-19129-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}