Simple type-theoretic foundations for object-oriented programming

Journal of Functional Programming - Tập 4 Số 2 - Trang 207-247 - 1994
Benjamin C. Pierce1, David N. Turner1
1Department of Computer Science, University of Edinburgh, The King's Buildings, Edinburgh, EH9 3JZ, UK

Tóm tắt

AbstractWe 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 λ-calculus.

Từ khóa


Tài liệu tham khảo

10.1016/1385-7258(72)90034-0

10.1145/6041.6042

Abadi, 1993, Baby Modula-3 and a Theory of Objects

Reynolds, 1978, Programming Methodology, A Collection of Articles by IFIP WG2.3, 309

Gunter, 1993, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design

10.1016/0890-5401(88)90007-7

Cook W. (1989) A Denotational Semantics of Inheritance, PhD thesis, Brown University.

10.1017/S0960129500000049

Goldberg, 1983, Smalltalk-80: The Language and Its Implementation

Gunter, 1993, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design

Snyder, 1986, Proc. OOPSLA '86., 38

Pierce, 1993, Proc. 20th ACM Symp. on Principles of Program. Lang., 109

10.1016/0890-5401(90)90062-M

Reynolds, 1985, Mathematical Foundations of Software Development; Lecture Notes in Computer Science 185

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.)

Graver, 1990, Proc. 17th Ann. ACM Symp. on Principles of Program. Lang., 125

Castagna G. (1992) Strong Typing in Object-Oriented Paradigms, Rapport de Recherche LIENS-92-11, Ecole Normale Supérieure, Paris, France, May.

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.

Cardelli, 1992, Extensible Records in a Pure Calculus of Subtyping

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–280, September.

Mitchell, 1993, IIEEE Symp. on Logic in Comput. Sci., 109

Mitchell, 1991, Proc. 18th ACM Symp. on Principles of Program. Lang., 270

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.

Bruce K.B. (1991) The equivalence of two semantic definitions for inheritance in object-oriented languages. In: Proc. Math. Foundations of Program. Semantics March.

10.1145/885631.885632

10.1007/3-540-17184-3_38

Cardelli L. (1988b) Structural subtyping and the notion of power type. In: Proc. 15th ACM Symp. on Principles of Program. Lang., pp. 70–79, January.

Girard J.-Y. (1972) Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VII, France

10.1017/S0960129500001134

Wand, 1987, Proc. IEEE Symp. on Logic in Comput. Sci., 227

Kamin, 1988, Proc. ACM Symp. on Principles of Program. Lang., 80

Bruce K.B. and van Gent R. (1993) TOIL: A new Type-safe Object-oriented Imperative Language, submitted for publication.

Mitchell, 1990, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design

Cook, 1990, Proc. 17th Ann. ACM Symp. on Principles of Program. Lang., 125

Ungar, 1987, Proc. ACM Symp. on Object-Oriented Program.: Lang., Syst. and Applic., 227

10.1007/3-540-54415-1_73

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 ‘An Abstract View of Objects and Subtyping (Preliminary Report)’ University of Edinburgh, LFCS Technical Report ECS-LFCS-92-226, 1992.)

Robinson E. and Tennent R. (1988) Bounded quantification and record-update problems. Message to Types electronic mail list.

Reynolds, 1983, Information Processing 83, 513

Rémy, 1989, Proc. 16th Ann. ACM Symp. on Principles of Program. Lang., 242

Ghelli, 1991, Conf. on Object-Oriented Program. Syst., Lang. and Applic., 129

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–124. (Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899.)

Wand, 1988, Proc. IEEE Symp. on Logic in Comput. Sci.

Cardelli L. (1992b) Typed Foundations of Object-oriented Programming, Tutorial given at POPL '92, January.

Bruce K.B. (1992) A Paradigmatic Object-Oriented Language: Design, Static Typing and Semantics, Technical Report CS-92-01, Williams College, January.

Cardelli L. (1990) Notes about F, Unpublished notes, October.

Budd, 1991, An Introduction to Object-Oriented Programming

Castagna, 1992, ACM Conf. on LISP and Functional Progra.g, 182

Mitchell, 1990, Proc. 17th ACM Symp. on Principles of Program. Lang., 109

Reddy, 1988, Proc. ACM Symp. on Lisp and Functional Program., 289

10.1002/malq.19810270205

Jategaonkar, 1988, Proc. ACM Conf. on Lisp and Functional Program., 198

10.1145/44501.45065

Schuman, New Advances in Algorithmic Languages 1975, 157

Wand, 1989, Proc. 4th Ann. IEEE Symp. on Logic in Comput. Sci., 92