Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part II: Reduction Semantics and Abstract Machines
We present a context-sensitive reduction semantics for a lambda-calculus with explicit substitutions and we show that the functional implementation of this small-step semantics mechanically corresponds to that of the abstract machine for Core Scheme presented by Clinger at PLDI’98, including first-class continuations. Starting from this reduction semantics, (1) we refocus it into a small-step abstract machine; (2) we fuse the transition function of this abstract machine with its driver loop, obtaining a big-step abstract machine which is staged; (3) we compress its corridor transitions, obtaining an eval/continue abstract machine; and (4) we unfold its ground closures, which yields an abstract machine that essentially coincides with Clinger’s machine. This lambda-calculus with explicit substitutions therefore aptly accounts for Core Scheme, including Clinger’s permutations and unpermutations.
KeywordsAbstract Machine Denotational Semantic Reduction Sequence Core Scheme Permutation Generator
Unable to display preview. Download preview PDF.
- 2.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
- 7.Curien, P.-L.: Categorical Combinators, Sequential Algorithms and Functional Programming. In: Progress in Theoretical Computer Science. Birkhauser, Basel (1993)Google Scholar
- 8.Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark (October 2006)Google Scholar
- 9.Danvy, O.: From reduction-based to reduction-free normalization. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832. Springer, Heidelberg (2009)Google Scholar
- 10.Danvy, O.: Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines. In: Palsberg, J. (ed.) Mosses Festschrift. LNCS, vol. 5700, pp. 162–185. Springer, Heidelberg (2009)Google Scholar
- 13.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.4Google Scholar
- 14.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
- 16.Marlow, S., Peyton Jones, S.L.: Making a fast curry: push/enter vs. eval/apply for higher-order languages. Journal of Functional Programming 16(4-5), 415–449 (2006); A preliminary version was presented at the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP 2004)MathSciNetCrossRefzbMATHGoogle Scholar
- 20.Strachey, C.: Fundamental concepts in programming languages. In: International Summer School in Computer Programming, Copenhagen, Denmark (August 1967); Reprinted in Higher-Order and Symbolic Computation 13(1/2), 11–49 (2000) with a foreword Google Scholar
- 21.Strachey, C., Wadsworth, C.P.: Continuations: A mathematical semantics for handling full jumps. Technical Monograph PRG-11, Oxford University Computing Laboratory, Programming Research Group, Oxford, England (1974); Reprinted in Higher-Order and Symbolic Computation 13(1/2), 135–152 (2000) with a foreword Google Scholar