Abstract
We present a new abstract machine for Abadi and Cardelli’s untyped calculus of objects. What is special about this semantic artifact (i.e., man-made construct) is that is mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli’s monograph. This abstract machine therefore embodies the soundness of Abadi and Cardelli’s reduction semantics and natural semantics relative to each other.
To move closer to actual implementations, which use environments rather than actual substitutions, we then represent object methods as closures and in the same inter-derivational spirit, we present three new semantic artifacts: a reduction semantics for a version of Abadi and Cardelli’s untyped calculus of objects with explicit substitutions, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and furthermore, they are coherent with the previous ones since as we show, the two abstract machines are bisimilar. Overall, though, the significance of these artifacts lies in them not having been designed from scratch and then proved correct: instead, they were mechanically inter-derived.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cardelli, L.: A Theory of Objects. In: Monographs in Computer Science. Springer, Heidelberg (1996)
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991); A preliminary version was presented at the Seventeenth Annual ACM Symposium on Principles of Programming Languages (POPL 1990) (1990)
Ager, M.S.: Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (January 2006)
Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondence between evaluators and abstract machines. In: Miller, D. (ed.) Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003), Uppsala, Sweden, August 2003, pp. 8–19. ACM Press, New York (2003)
Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between call-by-need evaluators and lazy abstract machines. Information Processing Letters 90(5), 223–232 (2004); Extended version available as the research report BRICS RS-04-3
Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science 342(1), 149–172 (2005); Extended version available as the research report BRICS RS-04-28
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundation of Mathematics, vol. 103, revised edn. North-Holland, Amsterdam (1984)
Biernacka, M.: A Derivational Approach to the Operational Semantics of Functional Languages. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (January 2006)
Biernacka, M., Biernacki, D., Danvy, O.: An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science 1(2:5), 1–39 (2005); A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW 2004) (2004)
Biernacka, M., Danvy, O.: A concrete framework for environment machines. ACM Transactions on Computational Logic 9(1), 1–30, Article #6 (2007); Extended version available as the research report BRICS RS-06-3
Biernacka, M., Danvy, O.: A syntactic correspondence between context-sensitive calculi and abstract machines. Theoretical Computer Science 375(1-3), 76–108 (2007); Extended version available as the research report BRICS RS-06-18
Biernacki, D.: The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (December 2005)
Cardelli, L.: Compiling a functional language. In: Steele Jr., G.L. (ed.) Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, Austin, Texas, August 1984, pp. 208–217. ACM Press, New York (1984)
Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)
Consel, C., Danvy, O.: Tutorial notes on partial evaluation. In: Graham, S.L. (ed.) Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993, pp. 493–501. ACM Press, New York (1993)
Cousineau, G., Curien, P.-L., Mauny, M.: The Categorical Abstract Machine. Science of Computer Programming 8(2), 173–202 (1987)
Curien, P.-L.: An abstract framework for environment machines. Theoretical Computer Science 82, 389–402 (1991)
Curien, P.-L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM 43(2), 362–397 (1996)
Danvy, O.: Back to direct style. Science of Computer Programming 22(3), 183–195 (1994); A preliminary version was presented at the Fourth European Symposium on Programming (ESOP 1992) (1992)
Danvy, O.: From reduction-based to reduction-free normalization. In: Antoy, S., Toyama, Y. (eds.) Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004), Invited talk, Aachen, Germany, May 2004. Electronic Notes in Theoretical Computer Science, vol. 124(2), pp. 79–100. Elsevier Science, Amsterdam (2004)
Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark (October 2006)
Danvy, O., Millikin, K.: Refunctionalization at work. Science of Computer Programming (in press); A preliminary version is available as the research report BRICS RS-07-7
Danvy, O., Millikin, K.: On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Information Processing Letters 106(3), 100–109 (2008)
Danvy, O., Nielsen, L.R.: Defunctionalization at work. In: Søndergaard, H. (ed.) Proceedings of the Third International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), Firenze, Italy, September 2001, pp. 162–174. ACM Press, New York (2001); Extended version available as the research report BRICS RS-01-23
Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (November 2004); A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science 59(4)
Dybvig, R.K.: The development of Chez Scheme. In: Lawall, J.L. (ed.) Proceedings of the 2006 ACM SIGPLAN International Conference on Functional Programming (ICFP 2006), Keynote talk, Portland, Oregon, September 2006. SIGPLAN Notices, vol. 41(9), pp. 1–12. ACM Press, New York (2006)
Felleisen, M.: The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana (August 1987)
Felleisen, M., Flatt, M.: Programming languages and lambda calculi (1989-2001) (last accessed, April 2008), unpublished lecture notes available at http://www.ccs.neu.edu/home/matthias/3810-w02/readings.html
Gordon, A.D., Hankin, P.D., Lassen, S.B.: Compilation and equivalence of imperative objects. Journal of Functional Programming 9(4), 373–426 (1999); Extended version available as the technical report BRICS RS-97-19
Johannsen, J.: Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (forthcoming, 2008)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall International, London (1993), http://www.dina.kvl.dk/~sestoft/pebook/
Kahn, G.: Natural semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)
Kesner, D., López, P.E.M.: Explicit substitutions for objects and functions. Journal of Functional and Logic Programming Special issue 2 (1999); A preliminary version was presented at PLILP 1998/ALP 1998 (1998)
Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)
Leroy, X.: The Zinc experiment: an economical implementation of the ML language. Rapport Technique 117, INRIA Rocquencourt, Le Chesnay, France (February 1990)
Marlow, S., Peyton Jones, S.L.: Making a fast curry: push/enter vs. eval/apply for higher-order languages. In: Fisher, K. (ed.) Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP 2004), Snowbird, Utah, September 2004. SIGPLAN Notices, vol. 39(9), pp. 4–15. ACM Press, New York (2004)
Midtgaard, J.: Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (June 2007)
Millikin, K.: A Structured Approach to the Transformation, Normalization and Execution of Computer Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (May 2007)
Nielsen, L.R.: A study of defunctionalization and continuation-passing style. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, BRICS DS-01-7 (July 2001)
Nielson, H.R., Nielson, F.: Semantics with Applications, a formal introduction. Wiley Professional Computing. John Wiley and Sons, Chichester (1992)
Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of 25th ACM National Conference, Boston, Massachusetts, pp. 717–740 (1972); reprinted in Higher-Order and Symbolic Computation 11(4), 363–397 (1998) with a foreword [42]
Reynolds, J.C.: Definitional interpreters revisited. Higher-Order and Symbolic Computation 11(4), 355–361 (1998)
Rose, K.H.: Explicit substitution – tutorial & survey. BRICS Lecture Series LS-96-3, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (September 1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danvy, O., Johannsen, J. (2008). Inter-deriving Semantic Artifacts for Object-Oriented Programming. In: Hodges, W., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2008. Lecture Notes in Computer Science(), vol 5110. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69937-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-69937-8_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69936-1
Online ISBN: 978-3-540-69937-8
eBook Packages: Computer ScienceComputer Science (R0)