Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Logic, Language, Information, and Computation

WoLLIC 2008: Logic, Language, Information and Computation pp 1–16Cite as

Inter-deriving Semantic Artifacts for Object-Oriented Programming

(Extended Abstract)

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 5110))

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.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. In: Monographs in Computer Science. Springer, Heidelberg (1996)

    Google Scholar 

  2. 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)

    Google Scholar 

  3. Ager, M.S.: Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (January 2006)

    Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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

    Google Scholar 

  6. 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

    Google Scholar 

  7. 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)

    Google Scholar 

  8. Biernacka, M.: A Derivational Approach to the Operational Semantics of Functional Languages. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (January 2006)

    Google Scholar 

  9. 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)

    Google Scholar 

  10. 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

    Google Scholar 

  11. 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

    Google Scholar 

  12. Biernacki, D.: The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (December 2005)

    Google Scholar 

  13. 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)

    Chapter  Google Scholar 

  14. Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)

    Google Scholar 

  15. 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)

    Google Scholar 

  16. Cousineau, G., Curien, P.-L., Mauny, M.: The Categorical Abstract Machine. Science of Computer Programming 8(2), 173–202 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  17. Curien, P.-L.: An abstract framework for environment machines. Theoretical Computer Science 82, 389–402 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  18. 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)

    Article  MATH  MathSciNet  Google Scholar 

  19. 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)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark (October 2006)

    Google Scholar 

  22. 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

    Google Scholar 

  23. 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)

    Article  MathSciNet  Google Scholar 

  24. 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

    Google Scholar 

  25. 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)

    Google Scholar 

  26. 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)

    Chapter  Google Scholar 

  27. 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)

    Google Scholar 

  28. 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

  29. 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

    Google Scholar 

  30. Johannsen, J.: Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (forthcoming, 2008)

    Google Scholar 

  31. 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/

  32. 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)

    Chapter  Google Scholar 

  33. 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)

    Google Scholar 

  34. Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)

    MATH  Google Scholar 

  35. Leroy, X.: The Zinc experiment: an economical implementation of the ML language. Rapport Technique 117, INRIA Rocquencourt, Le Chesnay, France (February 1990)

    Google Scholar 

  36. 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)

    Chapter  Google Scholar 

  37. Midtgaard, J.: Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark (June 2007)

    Google Scholar 

  38. 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)

    Google Scholar 

  39. 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)

    Google Scholar 

  40. Nielson, H.R., Nielson, F.: Semantics with Applications, a formal introduction. Wiley Professional Computing. John Wiley and Sons, Chichester (1992)

    MATH  Google Scholar 

  41. 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]

    Google Scholar 

  42. Reynolds, J.C.: Definitional interpreters revisited. Higher-Order and Symbolic Computation 11(4), 355–361 (1998)

    Article  MATH  Google Scholar 

  43. 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)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Aarhus, IT-parken, Aabogade 34, DK-8200, Aarhus N, Denmark

    Olivier Danvy & Jacob Johannsen

Authors
  1. Olivier Danvy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jacob Johannsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wilfrid Hodges Ruy de Queiroz

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation