Skip to main content
SpringerLink
Log in
Book cover

Semantics and Algebraic Specification pp 162–185Cite as

Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5700))

Abstract

We derive two big-step abstract machines, a natural semantics, and the valuation function of a denotational semantics based on the small-step abstract machine for Core Scheme presented by Clinger at PLDI’98. Starting from a functional implementation of this small-step abstract machine, (1) we fuse its transition function with its driver loop, obtaining the functional implementation of a big-step abstract machine; (2) we adjust this big-step abstract machine so that it is in defunctionalized form, obtaining the functional implementation of a second big-step abstract machine; (3) we refunctionalize this adjusted abstract machine, obtaining the functional implementation of a natural semantics in continuation-passing style; and (4) we closure-unconvert this natural semantics, obtaining a compositional continuation-passing evaluation function which we identify as the functional implementation of a denotational semantics in continuation-passing style. We then compare this valuation function with that of Clinger’s original denotational semantics of Scheme.

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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
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. Ager, M.S.: Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark (January 2006)

    Google Scholar 

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

    Google Scholar 

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

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

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  8. Biernacka, M., Danvy, O.: Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part II: Reduction Semantics and Abstract Machines. In: Palsberg, J. (ed.) Mosses’s Festschrift. LNCS, vol. 5700, pp. 186–206. Springer, Heidelberg (2009)

    Google Scholar 

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

    Google Scholar 

  10. Biernacki, D., Danvy, O.: From interpreter to logic engine by defunctionalization. In: Bruynooghe, M. (ed.) LOPSTR 2003. LNCS, vol. 3018, pp. 143–159. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Clinger, W., Friedman, D.P., Wand, M.: A scheme for a higher-level semantic algebra. In: Reynolds, J., Nivat, M. (eds.) Algebraic Methods in Semantics, pp. 237–250. Cambridge University Press, Cambridge (1985)

    Google Scholar 

  12. Clinger, W., Hartheimer, A.H., Ost, E.M.: Implementation strategies for first-class continuations. Higher-Order and Symbolic Computation 12(1), 7–45 (1999); A preliminary version was presented at the 1988 ACM Conference on Lisp and Functional Programming

    Article  MATH  Google Scholar 

  13. Clinger, W., Rees, J. (eds.): Revised4 report on the algorithmic language Scheme. LISP Pointers IV(3), 1–55 (1991)

    Article  Google Scholar 

  14. Clinger, W.D.: Proper tail recursion and space efficiency. In: Cooper, K.D. (ed.) Proceedings of the ACM SIGPLAN 1998 Conference on Programming Languages Design and Implementation, Montréal, Canada, pp. 174–185. ACM Press, New York (1998)

    Chapter  Google Scholar 

  15. Danvy, O.: Formalizing implementation strategies for first-class continuations. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 88–103. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Danvy, O.: A rational deconstruction of Landin’s SECD machine. In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds.) IFL 2004. LNCS, vol. 3474, pp. 52–71. Springer, Heidelberg (2004); Recipient of the 2004 Peter Landin prize. Extended version available as the research report BRICS RS-03-33

    Chapter  Google Scholar 

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

    Google Scholar 

  18. Danvy, O., Filinski, A.: Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  19. Danvy, O., Millikin, K.: Refunctionalization at work. Research Report BRICS RS-08-4, Department of Computer Science, Aarhus University, Aarhus, Denmark (August 2007); To appear in Science of Computer Programming, extended version

    Google Scholar 

  20. 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  MATH  Google Scholar 

  21. Danvy, O., Millikin, K.: Refunctionalization at Work. Science of Computer Programming 74(8), 534–549 (2009); Extended version available as the research report BRICS SCP09

    Article  MathSciNet  MATH  Google Scholar 

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

  23. Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University, 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, vol. 59.4 (2001)

    Google Scholar 

  24. Danvy, O., Yang, Z.: An operational investigation of the CPS hierarchy. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 224–242. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  25. de Bruin, A., de Vink, E.P.: Continuation semantics for Prolog with cut. In: Díaz, J., Orejas, F. (eds.) TAPSOFT 1989. LNCS, vol. 351, pp. 178–192. Springer, Heidelberg (1989)

    Google Scholar 

  26. Felleisen, M., Flatt, M.: Programming languages and lambda calculi (1989-2001) (unpublished lecture notes), http://www.ccs.neu.edu/home/matthias/3810-w02/readings.html (last accessed in April 2008)

  27. Felleisen, M., Friedman, D.P.: Control operators, the SECD machine, and the λ-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 193–217. Elsevier Science Publishers B.V (North-Holland), Amsterdam (1986)

    Google Scholar 

  28. Gasbichler, M., Knauel, E., Sperber, M.: How to add threads to a sequential language without getting tangled up. In: Flatt, M. (ed.) Proceedings of the Fourth ACM SIGPLAN Workshop on Scheme and Functional Programming, Technical report UUCS-03-023, School of Computing, University of Utah, Boston, Massachusetts, November 2003, pp. 30–47 (2003)

    Google Scholar 

  29. Griffin, T.G.: A formulae-as-types notion of control. In: Hudak, P. (ed.) Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, January 1990, pp. 47–58. ACM Press, New York (1990)

    Google Scholar 

  30. Harper, R., Duba, B.F., MacQueen, D.: Typing first-class continuations in ML. Journal of Functional Programming 3(4), 465–484 (1993); A preliminary version was presented at the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL 1991)

    Article  Google Scholar 

  31. Haynes, C.T., Friedman, D.P., Wand, M.: Continuations and coroutines. In: Steele Jr., G.L. (ed.) Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, Austin, Texas, August 1984, pp. 293–298. ACM Press, New York (1984)

    Chapter  Google Scholar 

  32. Hieb, R., Dybvig, R.K., Bruggeman, C.: Representing control in the presence of first-class continuations. In: Lang, B. (ed.) Proceedings of the ACM SIGPLAN 1990 Conference on Programming Languages Design and Implementation, White Plains, June 1990. SIGPLAN Notices, vol. 25(6), pp. 66–77. ACM Press, New York (1990)

    Chapter  Google Scholar 

  33. Johannsen, J.: An investigation of Abadi and Cardelli’s untyped calculus of objects. Master’s thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark, BRICS research report RS-08-6 (June 2008)

    Google Scholar 

  34. Kelsey, R., Clinger, W., Rees, J.: Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation 11(1), 7–105 (1998)

    Article  Google Scholar 

  35. Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3), 199–207 (2007)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  37. 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), September 2004. SIGPLAN Notices, vol. 39(9), pp. 4–15. ACM Press, New York (2004)

    Google Scholar 

  38. Matthews, J., Findler, R.B.: An operational semantics for Scheme. Journal of Functional Programming 18(1), 47–86 (2008)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  40. Millikin, K.: A Structured Approach to the Transformation, Normalization and Execution of Computer Programs. PhD thesis, BRICS PhD School, Aarhus University, Aarhus, Denmark (May 2007)

    Google Scholar 

  41. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)

    Google Scholar 

  42. Munk, J.: A study of syntactic and semantic artifacts and its application to lambda definability, strong normalization, and weak normalization in the presence of state. Master’s thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark, BRICS research report RS-08-3 (May 2007)

    Google Scholar 

  43. Nielsen, L.R.: A study of defunctionalization and continuation-passing style. PhD thesis, BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark (July 2001) BRICS DS-01-7

    Google Scholar 

  44. Ohori, A., Sasano, I.: Lightweight fusion by fixed point promotion. In: Felleisen, M. (ed.) Proceedings of the Thirty-Fourth Annual ACM Symposium on Principles of Programming Languages, January 2007. SIGPLAN Notices, vol. 42(1), pp. 143–154. ACM Press, New York (2007)

    Google Scholar 

  45. Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  46. Ramsdell, J.D.: An operational semantics for Scheme. LISP Pointers V(2), 6–10 (1992)

    Article  Google Scholar 

  47. Rees, J., Clinger, W. (eds.): Revised3 report on the algorithmic language Scheme. SIGPLAN Notices 21(12), 37–79 (1986)

    Article  Google Scholar 

  48. 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 [50]

    Google Scholar 

  49. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation 11(4), 363–397 (1998); Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword [50]

    Article  MATH  Google Scholar 

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

    Article  MATH  Google Scholar 

  51. Sperber, M., Kent Dybvig, R., Flatt, M., van Straaten, A. (eds.): Revised6 report on the algorithmic language Scheme (September 2007), http://www.r6rs.org/

  52. Steele Jr., G.L.: Rabbit: A compiler for Scheme. Master’s thesis, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, Technical report AI-TR-474 (May 1978)

    Google Scholar 

  53. Steele Jr., G.L., Sussman, G.J.: The revised report on Scheme, a dialect of Lisp. AI Memo 452, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts (January 1978)

    Google Scholar 

  54. Sussman, G.J., Steele Jr., G.L.: Scheme: An interpreter for extended lambda calculus. AI Memo 349, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts (December 1975); Reprinted in Higher-Order and Symbolic Computation 11(4), 405–439 (1998), with a foreword [55]

    Google Scholar 

  55. Sussman, G.J., Steele Jr., G.L.: The first report on Scheme revisited. Higher-Order and Symbolic Computation 11(4), 399–404 (1998)

    Article  MATH  Google Scholar 

  56. Wadler, P.: The essence of functional programming (invited talk). In: Appel, A.W. (ed.) Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 1992, pp. 1–14. ACM Press, New York (1992)

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Olivier Danvy

Authors
  1. Olivier Danvy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of California, Los Angeles, 4531K Boelter Hall, 90095-1596, Los Angeles, CA, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Danvy, O. (2009). Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines . In: Palsberg, J. (eds) Semantics and Algebraic Specification. Lecture Notes in Computer Science, vol 5700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04164-8_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04164-8_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04163-1

  • Online ISBN: 978-3-642-04164-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation