×

A modest model of records, inheritance, and bounded quantification. (English) Zbl 0711.68072

The paper presents a formal semantics for the language bounded fun from Cardelli and Wegner (1985). Bounded fun is an extension of second-order lambda calculus supporting both parametric and subtype (inheritance) polymorphism. Partial equivalence relations are used to model inheritance in this language in the presence of subtype and record types.
The technical part begins with an introduction to the typed lambda calculus with records and subtypes. It follows a discussion of its model- theoretic semantics based on partial equivalence relations. Syntax and semantics of the language minimal bounded fun and an extension of it are presented, which are modifications of bounded fun. Based on these languages, the semantics of bounded fun itself can be defined. A generalization of partial equivalence relations, called \(\omega\)-sets, are used in combination with modest sets to provide a model of bounded fun with explicit polymorphism. The paper ends with a discussion of principal problems arising with the chosen approach and its relation to other recent work.
Reviewer: G.Saake

MSC:

68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amadio, R., A fixed point extension of the second-order lambda-calculus: Observable equialences and models, (Proceeding, L.I.C.S. 88. Proceeding, L.I.C.S. 88, Edinburgh (1988)), 51-60
[2] Amadio, R., Recursion over Realizability Structures (1989), Dip. Informatica: Dip. Informatica Pisa, Report · Zbl 0760.03012
[3] Amadio, R., Proof theoretic properties of a theory of inheritance (1989), Dip. Informatica: Dip. Informatica Pisa, in preparation
[4] Andrews, T.; Harris, C., Combining language and database advances in an object-oriented development environment, (Proceeding of OOPSLA ’87. Proceeding of OOPSLA ’87, SIGPLAN Notices, 22 (1987)), 430-440, No. 12
[5] Asperti, A.; Longo, G., Applied category theory: An introduction to categories, types and structures for the working computer scientist (1989), MIT Press, book, to appear
[6] Bainbridge, E. S.; Freyd, P. J.; Scedrov, A.; Scott, P. J., Functorial polymorphism, Theoret. Comput. Sci., 70, 35-64 (1990) · Zbl 0717.18005
[7] Birtwistle, G.; Dahl, O. J.; Myrhaug, B.; Nygaard, K., Simula Begin (1973), Studentliteratur: Studentliteratur Lund and Auerback, New York
[8] Bobrow, D. G.; Stefik, M. J., Loops: An Object-Oriented Programming System for Interlisp (1982), Xerox PARC
[9] Breazu-Tannen, V.; Coquand, T., Extensional models for polymorphism, Theoret. Comput. Scie., 59, 85-114 (1987) · Zbl 0713.03005
[10] Breazu-Tannen, V.; Coquand, T.; Gunter, C.; Scedrov, A., Inheritance and explicit coercion (preliminary report), (Proceedings, of L.I.C.S. ’89 (1989)), 112-129 · Zbl 0716.68012
[11] Bruce, K.; Meyer, A., A completeness theorem for second-order polymorphic lambda calculus, (Kahn; MacQueen; Plotkin, Proceedings, International Symposium on the Semantics of Data Types. Proceedings, International Symposium on the Semantics of Data Types, Lect. Notes in Comput. Sci., Vol. 173 (1984), Springer-Verlag: Springer-Verlag New/York/Berlin), 131-144 · Zbl 0554.03011
[12] Bruce, K.; Meyer, A.; Mitchell, J., The semantics of second order lambda-calculus, Inform. and Comput. (1990), to appear; see also Bruce and Meyer (1984) for an earlier version · Zbl 0714.68052
[13] Bruce, K.; Wegner, P., An Algebraic Model of Subtype and Inherence, (Proceedings, International Workshop on Database and Programming Languages. Proceedings, International Workshop on Database and Programming Languages, Roscoff, France, September, 1987. Proceedings, International Workshop on Database and Programming Languages. Proceedings, International Workshop on Database and Programming Languages, Roscoff, France, September, 1987, Brown University Technical Report CS-87-21 (1987)), to appear
[14] Canning, P.; Cook, W.; Hill, W.; Mitchell, J.; Olthoff, W., \(F\)-bounded quantification for Object-Oriented Programming, HP Report STL-89-5 (1989)
[15] Carboni, A.; Freyd, P.; Scedrov, A., A categorical approach to realizability and polymorphic types, (Main; Mislove; Schmidt, Proceedings, 3d Symposium on Mathematical Foundations of Programming Language Semantics. Proceedings, 3d Symposium on Mathematical Foundations of Programming Language Semantics, Lect. Notes in Comput. Sci., Vol. 198 (1987), Springer-Verlag: Springer-Verlag New York/Berlin), 23-42 · Zbl 0651.18004
[16] Cardelli, L., (Kahn; MacQueen; Plotkin, Proceedings of International Symposium on the Semantics of Data Types. Proceedings of International Symposium on the Semantics of Data Types, Lect. Notes in Comput. Sci., Vol. 173 (1988), Springer-Verlag: Springer-Verlag New York/Berlin), 51-67, preliminary version appeared in
[17] Cardelli, L.; Longo, G., A Semantic Basis for Quest, DEC-SRC Report (1989), in preparation
[18] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, ACM Comput. Surveys, 17, 47-522 (1985)
[19] Coquand, T.; Huet, G., Constructions: A Higher Order Proof System for Mechanizing Mathematics, (presented at EUROCAL 85. presented at EUROCAL 85, Report 401 (1985), INRIA) · Zbl 0581.03007
[20] Curien, P.-L.; Ghelli, G., Coherence of subsumption, (Proceedings, CAAP 90 (1990)), to appear · Zbl 0759.03009
[21] Ehrhard, T., A categorical semantics of constructions, (Proceedings of L.I.C.S. ’88. Proceedings of L.I.C.S. ’88, Edinburgh (1988)), 264-273
[22] Girard, T., Interprétation fonctionelle et élimination des coupures dans l’arithmetic d’ordre supérieur, Thèse de Doctorat d’Etat, Paris (1972)
[23] Goldberg, A.; Robson, D., Smalltalk-80: The Language and Its Implementation (1983), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0518.68001
[24] Hyland, M., The effective Topos, (Troelstra; Van Dalen, The L.E.J. Brouwer Centary Symposium (1982), North-Holland: North-Holland Amsterdam), 165-216 · Zbl 0522.03055
[25] Hyland, M., A small complete category, (Ann. Pure Appl. Logic, Vol. 40 (1988), North-Holland: North-Holland Amsterdam), 93-133 · Zbl 0659.18007
[26] Hyland, M.; Pitts, A., The theory of Constructions: Categorical semantics and topos-theoretic models (1987), Amer. Math. Soc. Notes: Amer. Math. Soc. Notes Boulder · Zbl 0721.03048
[27] Hyland, M.; Robinson, E.; Rosolini, P., The discrete objects in the effective topos, (Proc. London Math. Soc., 60 (1990)), 1-36, (3) · Zbl 0703.18002
[28] Jategaonkar, L.; Mitchell, J., ML with extended pattern matching and subtypes, (Proceedings, 1988 ACM Conference on the LISP and Functional Programming (1988)), 198-211
[29] Liskov, B., Data abstraction and hierarchy, Addendum, (Proceedings of OOPSLA ’87. Proceedings of OOPSLA ’87, SIGPLAN Notices, 23 (1988)), 17-34, No. 5
[30] Longo, G., On Church’s formal theory of functions and functionals, (Ann. Pure Appl. Logic, 40 (1988), North-Holland: North-Holland Amsterdam), 93-133 · Zbl 0673.03009
[31] Longo, G., From type structures to type theories, Lecture Notes for a graduate course at Carnegie-Mellon University, 1987/88 (1988)
[32] Longo, G.; Moggi, E., Constructive natural deduction and its modest interpretation, (Meseguer, Workshop, Semantics of Natural and Programming Languages. Workshop, Semantics of Natural and Programming Languages, Stanford, March 1987 (1988), MIT Press), to appear · Zbl 0756.03028
[33] MacQueen, D.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, (Proceedings, 11th ACM Symposium on the Principles of Programming Languages (1984)), 165-174
[34] Martini, S., Modelli non estensionali del polimorfismo in programmazione funzionale, Tesi di Dottorato (1988), Pisa, forthcoming
[35] Meseguer, J., Relating models of polymorphism, (Proceedings, 16th ACM Symposium on the Principles of Programming Languages (1989)), 228-241
[36] Meyer, A.; Mitchell, J.; Moggi, E.; Statman, R., Empty types in polymorphic lambda calculus, (Proceedings of POPL ’87 (1987)), 253-262
[37] Meyer, B., Object-oriented Software Construction (1988), Prentice-Hall: Prentice-Hall New York
[38] Mitchell, J. C., Semantic models for second-order lambda calculus, (Proceedings, 25th IEEE Sympos. on Foundations of Computer Science (1984)), 289-299
[39] Mitchell, J. C., Coercion and type inference, (Proceedings, 11th ACM Symposium on the Principles of Programming Languages (1984)), 175-185
[40] Mitchell, J. C., A type-inference approach to reduction properties and semantics of polymorphic expressions, (Proceedings, ACM Conference on LISP and Functional Programming. Proceedings, ACM Conference on LISP and Functional Programming, Boston (1986)), 308-319
[41] Mitchell, J. C., (Kahn; MacQueen; Plotkin, Symposium on Semantics of Data Types. Symposium on Semantics of Data Types, Lect. Notes in Comput. Sci., Vol. 173 (1988), Springer-Verlag: Springer-Verlag New York/Berlin), 257-278, An earlier version appeared in · Zbl 0656.68023
[42] Moggi, E., Message on “Types electronic-mailing list, January, 1986” (1986)
[43] Pitts, A., Polymorphism is set theoretic, constructively, (Pitts; etal., Symposium on Category Theory and Comput. Sci.. Symposium on Category Theory and Comput. Sci., Edinburgh. Symposium on Category Theory and Comput. Sci.. Symposium on Category Theory and Comput. Sci., Edinburgh, Lect. Notes in Comput. Sci., Vol. 283 (1987), Springer-Verlag: Springer-Verlag New York/Berlin) · Zbl 0644.18003
[44] Reynolds, J. C., Towards a theory of type structure, (Paris Colloquium on Programming. Paris Colloquium on Programming, Lect. Notes in Comput. Sci., Vol. 19 (1974), Springer-Verlag: Springer-Verlag New York/Berlin), 408-425 · Zbl 0309.68016
[45] Reynolds, J. C., Using category theory to design implicit conversions and generic operators, (Semantics Directed Compiler Generation. Semantics Directed Compiler Generation, Lect. Notes in Comput. Sci., Vol. 94 (1980), Springer-Verlag: Springer-Verlag New York/Berlin), 211-258
[46] Reynolds, J. C., Polymorphism is not set-theoretic, (Kahn; MacQueen; Plotkin, Symposium on Semantics of Data Types. Symposium on Semantics of Data Types, Lect. Notes in Comput. Sci., Vol. 173 (1984), Springer-Verlag: Springer-Verlag New York/Berlin), 145-156 · Zbl 0554.03012
[47] Rosolini, G., About Modest Sets (1986), notes for a talk delivered in Pisa · Zbl 0729.18003
[48] Seely, R. A.G., Categorical semantics for higher order polymorphic lambda calculus, J. Symbolic Logic, 52, 969-989 (1986) · Zbl 0642.03007
[49] Shaffert, C.; Cooper, T.; Bullis, B.; Kilian, M.; Wilpolt, C., An introduction to Trellis/Owl, (Proceedings of OOPSLA ’86. Proceedings of OOPSLA ’86, SIGPLAN Notices, 21 (1986)), 9-16, No. 11
[50] Snyder, A., Encapsulation and inheritance in object-oriented programming languages, (Proceedings of OOPSLA ’86. Proceedings of OOPSLA ’86, SIGPLAN Notices, 21 (1986)), 38-45, No. 11
[51] Stroustrup, B., The C++ Programming Language (1986), Addison-Wesley: Addison-Wesley Menlo Park, CA · Zbl 0609.68011
[52] Troelstra, A. S., Notes in intuitionistic second order arithmetic, (Cambridge Summer School in Mathematical Logic. Cambridge Summer School in Mathematical Logic, Lect. Notes in Math., Vol. 337 (1973), Springer-Verlag: Springer-Verlag New York/Berlin), 171-203 · Zbl 0275.02036
[53] Wand, M., Type inference for record concatenation and multiple inheritance, (Proceedings, Fourth Annual Symposium on Logic in Computer Science (1989)), 92-97 · Zbl 0716.68017
[54] Weinreb, D.; Moon, D., (Lisp Machine Manual, Chapter 20: Objects, Message-Passing, and Flavors (1981), Symbolics Inc: Symbolics Inc Cambridge, MA)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.