Abstract
In this paper, we give a general framework for the foundation of an operational (small step) semantics of object-based languages with an emphasis on functional and imperative issues. The framework allows classifying very naturally many object-based calculi according to their main implementation techniques of inheritance, namely delegation and embedding, and their particular strategies. This distinction comes easily from a choice in the rules. Our framework is founded on two previous works: λObj/+, a version of the Lambda Calculus of Objects of Fischer, Honsell, and Mitchell, for the object aspects, and λσaw of Benaissa, Lescanne, and Rose, for the description of the operational semantics and sharing. The former is the formalization of a small delegation-based language which contains both lambda calculus and object primitives to create, update, and send messages to objects, while the latter is designed to provide a generic description of functional language implementations and is based on a calculus of explicit substitution extended with addresses to deal with memory management. The framework is presented as a set of modules, each of which captures a particular aspect of object-calculi (functional vs. imperative, delegation vs. embedding, and any combination of them). Above all, it introduces and illustrates a new promising approach to formally reason about the operational semantics of languages with (possibly) mutable states.
Acknowledgement
The authors are grateful to Zine-El-Abidine Benaissa, Furio Honsell, and Kristoffer H∅gsbro Rose for their useful comments on this work.
Chapter PDF
Similar content being viewed by others
Keywords
References
M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991.
Z.-E.-A. Benaissa. Les calculs de substitutions explicites comme fondement de l’implantation des langages fonctionnels. PhD thesis, Université Henri Poincaré Nancy 1, 1997. In french.
Z.-E.-A. Benaissa, K.H. Rose, and P. Lescanne. Modeling sharing and recursion for weak reduction strategies using explicit substitution. In Proc. of PLILP, number 1140 in Lecture Notes in Computer Science, pages 393–407. Springer-Verlag, 1996.
V. Bono and K. Fisher. An imperative first-order calculus with object extension. In Proc. of ECOOP, volume 1445 of Lecture Notes in Computer Science, pages 462–497. Springer-Verlag, 1998.
L. Cardelli. A language with distributed scope. Computing Systems, 8(1):27–59, 1995.
C. Chambers. The Cecil language specification, and rationale. Technical Report 93-03-05, University of Washington, Department of Computer Science and Engineering, 1993.
P.-L. Curien, T. Hardin, and J.-J. Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, 1996.
P. Di Gianantonio, F. Honsell, and L. Liquori. A lambda calculus of objects with self-inflicted extension. In Proc. of OOPSLA, pages 166–178. The ACM Press, 1998.
M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 102, 1992.
K. Fisher, F. Honsell, and J. C. Mitchell. A lambda calculus of objects and method specialization. Nordic Journal of Computing, 1(1):3–37, 1994.
F. Lang. Modèles de la ß-réduction pour les implantations. PhD thesis, École Normale Supérieure de Lyon, 1998. In french.
F. Lang, D. Dougherty, P. Lescanne, and K. H. Rose. Addressed term rewriting systems. Research Report RR 1999-30, Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon, 1999.
F. Lang, P. Lescanne, and L. Liquori. A framework for defining object calculi. Research Report RR 1998-51, Laboratoire de l’Informatique du Parallélisme, École Normale Supérieure de Lyon, 1998.
P. Lescanne. From λσ to λυ, a journey through calculi of explicit substitutions. In Proc. of POPL, pages 60–69, 1994.
T. Lindholm and F. Yellin. The Java Virtual Machine specification. Addison-Wesley Publishing Company, 1996.
J. Peterson, K. Hammond, L. Augustsson, B. Boutel, W. Burton, J. Fasel, A. Gordon, J. Hughes, P. Hudak, T. Johnsson, M. Jones, E. Meijer, S. Peyton Jones, A. Reid, and P. Wadler. Haskell 1.4, a non strict purely functional language, 1997.
K. H. Rose. Operational reduction models for functional programming languages. PhD thesis, DIKU, K∅benhavn, 1996.
A. Tailvalsaari. Kevo, a prototype-based object-oriented language based on concatenation and modules operations. Technical Report LACIR 92-02, University of Victoria, 1992.
M. Tofte. Type inference for polymorphic references. Information and Computation, 89(1):1–34, 1990.
D. A. Turner. A new implementation technique for applicative languages. Software Practice and Experience, 9:31–49, 1979.
D. Ungar and B. Smith, R. Self: the power of simplicity. In Proc. of OOPSLA, pages 227–241. The ACM Press, 1987.
C. P. Wadsworth. Semantics and pragmatics of the lambda calculus. PhD thesis, Oxford, 1971.
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38–94, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lang, F., Lescanne, P., Liquori, L. (1999). A framework for defining Object-Calculi extended abstract. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_2
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive