Skip to main content
SpringerLink
Log in

A semantics for λ &-early: a calculus with overloading and early binding

Extended abstract

  • Conference paper
  • First Online:
Typed Lambda Calculi and Applications (TLCA 1993)

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

Included in the following conference series:

Abstract

The role of λ-calculus as core functional language is due to its nature as “pure” theory of functions. In the present approach we use the functional expressiveness of typed λ-calculus and extend it with our understanding of some relevant features of a broadly used programming style: Object Oriented Programming (OOP). The core notion we focus on, yields a form of “dependency on input types” (or “on the types of the inputs”) and formalizes “overloading” as implicitly used in OOP.

The basis of this work has been laid in [CGL92a], where the main syntactic properties of this extension have been shown. In this paper, we investigate an elementary approach to its mathematical meaning. The approach is elementary, as we tried to follow the most immediate semantic intuition which underlies our system, and yet provide a rigorous mathematical model. Indeed, our semantics provides an understanding of a slightly modified version of the system in [CGL92a]: we had, so far, to restrict our attention only to “early binding”.

In order to motivate our extended λ-calculus, we first survey the key features in OOP which inspired our work. Then we summarize the system presented in [CGL92a] and introduce the variant with “early binding”. Finally we present the model.

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. M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. In Ann. ACM Symp. on Principles of Programming Languages. ACM, ACM-press, 1993. Extended abstract.

    Google Scholar 

  2. H Aït-Kaci and A. Podelski. Towards a meaning of LIFE. Technical Report 11, Digital, Paris Research Laboratory, June 1991.

    Google Scholar 

  3. A. Asperti and G. Longo. Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT-Press, 1991.

    Google Scholar 

  4. R. Amadio. Domains in a realizability framework. Technical Report 19, Laboratoire d'Informatique, Ecole Normale Supérieure-Paris, 1990.

    Google Scholar 

  5. K.B. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87(1/2):196–240, 1990. A preliminary version can be found in 3rd Ann. Symp. on Logic in Computer Science, 1988.

    Google Scholar 

  6. K.B. Bruce. The equivalence of two semantic definitions of inheritance in object-oriented languages. In Proceedings of the 6th International Conference on Mathematical Foundation of Programming Semantics, 1991. to appear.

    Google Scholar 

  7. Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. A first version can be found in Semantics of Data Types, LNCS 173, 51–67, Springer-Verlag, 1984.

    Google Scholar 

  8. P.S. Canning, W.R. Cook, W.L. Hill, J. Mitchell, and W.G. Orthoff. F-bounded quantification for object-oriented programming. In ACM Conference on Functional Programming and Computer Architecture, September 1989.

    Google Scholar 

  9. G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. In ACM Conference on LISP and Functional Programming, pages 182–192, San Francisco, July 1992. ACM Press. Extended abstract.

    Google Scholar 

  10. G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. Technical Report 92–4, Laboratoire d'Informatique, Ecole Normale Supérieure-Paris, February 1992.

    Google Scholar 

  11. W.R. Cook, W.L. Hill, and P.S. Canning. Inheritance is not subtyping. 17th Ann. ACM Symp. on Principles of Programming Languages, January 1990.

    Google Scholar 

  12. L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417–458, 1991.

    Google Scholar 

  13. L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Software, pages 750–771. Springer-Verlag, September 1991. LNCS 526 (preliminary version). To appear in Information and Computation.

    Google Scholar 

  14. L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. Computing Surveys, 17(4):471–522, December 1985.

    Google Scholar 

  15. G. Ghelli. Modelling features of object-oriented languages in second order functional languages with subtypes. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, number 489 in LNCS, pages 311–340, Berlin, 1991. Springer-Verlag.

    Google Scholar 

  16. G. Ghelli. A static type system for message passing. In Proc. of OOPSLA '91, 1991.

    Google Scholar 

  17. J-Y. Girard. Interprétation fouctionelle et élimination des coupures dans l'arithmetique d'ordre supérieur. Thèse de doctorat d'état, 1972. Université Paris VII.

    Google Scholar 

  18. Joseph Goguen and José Meseguer. EQLOG: equality, types and generic modules for logic programming. In deGroot and Lindstrom, editors, Functional and Logic Programming. Prentice-Hall, 1985.

    Google Scholar 

  19. J.A. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Technical Report SRI-CSL-89-10, Computer Science Laboratory, SRI International, July 1989.

    Google Scholar 

  20. S.K. Keene. Object-Oriented Programming in Common Lisp: A Programming Guide to CLOS. Addison-Wesley, 1989.

    Google Scholar 

  21. G. Longo and E. Moggi. Constructive natural deduction and its ω-set interpretation. Mathematical Structures in Computer Science, 1(2):215–253, 1991.

    Google Scholar 

  22. G Longo, K. Milsted, and S. Soloviev. The genericity theorem and parametricity in functional languages. Technical report, Digital, Paris Reserch Lab., 1992.

    Google Scholar 

  23. Bertrand Meyer. Object-Oriented Software Construction. Prentice-Hall International Series, 1988.

    Google Scholar 

  24. NeXT Computer Inc. NeXTstep-concepts. Chapter 3: Object-Oriented Programming and Objective-C, 2.0 edition, 1991.

    Google Scholar 

  25. B.C. Pierce. Type-theoretic foundations for object-oriented programming. Technical report, LFCS, Departement of Computer Science, University of Edinburgh, May 1992. Lecture note for a short course.

    Google Scholar 

  26. B.C. Pierce and D.N. Turner. Object-oriented programming without recursive types. In 10th Ann. ACM Symp. on Principles of Programming Languages. ACM-Press, 1993.

    Google Scholar 

  27. D. Rémy. Typechecking records and variants in a natural extension of ML. In Ann. ACM Symp. on Principles of Programming Languages, 1989.

    Google Scholar 

  28. J.C. Reynolds. Polymorphism is not set-theoretic. LNCS, 173, 1984.

    Google Scholar 

  29. D. Scott. Data-types as lattices. S. I. A. M. J. Comp., 5:522–587, 1976.

    Google Scholar 

  30. Mitchell Wand. Complete type inference for simple objects. In 2nd Ann. Symp. on Logic in Computer Science, 1987.

    Google Scholar 

  31. Mitchell Wand. Type inference for record concatenation and multiple inheritance. In 4th Ann. Symp. on Logic in Computer Science, 1989.

    Google Scholar 

  32. Philip Wadler and Stephen Blott. How to make “ad-hoc” polymorphism less “ad-hoc”. In 16th Ann. ACM Symp. on Principles of Programming Languages, pages 60–76, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DISI (Univ. Genova), Italy

    Giuseppe Castagna

  2. LIENS-DMI, Paris

    Giuseppe Castagna

  3. Dipartimento d'Informatica, Corso Italia 40, Pisa, Italy

    Giorgio Ghelli

  4. Ecole Normale Sup., LIENS(CNRS)-DMI, 45 rue d'Ulm, Paris, France

    Giuseppe Longo

Authors
  1. Giuseppe Castagna
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giorgio Ghelli
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Giuseppe Longo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Marc Bezem Jan Friso Groote

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Castagna, G., Ghelli, G., Longo, G. (1993). A semantics for λ &-early: a calculus with overloading and early binding. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037101

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56517-8

  • Online ISBN: 978-3-540-47586-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation