×

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.

MSC:

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

Software:

Smalltalk; Simula 67
PDFBibTeX XMLCite
Full Text: DOI

References:

[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, (Proc. Symp. on Logic in Computer Science (1989), IEEE), 112-129 · Zbl 0716.68012
[6] Bruce, K.; Longo, G., A modest model of records, inheritance and bounded quantification, (Proc. Symp. on Logic in Computer Science (1988), IEEE), 38-50
[8] Cardelli, L., Amber, (Combinators and Functional Programming Languages, 242 (1986), Springer: Springer Berlin), 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: Tulane University New Orleans, to appear · Zbl 1493.68082
[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, (Proc. Symp. on Principles of Programming Languages (1985), ACM), 22-36
[15] Coppo, M., A completeness theorem for recursively defined types, (Bauer, W., Proc. 12th Internat. Colloquium on Automata, Languages and Programming, 194 (1985), Springer: Springer Berlin), 120-129, Lecture Notes in Computer Science · Zbl 0585.68047
[16] Coppo, M.; Zacchi, M., Type inference and logical relations, (Proc. Symp. on Logic in Computer Science (1986), IEEE), 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: 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, (van Leeuwen, J., Handbook of Theoretical Computer Science (1990), North-Holland: North-Holland Amsterdam) · 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: Summer School Pisa
[33] Reynolds, J., On the relation between direct and continuation semantics, (Loeckx, J., Proc. 2nd Internat. Colloquium on Automata, Languages and Programming, 14 (1974), Springer: Springer Berlin), 141-156, Lecture Notes in Computer Science · Zbl 0313.68023
[34] Reynolds, J., Towards a theory of type structure, (Colloque sur la Programmation, 19 (1974), Springer: Springer Berlin), 408-425, Lecture Notes in Computer Science · Zbl 0309.68016
[35] Scott, D., Continuous lattices, (Lawvere, F. W., Toposes, Algebraic Geometry and Logic, 274 (1972), Springer: Springer Berlin), 97-136, Lecture Notes in Mathematics · Zbl 0239.54006
[36] Scott, D., Domains for denotational semantics, (Nielsen, M.; Schmidt, E. M., Proc. 9th Internat. Colloquium on Automata, Languages and Programming, 140 (1982), Springer: Springer Berlin), 577-613, Lecture Notes in Computer Science · Zbl 0495.68025
[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. 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.