{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:16:36Z","timestamp":1759637796945},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_73","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:47:00Z","timestamp":1330210020000},"page":"750-770","source":"Crossref","is-referenced-by-count":29,"title":["An extension of system F with subtyping"],"prefix":"10.1007","author":[{"given":"Luca","family":"Cardelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simone","family":"Martini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John C.","family":"Mitchell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andre","family":"Scedrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"36_CR1","unstructured":"S. Abramsky, J.C. Mitchell, A.Scedrov, P.Wadler: Relators, to appear."},{"key":"36_CR2","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. B\u00f6hm","year":"1985","unstructured":"C. B\u00f6hm, A. Berarducci: Automatic synthesis of typed \u03bb-programs on term algebras, Theoretical Computer Science, 39, pp. 135\u2013154, 1985.","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"36_CR3","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"E.S. Bainbridge","year":"1990","unstructured":"E.S. Bainbridge, P.J. Freyd, A. Scedrov, P.J. Scott: Functorial polymorphism, Theoretical Computer Science, vol.70, no.1, pp 35\u201364, 1990.","journal-title":"Theoretical Computer Science"},{"issue":"1\/2","key":"36_CR4","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0890-5401(90)90062-M","volume":"87","author":"K.B. Bruce","year":"1990","unstructured":"K.B. Bruce, G. Longo: A modest model of records, inheritance and bounded quantification, Information and Computation, 87(1\/2):196\u2013240, 1990.","journal-title":"Information and Computation"},{"key":"36_CR5","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1016\/0890-5401(88)90007-7","volume":"76","author":"L. Cardelli","year":"1988","unstructured":"L. Cardelli: A semantics of multiple inheritance, in Information and Computation 76, pp 138\u2013164, 1988.","journal-title":"Information and Computation"},{"key":"36_CR6","unstructured":"L.Cardelli: Extensible records in a pure calculus of subtyping, to appear."},{"key":"36_CR7","doi-asserted-by":"crossref","unstructured":"L.Cardelli, G.Longo: A semantic basis for Quest, Proceedings of the 6th ACM LISP and Functional Programming Conference, ACM Press, 1990.","DOI":"10.1145\/91556.91586"},{"key":"36_CR8","doi-asserted-by":"crossref","unstructured":"L.Cardelli, J.C.Mitchell: Operations on records, Proc. of the Fifth Conference on Mathematical Foundations of Programming Language Semantics, New Orleans, 1989. To appear in Mathematical Structures in Computer Science, 1991.","DOI":"10.1017\/S0960129500000049"},{"issue":"4","key":"36_CR9","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli, P. Wegner: On understanding types, data abstraction and polymorphism, Computing Surveys, Vol 17 n. 4, pp 471\u2013522, December 1985.","journal-title":"Computing Surveys"},{"key":"36_CR10","unstructured":"P.-L.Curien, G.Ghelli: Coherence of subsumption, Mathematical Structures in Computer Science, to appear."},{"key":"36_CR11","unstructured":"P.-L.Curien, G.Ghelli: Subtyping + extensionality: confluence of \u03b2\u03b7-reductions in F \u2264, to appear."},{"issue":"5","key":"36_CR12","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn: Lambda-calculus notation with nameless dummies, in Indag. Math. 34(5), pp. 381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"36_CR13","unstructured":"J.Fairbairn: Some types with inclusion properties in \u2200, \u2192, \u03bc, Technical report No 171, University of Cambridge, Computer Laboratory."},{"key":"36_CR14","unstructured":"P.J.Freyd: Structural polymorphism, to appear in TCS."},{"key":"36_CR15","unstructured":"G.Ghelli: Proof theoretic studies about a mininal type system integrating inclusion and parametric polymorphism, Ph.D. Thesis TD-6\/90, Universit\u00e0 di Pisa, Dipartimento di Informatica, 1990."},{"key":"36_CR16","doi-asserted-by":"crossref","unstructured":"J-Y.Girard: Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 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":"36_CR17","unstructured":"J.Lambek, P.J.Scott: Introduction to higher order categorical logic, Cambridge University Press, 1986."},{"key":"36_CR18","unstructured":"J.C.Mitchell: A type inference approach to reduction properties and semantics of polymorphic expressions, Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley, 1990."},{"key":"36_CR19","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1090\/conm\/092\/1003204","volume":"92","author":"J.C. Mitchell","year":"1989","unstructured":"J.C. Mitchell, P.J. Scott: Typed \u03bb-models and cartesian closed categories, in Categories in Computer Science and Logic, J.W. Gray and A.Scedrov Eds. Contemporary Math. vol. 92, Amer. Math. Soc., pp 301\u2013316, 1989.","journal-title":"Contemporary Math."},{"key":"36_CR20","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1007\/3-540-18508-9_18","volume":"283","author":"A.M. Pitts","year":"1987","unstructured":"A.M. Pitts: Polymorphism is set-theoretic, constructively, in Category Theory and Computer Science, Proceedings Edinburgh 1987, D.H.Pitt, A.Poigne, and D.E.Rydeheard Eds. Springer Lecture Notes in Computer Science, vol. 283, pp 12\u201339, 1987.","journal-title":"Springer Lecture Notes in Computer Science"},{"key":"36_CR21","doi-asserted-by":"crossref","unstructured":"J.C.Reynolds: Towards a theory of type structure, in Colloquium sur la programmation pp. 408\u2013423, Springer-Verlag Lecture Notes in Computer Science, n.19, 1974.","DOI":"10.1007\/3-540-06859-7_148"},{"key":"36_CR22","first-page":"513","volume-title":"Information Processing '83","author":"J.C. Reynolds","year":"1983","unstructured":"J.C. Reynolds: Types, abstraction, and parametric polymorphism, in Information Processing '83, pp 513\u2013523, R.E.A. Mason ed., North Holland, Amsterdam, 1983."},{"key":"36_CR23","doi-asserted-by":"crossref","unstructured":"A.Scedrov: A guide to polymorphic types, in Logic and Computer Science, pp 387\u2013420, P.Odifreddi ed., Academic Press, 1990.","DOI":"10.1007\/BFb0093926"},{"key":"36_CR24","unstructured":"C.Strachey: Fundamental concepts in programming languages, lecture notes for the International Summer School in Computer Programming, Copenhagen, August 1967."},{"key":"36_CR25","doi-asserted-by":"crossref","unstructured":"P.Wadler: Theorems for free!, Proc. of the Fourth International Conference on Fuctional Programming and Computer Architecture, ACM Press, 1989.","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_73.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:54:16Z","timestamp":1605646456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_73"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_73","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}