{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:15Z","timestamp":1779836715158,"version":"3.53.1"},"reference-count":55,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5334,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1994,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We develop a formal, type-theoretic account of the basic mechanisms of object-oriented programming: encapsulation, message passing, subtyping and inheritance. By modelling object encapsulation in terms of existential types instead of the recursive records used in other recent studies, we obtain a substantial simplification both in the model of objects and in the underlying typed \u03bb-calculus.<\/jats:p>","DOI":"10.1017\/s0956796800001040","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T11:12:55Z","timestamp":1226056375000},"page":"207-247","source":"Crossref","is-referenced-by-count":101,"title":["Simple type-theoretic foundations for object-oriented programming"],"prefix":"10.1017","volume":"4","author":[{"given":"Benjamin C.","family":"Pierce","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David N.","family":"Turner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001040_ref028","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796800001040_ref018","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0956796800001040_ref001","volume-title":"Baby Modula-3 and a Theory of Objects","author":"Abadi","year":"1993"},{"key":"S0956796800001040_ref047","first-page":"309","volume-title":"Programming Methodology, A Collection of Articles by IFIP WG2.3","author":"Reynolds","year":"1978"},{"key":"S0956796800001040_ref049","volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"Gunter","year":"1993"},{"key":"S0956796800001040_ref012","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90007-7"},{"key":"S0956796800001040_ref023","doi-asserted-by":"crossref","unstructured":"Cook W. (1989) A Denotational Semantics of Inheritance, PhD thesis, Brown University.","DOI":"10.1145\/74877.74922"},{"key":"S0956796800001040_ref017","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000049"},{"key":"S0956796800001040_ref031","volume-title":"Smalltalk-80: The Language and Its Implementation","author":"Goldberg","year":"1983"},{"key":"S0956796800001040_ref027","volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"Gunter","year":"1993"},{"key":"S0956796800001040_ref051","first-page":"38","volume-title":"Proc. OOPSLA '86.","author":"Snyder","year":"1986"},{"key":"S0956796800001040_ref041","first-page":"109","volume-title":"Proc. 20th ACM Symp. on Principles of Program. Lang.","author":"Pierce","year":"1993"},{"key":"S0956796800001040_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90062-M"},{"key":"S0956796800001040_ref046","volume-title":"Mathematical Foundations of Software Development; Lecture Notes in Computer Science 185","author":"Reynolds","year":"1985"},{"key":"S0956796800001040_ref022","unstructured":"Compagnoni A.B. and Pierce B.C. (1993) Multiple Inheritance via Intersection Types, Technical Report ECS-LFCS-93-275, LFCS, University of Edinburgh, UK, August. (Also available as Catholic University Nijmegen Computer Science Technical Report 93-18. Submitted for conference publication.)"},{"key":"S0956796800001040_ref032","first-page":"125","volume-title":"Proc. 17th Ann. ACM Symp. on Principles of Program. Lang.","author":"Graver","year":"1990"},{"key":"S0956796800001040_ref021","unstructured":"Castagna G. (1992) Strong Typing in Object-Oriented Paradigms, Rapport de Recherche LIENS-92-11, Ecole Normale Sup\u00e9rieure, Paris, France, May."},{"key":"S0956796800001040_ref006","doi-asserted-by":"crossref","unstructured":"Bruce K.B. (1993) Safe type checking in a statically typed object-oriented programming language. In: Proc. 20th ACM Symp. on Principles of Program. Lang. January.","DOI":"10.1145\/158511.158650"},{"key":"S0956796800001040_ref015","volume-title":"Extensible Records in a Pure Calculus of Subtyping","author":"Cardelli","year":"1992"},{"key":"S0956796800001040_ref010","doi-asserted-by":"crossref","unstructured":"Canning P. , Cook W , Olthoff G. and Mitchell J. (1989) F-bounded quantification for object-oriented programming. In: Proc. 4th Intern. Conf. on Functional Program. & Computer Archit., pp. 273\u2013280, September.","DOI":"10.1145\/99370.99392"},{"key":"S0956796800001040_ref040","first-page":"109","volume-title":"IIEEE Symp. on Logic in Comput. Sci.","author":"Mitchell","year":"1993"},{"key":"S0956796800001040_ref037","first-page":"270","volume-title":"Proc. 18th ACM Symp. on Principles of Program. Lang.","author":"Mitchell","year":"1991"},{"key":"S0956796800001040_ref003","doi-asserted-by":"crossref","unstructured":"Bruce K. and Mitchell J. (1992) PER models of subtyping, recursive types and higher-order polymorphism. In: Proc. 19th ACM Symp. on Principles of Program. Lang. January.","DOI":"10.1145\/143165.143230"},{"key":"S0956796800001040_ref004","doi-asserted-by":"crossref","unstructured":"Bruce K.B. (1991) The equivalence of two semantic definitions for inheritance in object-oriented languages. In: Proc. Math. Foundations of Program. Semantics March.","DOI":"10.1007\/3-540-55511-0_5"},{"key":"S0956796800001040_ref002","doi-asserted-by":"publisher","DOI":"10.1145\/885631.885632"},{"key":"S0956796800001040_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17184-3_38"},{"key":"S0956796800001040_ref013","doi-asserted-by":"crossref","unstructured":"Cardelli L. (1988b) Structural subtyping and the notion of power type. In: Proc. 15th ACM Symp. on Principles of Program. Lang., pp. 70\u201379, January.","DOI":"10.1145\/73560.73566"},{"key":"S0956796800001040_ref030","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, France"},{"key":"S0956796800001040_ref026","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001134"},{"key":"S0956796800001040_ref053","first-page":"227","volume-title":"Proc. IEEE Symp. on Logic in Comput. Sci.","author":"Wand","year":"1987"},{"key":"S0956796800001040_ref035","first-page":"80","volume-title":"Proc. ACM Symp. on Principles of Program. Lang.","author":"Kamin","year":"1988"},{"key":"S0956796800001040_ref008","unstructured":"Bruce K.B. and van Gent R. (1993) TOIL: A new Type-safe Object-oriented Imperative Language, submitted for publication."},{"key":"S0956796800001040_ref039","volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"Mitchell","year":"1990"},{"key":"S0956796800001040_ref024","first-page":"125","volume-title":"Proc. 17th Ann. ACM Symp. on Principles of Program. Lang.","author":"Cook","year":"1990"},{"key":"S0956796800001040_ref052","first-page":"227","volume-title":"Proc. ACM Symp. on Object-Oriented Program.: Lang., Syst. and Applic.","author":"Ungar","year":"1987"},{"key":"S0956796800001040_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54415-1_73"},{"key":"S0956796800001040_ref033","unstructured":"Hofmann M. and Pierce B. (1994) A unifying type-theoretic framework for objects. In: Symp. on Theoretical Aspects of Comput. Sci. (Extended version available as \u2018An Abstract View of Objects and Subtyping (Preliminary Report)\u2019 University of Edinburgh, LFCS Technical Report ECS-LFCS-92-226, 1992.)"},{"key":"S0956796800001040_ref050","unstructured":"Robinson E. and Tennent R. (1988) Bounded quantification and record-update problems. Message to Types electronic mail list."},{"key":"S0956796800001040_ref045","first-page":"513","volume-title":"Information Processing 83","author":"Reynolds","year":"1983"},{"key":"S0956796800001040_ref044","first-page":"242","volume-title":"Proc. 16th Ann. ACM Symp. on Principles of Program. Lang.","author":"R\u00e9my","year":"1989"},{"key":"S0956796800001040_ref029","first-page":"129","volume-title":"Conf. on Object-Oriented Program. Syst., Lang. and Applic.","author":"Ghelli","year":"1991"},{"key":"S0956796800001040_ref042","unstructured":"Pierce B.C. and Turner D.N. (1993b) Statically Typed Friendly Functions via Partially Abstract Types, Technical Report ECS-LFCS-93-256. University of Edinburgh, LFCS, pp. 109\u2013124. (Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.)"},{"key":"S0956796800001040_ref054","volume-title":"Proc. IEEE Symp. on Logic in Comput. Sci.","author":"Wand","year":"1988"},{"key":"S0956796800001040_ref016","unstructured":"Cardelli L. (1992b) Typed Foundations of Object-oriented Programming, Tutorial given at POPL '92, January."},{"key":"S0956796800001040_ref005","unstructured":"Bruce K.B. (1992) A Paradigmatic Object-Oriented Language: Design, Static Typing and Semantics, Technical Report CS-92-01, Williams College, January."},{"key":"S0956796800001040_ref014","unstructured":"Cardelli L. (1990) Notes about F, Unpublished notes, October."},{"key":"S0956796800001040_ref009","volume-title":"An Introduction to Object-Oriented Programming","author":"Budd","year":"1991"},{"key":"S0956796800001040_ref020","first-page":"182","volume-title":"ACM Conf. on LISP and Functional Progra.g","author":"Castagna","year":"1992"},{"key":"S0956796800001040_ref038","first-page":"109","volume-title":"Proc. 17th ACM Symp. on Principles of Program. Lang.","author":"Mitchell","year":"1990"},{"key":"S0956796800001040_ref043","first-page":"289","volume-title":"Proc. ACM Symp. on Lisp and Functional Program.","author":"Reddy","year":"1988"},{"key":"S0956796800001040_ref025","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"S0956796800001040_ref034","first-page":"198","volume-title":"Proc. ACM Conf. on Lisp and Functional Program.","author":"Jategaonkar","year":"1988"},{"key":"S0956796800001040_ref036","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"S0956796800001040_ref048","first-page":"157","volume-title":"New Advances in Algorithmic Languages 1975","author":"Schuman"},{"key":"S0956796800001040_ref055","first-page":"92","volume-title":"Proc. 4th Ann. IEEE Symp. on Logic in Comput. Sci.","author":"Wand","year":"1989"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:35:15Z","timestamp":1779834915000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001040\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,4]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,4]]}},"alternative-id":["S0956796800001040"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001040","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,4]]}}}