Recursive types for Fun. (English) Zbl 0746.68018

Summary: The language Fun [L. Cardelli and P.Wegner, On understanding types, data abstraction, and polymorphism, ACM Comput. Surv. 17, 471-522 (1985)] is a typed polymorphic lambda calculus with a notion of subtyping and quantifiers ranging over subtypes of a given type. We show that it is consistent to allow recursive type definitions in Fun, by constructing an interpretation of types as partial equivalence relations of a special kind, terms being interpreted as equivalence classes, modulo such results, of elements of a model for an underlying untyped language.


68N15 Theory of programming languages
03B40 Combinatory logic and lambda calculus
68N01 General topics in the theory of software


Simula 67; Smalltalk
Full Text: DOI


[1] Abadi, M.; Plotkin, G.D., Intrinsic orders on pers, (1989), Unpublished manuscript, Edinburgh
[2] Amadio, R., Recursion over realizability structures, Rapporto interno TR-1/89, (1989), Università di Pisa, Dipartimento di Informatica · Zbl 0760.03012
[3] Amadio, R., Formal theories of inheritance, Rapporto interno, (1989), Università di Pisa, Dipartimento di Informatica
[4] Breazu-Tannen, V.; Coquand, T., Extensional models for polymorphism, Theoret. comput. sci., 59, 85-114, (1988) · Zbl 0713.03005
[5] Breazu-Tannen, V.; Coquand, T.; Gunter, C.; Scedrov, A., Inheritance and explicit coercion, (), 112-129 · Zbl 0716.68012
[6] Bruce, K.; Longo, G., A modest model of records, inheritance and bounded quantification, (), 38-50
[7] K. Bruce, A. Meyer and J.C. Mitchell, The semantics of second order lambda-calculus, Inform. and Comput., to appear. · Zbl 0714.68052
[8] Cardelli, L., Amber, (), 21-47, Lecture Notes in Computer Science
[9] Cardelli, L., A semantics of multiple inheritance, Inform. and comput., 76, 138-164, (1988) · Zbl 0651.68017
[10] Cardelli, L., Structural subtyping and the notion of power type, Proc. 15th ACM symp. on principles of programming languages, 70-79, (1988)
[11] Cardelli, L., Typeful programming, Internal report 45, (1989), DEC SRC
[12] Cardelli, L.; Mitchell, J.C., Operations on records, Proc. 5th internat. conf. on mathematical foundation of programming semantics, (1989), Tulane University New Orleans, to appear
[13] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, ACM comput. surv., 17, 471-522, (1985)
[14] Cartwright, R., Types as intervals, (), 22-36
[15] Coppo, M., A completeness theorem for recursively defined types, (), 120-129, Lecture Notes in Computer Science · Zbl 0585.68047
[16] Coppo, M.; Zacchi, M., Type inference and logical relations, (), 218-226
[17] Dahl, O.; Nygaard, K., Simula, an algol-based simulation language, Comm. ACM, 9, 671-678, (1966) · Zbl 0139.32903
[18] Danforth, S.; Tomlinson, C., Type theories and object-oriented programming, ACM comput. surv., 20, 1, 29-72, (1988) · Zbl 0649.68009
[19] Girard, J.Y., Interpretation fonctionelle et elimination des coupures dans l’arithmetique d’ordre superieur, Thèse de doctorat d’etat, (1972), Paris VII
[20] Goldberg, A.; Robson, D., Smalltalk-80: the language and its implementation, (1983), Addison-Wesley Reading, MA · Zbl 0518.68001
[21] Gunter, C., Universal profinite domains, Inform. and comput., 72, 1-30, (1987) · Zbl 0628.68050
[22] Gunter, C.; Scott, D., Semantic domains, () · Zbl 0900.68301
[23] Longo, G.; Moggi, E., Constructive natural deduction and its modest interpretation, CMU report CS-88-131, (1988)
[24] MacQueen, D.; Plotkin, G.D.; Sethi, R., An ideal model for recursive polymorphic types, Inform. and control, 71, 1/2, 95-130, (1986) · Zbl 0636.68016
[25] Martini, S., Modelli non estensionali del polimorfismo in programmazione funzionale, (1988), Tesi di Dottorato, Università di Pisa
[26] Mitchell, J.C., Coercion and type inference, Proc. 11th ACM symp. on principles of programming languages, 175-185, (1984)
[27] Mitchell, J.C., Type inference and type containment, Inform. and comput., 76, 211-249, (1988) · Zbl 0656.68023
[28] Mitchell, J.C., A type inference approach to reduction properties and semantics of polymorphic expressions, Proc. ACM conf. on LISP and functional programming, 308-319, (1986), Boston
[29] Mitchell, J.C., Toward a typed foundation for method specialization and inheritance, Proc. 17th ACM symp. on principles of programming languages, 109-124, (1990)
[30] Moggi, E., Communication on the types e-mailing List, (1986)
[31] Plotkin, G.D., A powerdomain construction, SIAM J. comput., 5, 452-487, (1976) · Zbl 0355.68015
[32] Plotkin, G.D., Advanced domains, (1978), Summer School Pisa
[33] Reynolds, J., On the relation between direct and continuation semantics, (), 141-156, Lecture Notes in Computer Science
[34] Reynolds, J., Towards a theory of type structure, (), 408-425, Lecture Notes in Computer Science
[35] Scott, D., Continuous lattices, (), 97-136, Lecture Notes in Mathematics
[36] Scott, D., Domains for denotational semantics, (), 577-613, Lecture Notes in Computer Science
[37] Smyth, M.; Plotkin, G.D., The category-theoretic solution of recursive domain equations, SIAM J. comput., 11, 761-783, (1982) · Zbl 0493.68022
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.