{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:20Z","timestamp":1790927600403,"version":"4.1.0"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":6578,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1991,3]]},"abstract":"<jats:p>We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over these operations supports both subtyping and polymorphism. We provide typechecking algorithms and limited semantic models.<\/jats:p><jats:p>Our approach unifies and extends previous notions of records, bounded quantification, record extension, and parametrization by row-variables. The general aim is to provide foundations for concepts found in object-oriented languages, within a framework based on typed lambda-calculus.<\/jats:p>","DOI":"10.1017\/s0960129500000049","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:03:24Z","timestamp":1236157404000},"page":"3-48","source":"Crossref","is-referenced-by-count":62,"title":["Operations on records"],"prefix":"10.1017","volume":"1","author":[{"given":"Luca","family":"Cardelli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John C.","family":"Mitchell","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000049_ref009","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0960129500000049_ref010","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans 1\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de doctorat d\u2019\u00e9tat, University of Paris."},{"key":"S0960129500000049_ref023","volume-title":"Programming Language","author":"Stroustrup","year":"1986"},{"key":"S0960129500000049_ref018","doi-asserted-by":"crossref","unstructured":"Ohori A. , Buneman P. and Breazu-Tannen V. (1988) database programming in Machiavelli \u2013 a polymorphic language with static type inference. Report MS-CIS-88\u2013103, University of Pennsylvania, Computer and Information Science Department.","DOI":"10.1145\/67544.66931"},{"key":"S0960129500000049_ref024","unstructured":"Wand M. (1987) Complete type inference for simple objects. Proc. Second IEEE Symp. on Logic in Computer Science, pp. 37\u201344"},{"key":"S0960129500000049_ref008","doi-asserted-by":"publisher","DOI":"10.1145\/365813.365819"},{"key":"S0960129500000049_ref007","doi-asserted-by":"crossref","unstructured":"Curien P.-L. and Ghelli G. (1991) Coherence of subsumption. Math. Struct. Comp. Sci, to appear.","DOI":"10.1007\/3-540-52590-4_45"},{"key":"S0960129500000049_ref002","doi-asserted-by":"crossref","unstructured":"Bruce K.B. and Longo G. (1988) A modest model of records, inheritance and bounded quantification. Proc. Third IEEE Symp. on Logic in Computer Science, pp. 38\u201350","DOI":"10.1109\/LICS.1988.5099"},{"key":"S0960129500000049_ref016","doi-asserted-by":"crossref","unstructured":"Mitchell J.C. (1986) A type inference approach to reduction properties and semantics of polymorphic expressions. Proc. Symp. on Lisp and Functional Programming, pp. 308\u2013319 (Revised version in Logic Foundations of Functional Programming, ed. G. Huet, Addison-Wesley, 1989, pp. 195\u2013212)","DOI":"10.1145\/319838.319872"},{"key":"S0960129500000049_ref005","unstructured":"Cardelli L. , Donahue J. , Glassman L. , Jordan M. , Kalsow B. and Nelson G. (1989) Modula-3 report (revised). Research Report no. 52, DEC Systems Research Center."},{"key":"S0960129500000049_ref006","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0960129500000049_ref025","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39162"},{"key":"S0960129500000049_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90044-I"},{"key":"S0960129500000049_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90007-7"},{"key":"S0960129500000049_ref020","unstructured":"R\u00e9my D. (1989) Typechecking records and variants in a natural extension of ML. Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 77\u201388"},{"key":"S0960129500000049_ref011","doi-asserted-by":"crossref","unstructured":"Jategaonkar L.A. and Mitchell J.C. (1988) ML with extended pattern matching and subtypes. Proc. ACM Conf. on Lisp and Functional Programming, pp. 198\u2013211","DOI":"10.1145\/62678.62702"},{"key":"S0960129500000049_ref013","volume-title":"Object-oriented Software Construction","author":"Meyer","year":"1988"},{"key":"S0960129500000049_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"S0960129500000049_ref019","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62700"},{"key":"S0960129500000049_ref022","doi-asserted-by":"crossref","unstructured":"Schaffert C. , Cooper T. , Bullis B. , Kilian M. and Wilpolt C. (1986) An introduction to Trellis\/Owl. Proc. ACM Conf. Object-Oriented Programming Systems, Languages and Applications, pp. 9\u201316","DOI":"10.1145\/28697.28699"},{"key":"S0960129500000049_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-06859-7_148"},{"key":"S0960129500000049_ref001","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39166"},{"key":"S0960129500000049_ref015","doi-asserted-by":"crossref","unstructured":"Mitchell J.C. (1984) Coercion and type inference. Proc. 11th ACM Symp. on Principles of Programming Languages, pp. 175\u2013185","DOI":"10.1145\/800017.800529"},{"key":"S0960129500000049_ref017","first-page":"365","volume-title":"Handbook of Theoretical Computer Science","author":"Mitchell","year":"1990"},{"key":"S0960129500000049_ref012","article-title":"Constructive natural deduction and its \u2018w-set\u2019 interpretation. Report CMU-CS-88\u2013131, CMU, Dept. of Computer Science","volume":"1","author":"Longo","year":"1988","journal-title":"Math. Struct. Comput. Set"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000049","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T00:06:32Z","timestamp":1738973192000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000049\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,3]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,3]]}},"alternative-id":["S0960129500000049"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000049","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,3]]}}}