{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:18Z","timestamp":1761611238147,"version":"3.35.0"},"reference-count":48,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4786,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1995,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit constructor for object types and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a basis for justifying and comparing previous encodings of objects based on recursive record types (Cardelli, 1984; Cardelli, 1992; Bruce, 1994; Cook<jats:italic>et al.<\/jats:italic>, 1990; Mitchell, 1990a) and encodings based on existential types (Pierce &amp; Turner, 1994).<\/jats:p>","DOI":"10.1017\/s0956796800001490","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T16:11:23Z","timestamp":1226074283000},"page":"593-635","source":"Crossref","is-referenced-by-count":20,"title":["A unifying type-theoretic framework for objects"],"prefix":"10.1017","volume":"5","author":[{"given":"Martin","family":"Hofmann","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Pierce","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"volume-title":"The C++ Programming Language","year":"1986","author":"Stroustrup","key":"S0956796800001490_ref046"},{"key":"S0956796800001490_ref042","first-page":"408","volume-title":"Proc. Colloque sur la Programmation","author":"Reynolds","year":"1974"},{"key":"S0956796800001490_ref041","doi-asserted-by":"crossref","unstructured":"Reichel H. 1995. An Approach to Object Semantics based on Terminal Co-algebras. Mathematical Structures in Computer Science. To appear.","DOI":"10.1017\/S0960129500000694"},{"key":"S0956796800001490_ref039","unstructured":"Pierce B. C. , & Turner D. N. 1993 (Apr.). Statically Typed Friendly Functions via Partially Abstract Types. Technical Report ECS-LFCS-93-256. University of Edinburgh, LFCS. Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899."},{"key":"S0956796800001490_ref037","doi-asserted-by":"crossref","unstructured":"Moggi E. 1989. Computational lambda-calculus and monads. Pages 14\u201323 of: Fourth Annual Symposium on Logic in Computer Science (Asilomar, CA).IEEE Computer Society Press.","DOI":"10.1109\/LICS.1989.39155"},{"key":"S0956796800001490_ref036","first-page":"195","volume-title":"Logical Foundations of Functional Programming","author":"Mitchell","year":"1990"},{"key":"S0956796800001490_ref033","doi-asserted-by":"crossref","unstructured":"L\u00e4ufer K. , & Odersky M. 1994. Polymorphic Type Inference and Abstract Data Types. ACM Transactions on Programming Languages and Systems (TOPLAS). To appear; an earlier version appeared in the Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, 1992, under the title \u201cAn Extension of ML with First-Class Abstract Types\u201d.","DOI":"10.1145\/186025.186031"},{"key":"S0956796800001490_ref031","first-page":"464","volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"Kamin","year":"1994"},{"volume-title":"Positive Subtyping","year":"1994","author":"Hofmann","key":"S0956796800001490_ref030"},{"volume-title":"Smalltalk-80: The Language and Its Implementation","year":"1983","author":"Goldberg","key":"S0956796800001490_ref028"},{"key":"S0956796800001490_ref025","doi-asserted-by":"publisher","DOI":"10.1145\/62058.62060"},{"key":"S0956796800001490_ref023","unstructured":"Cook W. R. , Hill W. L. , & Canning P. S. 1990 (Jan.). Inheritance is not Subtyping. Pages 125\u2013135 of: Seventeenth Annual ACM Symposium on Principles of Programming Languages. Also in Gunter Carl A. and Mitchell John C. , editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994)."},{"key":"S0956796800001490_ref016","doi-asserted-by":"publisher","DOI":"10.1145\/6041.6042"},{"key":"S0956796800001490_ref035","unstructured":"Mitchell J. C. 1990a (Jan.). Toward a Typed Foundation for Method Specialization and Inheritance. Pages 109\u2013124 of: Proceedings of the 17th ACM Symposium on Principles of Programming Languages. Also in Gunter Carl A. and Mitchell John C. , editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994)."},{"volume-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1992","author":"Cardelli","key":"S0956796800001490_ref014"},{"key":"S0956796800001490_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-13346-1_2"},{"key":"S0956796800001490_ref010","doi-asserted-by":"crossref","unstructured":"Canning P. , Cook W. , Hill W. , Olthoff W. , & Mitchell J. 1989 (Sept.). F-Bounded Quantification for Object-Oriented Programming. Pages 273\u2013280 of: Fourth International Conference on Functional Programming Languages and Computer Architecture.","DOI":"10.1145\/99370.99392"},{"key":"S0956796800001490_ref009","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001039"},{"key":"S0956796800001490_ref008","doi-asserted-by":"crossref","unstructured":"Bruce K. , & Mitchell J. 1992 (Jan.). PER models of subtyping, recursive types and higher-order polymorphism. In: Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/143165.143230"},{"key":"S0956796800001490_ref002","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001052"},{"key":"S0956796800001490_ref019","unstructured":"Compagnoni A. B. 1994 (Jan.). Subtyping in F_{\\caret}^{\\omega} is decidable. Tech. rept. ECS-LFCS-94-281. LFCS, University of Edinburgh. To appear in the proceedings of Computer Science Logic, September 1994, under the title \u201cDecidability of Higher-Order Subtyping with Intersection Types\u201d."},{"volume-title":"LNCS 389","year":"1989","author":"Coquand","key":"S0956796800001490_ref024"},{"key":"S0956796800001490_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019443"},{"volume-title":"Various Publications Series 11","year":"1970","author":"Kock","key":"S0956796800001490_ref032"},{"key":"S0956796800001490_ref017","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"S0956796800001490_ref001","unstructured":"Abadi M. 1992 (Feb.). Doing without F-bounded quantification. Message to Types electronic mail list."},{"key":"S0956796800001490_ref013","unstructured":"Cardelli L. 1990 (Oct.). Notes about F_{\\lt}^{\\omega} Unpublished manuscript."},{"key":"S0956796800001490_ref012","doi-asserted-by":"crossref","unstructured":"Cardelli L. 1988 (Jan.). Structural Subtyping and the Notion of Power Type. Pages 70\u201379 of: Proceedings of the 15th ACM Symposium on Principles of Programming Languages.","DOI":"10.1145\/73560.73566"},{"key":"S0956796800001490_ref034","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"volume-title":"An Abstract View of Objects and Subtyping (Preliminary Report)","year":"1992","author":"Hofmann","key":"S0956796800001490_ref029"},{"key":"S0956796800001490_ref022","doi-asserted-by":"crossref","unstructured":"Cook W. 1989. A Denotational Semantics of Inheritance. Ph.D. thesis, Brown University.","DOI":"10.1145\/74877.74922"},{"key":"S0956796800001490_ref015","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000198"},{"volume-title":"Theoretical Aspects of Computer Software (TACS)","year":"1994","author":"Abadi","key":"S0956796800001490_ref004"},{"key":"S0956796800001490_ref005","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155231"},{"volume-title":"Category Theory for Computing Science","year":"1990","author":"Barr","key":"S0956796800001490_ref007"},{"key":"S0956796800001490_ref047","unstructured":"Wand M. 1987 (June). Complete type inference for simple objects. In: Proceedings of the IEEE Symposium on Logic in Computer Science."},{"volume-title":"Programming in Higher-order Typed Lambda-Calculi","year":"1989","author":"Pierce","key":"S0956796800001490_ref038"},{"key":"S0956796800001490_ref040","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001040"},{"volume-title":"Programming in Martin-L\u00f6f's Type Theory. An Introduction","year":"1990","author":"Smith","key":"S0956796800001490_ref044"},{"key":"S0956796800001490_ref003","doi-asserted-by":"crossref","unstructured":"Abadi M. , & Cardelli L. 1994b. A Theory of Primitive Objects: Second-order Systems. In: European Symposium on Programming (ESOP), Edinburgh, Scotland.","DOI":"10.1007\/3-540-57880-3_1"},{"volume-title":"Information and Computation","year":"1994","author":"Castagna","key":"S0956796800001490_ref018"},{"key":"S0956796800001490_ref045","unstructured":"Steffen M. , & Pierce B. 1994 (June). Higher-Order Subtyping. In: IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET). An earlier version appeared as University of Edinburgh technical report ECS-LFCS-94-280 and Universit\u00e4t Erlangen-N\u00fcrnberg Interner Bericht IMMD7-01\/94, January 1994."},{"key":"S0956796800001490_ref020","unstructured":"Compagnoni A. B. , & Pierce B. C. 1993 (Aug.). Multiple Inheritance via Intersection Types. Tech. rept. ECS-LFCS-93-275. LFCS, University of Edinburgh. Also available as Catholic University Nijmegen computer science technical report 93\u201318."},{"volume-title":"A note on categorical datatypes. Lecture Notes in Computer Science","year":"1989","author":"Wraith","key":"S0956796800001490_ref048"},{"key":"S0956796800001490_ref026","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_128"},{"key":"S0956796800001490_ref043","first-page":"309","volume-title":"Programming Methodology, A Collection of Articles by IFIP WG2.3.","author":"Reynolds","year":"1978"},{"key":"S0956796800001490_ref027","unstructured":"Girard J.-Y. 1972. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. Ph.D. thesis, Universit\u00e9 Paris VII."},{"key":"S0956796800001490_ref006","volume-title":"Handbook of Logic in Computer Science","volume":"II","author":"Barendregt","year":"1992"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001490","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T15:29:31Z","timestamp":1738510171000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001490\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,10]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1995,10]]}},"alternative-id":["S0956796800001490"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001490","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"type":"print","value":"0956-7968"},{"type":"electronic","value":"1469-7653"}],"subject":[],"published":{"date-parts":[[1995,10]]}}}