Relational semantics for recursive types and bounded quantification | SpringerLink
Skip to main content
Springer Nature Link
Log in

Relational semantics for recursive types and bounded quantification

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1989)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 372))

Included in the following conference series:

Abstract

The language Fun [Cardelli, Wegner, 1985] is a typed polymorphic lambda calculus with record types, quantification over subtypes of a given type and inheritance. In this paper it is extended with recursive types, and the consistency of the resulting language is proved by constructing an interpretation of its types as partial equivalence relations of a special kind, terms being interpreted as equivalence classes, modulo such relations, of elements of a model of the underlying language of untyped terms.

Research supported by EEC Joint Collaboration Contract ST2-0374-C (EDB) and 40% M.P.I.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A fixed point extension of the second order lambda calculus: observable equivalences and models, Proc. Symposium on Logic in Computer Science, IEEE, pp. 51–60

    Google Scholar 

  2. Recursion over realizability structures, unpublished, November 1988

    Google Scholar 

  3. The lambda calculus; its syntax and semantics, IIo edition, North Holland

    Google Scholar 

  4. Extensional models for polymorphism, Theoretical Computer Science, 59, pp. 85–114.

    Article  Google Scholar 

  5. Communication on the Types e-mailing list, September 1988

    Google Scholar 

  6. Inheritance and explicit coercion, to appear in Proc. Symposium on Logic in Computer Science, IEEE, 1989

    Google Scholar 

  7. A modest model of Records, Inheritance and Bounded Quantification, Proc. Symposium on Logic in Computer Science, IEEE, pp. 38–50

    Google Scholar 

  8. The semantics of second order lambda-calculus, to appear in Information and Computation

    Google Scholar 

  9. A Semantics of Multiple Inheritance, Information and Computation, 76, 1988, pp. 138–164

    Article  Google Scholar 

  10. A Quest Preview, Internal Report, DEC SRC, Jan. 1988

    Google Scholar 

  11. Structural Subtyping and the notion of Power Type, Proc. 15o ACM Symp. on Principles of Programming Languages, pp. 70–79

    Google Scholar 

  12. On understanding types, data abstraction, and polymorphism, ACM Computing Surveys, 17, Dec. 1985, pp. 471–522

    Article  Google Scholar 

  13. A completeness theorem for recursively defined types, Proc. 12th International Colloquium on Automata, Languages and Programming (Brauer, W. ed), Springer LNCS 194, 1985, pp. 120–129

    Google Scholar 

  14. Type inference and logical relations, Proc. Symposium on Logic in Computer Science, IEEE, pp. 218–226

    Google Scholar 

  15. Simula, an Algol-based simulation language, Communications ACM, 9, 1966, pp. 671–678

    Article  Google Scholar 

  16. Interpretation fonctionelle et elimination des coupures dans l'arithmetique d'ordre superieur, These de Doctorat d'Etat, Paris VII

    Google Scholar 

  17. Smalltalk-80: The Language and its Implementation, Addison-Wesley, 1983

    Google Scholar 

  18. Constructive Natural Deduction and its Modest Interpretation, CMU Report CS-88-131

    Google Scholar 

  19. An ideal model for recursive polymorphic types, Information and Control 71(1/2), pp. 95–130

    Article  Google Scholar 

  20. Modelli non estensionali del polimorfismo in programmazione funzionale, Tesi di Dottorato, Universita' di Pisa, 1988

    Google Scholar 

  21. Coercion and type inference, Proceedings 11th ACM Symposium on Principles of Programming Languages, pp. 175–185

    Google Scholar 

  22. Type inference and type containment, Information and Computation, 76, 1988, pp. 211–249

    Article  Google Scholar 

  23. A type inference approach to reduction properties and semantics of polymorphic expressions, Proceedings of ACM Conference on LISP and Functional Programming, Boston, pp. 308–319

    Google Scholar 

  24. Communication on the Types e-mailing list, January 1986

    Google Scholar 

  25. On the relation between direct and continuation semantics, Proc. 2nd International Colloquium on Automata, Languages and Programming (Loeckx, J., ed), Springer LNCS 14, 1974, pp. 141–156

    Google Scholar 

  26. Towards a theory of type structure, Colloque sur la Programmation, LNCS 19, Springer-Verlag, pp. 408–425

    Google Scholar 

  27. Continuous Lattices, in: Toposes, Algebraic Geometry and Logic (F.W. Lawvere, ed.), Springer LNM 274, 1972, pp. 97–136

    Google Scholar 

  28. Domains for Denotational Semantics, Proc. 9th international Colloquium on Automata, Languages and Programming( M.Nielsen, E.M.Schmidt eds.), Springer LNCS 140, 1982, pp. 577–613

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Informatica, Universita' di Torino, C.so Svizzera 185, I-10149, Torino

    Felice Cardone

Authors
  1. Felice Cardone
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Giorgio Ausiello Mariangiola Dezani-Ciancaglini Simonetta Ronchi Della Rocca

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cardone, F. (1989). Relational semantics for recursive types and bounded quantification. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds) Automata, Languages and Programming. ICALP 1989. Lecture Notes in Computer Science, vol 372. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035759

Download citation

  • DOI: https://doi.org/10.1007/BFb0035759

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51371-1

  • Online ISBN: 978-3-540-46201-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation