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


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


[1] Amadio, R., A fixed point extension of the second-order lambda-calculus: observable equialences and models, (), 51-60
[2] Amadio, R., Recursion over realizability structures, (1989), Dip. Informatica Pisa, Report · Zbl 0760.03012
[3] Amadio, R., Proof theoretic properties of a theory of inheritance, (1989), Dip. Informatica Pisa, in preparation
[4] Andrews, T.; Harris, C., Combining language and database advances in an object-oriented development environment, (), 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 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), (), 112-129 · Zbl 0716.68012
[11] Bruce, K.; Meyer, A., A completeness theorem for second-order polymorphic lambda calculus, (), 131-144
[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, (), 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, (), 23-42
[16] Cardelli, L.; Cardelli, L., A semantics of multiple inheritance, (), 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, () · Zbl 0581.03007
[20] Curien, P.-L.; Ghelli, G., Coherence of subsumption, (), to appear · Zbl 0759.03009
[21] Ehrhard, T., A categorical semantics of constructions, (), 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 Reading, MA · Zbl 0518.68001
[24] Hyland, M., The effective topos, (), 165-216 · Zbl 0522.03055
[25] Hyland, M., A small complete category, (), 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 Boulder · Zbl 0721.03048
[27] Hyland, M.; Robinson, E.; Rosolini, P., The discrete objects in the effective topos, (), 1-36, (3) · Zbl 0703.18002
[28] Jategaonkar, L.; Mitchell, J., ML with extended pattern matching and subtypes, (), 198-211
[29] Liskov, B., Data abstraction and hierarchy, addendum, (), 17-34, No. 5
[30] Longo, G., On Church’s formal theory of functions and functionals, (), 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, (), to appear · Zbl 0756.03028
[33] MacQueen, D.; Plotkin, G.; Sethi, R., An ideal model for recursive polymorphic types, (), 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, (), 228-241
[36] Meyer, A.; Mitchell, J.; Moggi, E.; Statman, R., Empty types in polymorphic lambda calculus, (), 253-262
[37] Meyer, B., Object-oriented software construction, (1988), Prentice-Hall New York
[38] Mitchell, J.C., Semantic models for second-order lambda calculus, (), 289-299
[39] Mitchell, J.C., Coercion and type inference, (), 175-185
[40] Mitchell, J.C., A type-inference approach to reduction properties and semantics of polymorphic expressions, (), 308-319
[41] Mitchell, J.C.; Mitchell, J.C., Polymorphic type inference and containment, (), 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, () · Zbl 0644.18003
[44] Reynolds, J.C., Towards a theory of type structure, (), 408-425
[45] Reynolds, J.C., Using category theory to design implicit conversions and generic operators, (), 211-258
[46] Reynolds, J.C., Polymorphism is not set-theoretic, (), 145-156
[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, (), 9-16, No. 11
[50] Snyder, A., Encapsulation and inheritance in object-oriented programming languages, (), 38-45, No. 11
[51] Stroustrup, B., The C++ programming language, (1986), Addison-Wesley Menlo Park, CA · Zbl 0609.68011
[52] Troelstra, A.S., Notes in intuitionistic second order arithmetic, (), 171-203 · Zbl 0275.02036
[53] Wand, M., Type inference for record concatenation and multiple inheritance, (), 92-97
[54] Weinreb, D.; Moon, D., ()
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.