Document Open Access Logo

Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators

Authors Maika Fujii, Kenichi Asai

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2021.16.pdf
  • Filesize: 0.61 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Control primitives
  • Theory of computation → Lambda calculus
  • Theory of computation → Operational semantics
  • Theory of computation → Abstract machines
  • Software and its engineering → Virtual machines
Keywords
  • delimited-control operators
  • functional derivation
  • CPS transformation
  • defunctionalization
  • abstract machine
  • virtual machine

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

This paper derives an abstract machine and a virtual machine for the λ-calculus with four variants of delimited-control operators: shift/reset, control/prompt, shift₀/reset₀, and control₀/prompt₀. Starting from Shan’s definitional interpreter for the four operators, we successively apply various meaning-preserving transformations. Both trails of invocation contexts (needed for control and control₀) and metacontinuations (needed for shift₀ and control₀) are defunctionalized and eventually represented as a list of stack frames. The resulting virtual machine clearly models not only how the control operators and captured continuations behave but also when and which portion of stack frames is copied to the heap.

Cite As Get BibTex

Maika Fujii and Kenichi Asai. Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.FSCD.2021.16

Author Details

Maika Fujii
  • Ochanomizu University, Tokyo, Japan
Kenichi Asai
  • Ochanomizu University, Tokyo, Japan

Funding

  • Asai, Kenichi: supported in part by JSPS KAKENHI under Grant No. JP18H03218.

Acknowledgements

We are grateful to Youyou Cong and anonymous reviewers for their valuable comments and suggestions.

Supplementary Materials

References

  1. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From interpreter to compiler and virtual machine: a functional derivation. BRICS Report Series, 03(14), 2003. Google Scholar
  2. Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 8-19. ACM, 2003. URL: https://doi.org/10.1145/888251.888254.
  3. Kenichi Asai and Arisa Kitani. Functional derivation of a virtual machine for delimited continuations. In Temur Kutsia, Wolfgang Schreiner, and Maribel Fernández, editors, Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pages 87-98. ACM, 2010. URL: https://doi.org/10.1145/1836089.1836101.
  4. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program., 84(1):108-123, 2015. URL: https://doi.org/10.1016/j.jlamp.2014.02.001.
  5. Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A dynamic continuation-passing style for dynamic delimited continuations. ACM Trans. Program. Lang. Syst., 38(1):2:1-2:25, 2015. URL: https://doi.org/10.1145/2794078.
  6. Youyou Cong, Chiaki Ishio, Kaho Honda, and Kenichi Asai. A functional abstraction of typed invocation contexts. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 12:1-12:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.12.
  7. Olivier Danvy. Defunctionalized interpreters for programming languages. In James Hook and Peter Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 131-142. ACM, 2008. URL: https://doi.org/10.1145/1411204.1411206.
  8. Olivier Danvy and Andrzej Filinski. Abstracting control. In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP 1990, Nice, France, 27-29 June 1990, pages 151-160. ACM, 1990. URL: https://doi.org/10.1145/91556.91622.
  9. Olivier Danvy and Andrzej Filinski. Representing control: A study of the CPS transformation. Math. Struct. Comput. Sci., 2(4):361-391, 1992. URL: https://doi.org/10.1017/S0960129500001535.
  10. Olivier Danvy and Kevin Millikin. Refunctionalization at work. Sci. Comput. Program., 74(8):534-549, 2009. URL: https://doi.org/10.1016/j.scico.2007.10.007.
  11. R. Kent Dybvig, Simon L. Peyton Jones, and Amr Sabry. A monadic framework for delimited continuations. J. Funct. Program., 17(6):687-730, 2007. URL: https://doi.org/10.1017/S0956796807006259.
  12. Kavon Farvardin and John H. Reppy. From folklore to fact: comparing implementations of stacks and continuations. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 75-90. ACM, 2020. URL: https://doi.org/10.1145/3385412.3385994.
  13. Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and P. Mager, editors, Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, California, USA, January 10-13, 1988, pages 180-190. ACM Press, 1988. URL: https://doi.org/10.1145/73560.73576.
  14. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang., 1(ICFP):13:1-13:29, 2017. URL: https://doi.org/10.1145/3110257.
  15. Martin Gasbichler and Michael Sperber. Final shift for call/cc: direct implementation of shift and reset. In Mitchell Wand and Simon L. Peyton Jones, editors, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002, pages 271-282. ACM, 2002. URL: https://doi.org/10.1145/581478.581504.
  16. Carl A. Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ml-like languages. In John Williams, editor, Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995, pages 12-23. ACM, 1995. URL: https://doi.org/10.1145/224164.224173.
  17. Daniel Hillerström, Sam Lindley, and Robert Atkey. Effect handlers via generalised continuations. J. Funct. Program., 30:e5, 2020. URL: https://doi.org/10.1017/S0956796820000040.
  18. Atsushi Igarashi and Masashi Iwaki. Deriving compilers and virtual machines for a multi-level language. In Zhong Shao, editor, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings, volume 4807 of Lecture Notes in Computer Science, pages 206-221. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_14.
  19. Yukiyoshi Kameyama and Takuo Yonezawa. Typed dynamic control operators for delimited continuations. In Jacques Garrigue and Manuel V. Hermenegildo, editors, Functional and Logic Programming, 9th International Symposium, FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings, volume 4989 of Lecture Notes in Computer Science, pages 239-254. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78969-7_18.
  20. Ohad Kammar, Sam Lindley, and Nicolas Oury. Handlers in action. In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25-27, 2013, pages 145-158. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500590.
  21. Oleg Kiselyov. Delimited control in ocaml, abstractly and concretely. Theor. Comput. Sci., 435:56-76, 2012. URL: https://doi.org/10.1016/j.tcs.2012.02.025.
  22. Moe Masuko and Kenichi Asai. Caml light+ shift/reset= caml shift. Theory and Practice of Delimited Continuations (TPDC 2011), pages 33-46, 2011. Google Scholar
  23. Marek Materzok and Dariusz Biernacki. Subtyping delimited continuations. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 81-93. ACM, 2011. URL: https://doi.org/10.1145/2034773.2034786.
  24. Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Typed equivalence of effect handlers and delimited control. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 30:1-30:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.30.
  25. Gordon D. Plotkin and Matija Pretnar. Handlers of algebraic effects. In Giuseppe Castagna, editor, Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5502 of Lecture Notes in Computer Science, pages 80-94. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-00590-9_7.
  26. John C. Reynolds. Definitional interpreters for higher-order programming languages. In John J. Donovan and Rosemary Shields, editors, Proceedings of the ACM annual conference, ACM 1972, 1972, Volume 2, pages 717-740. ACM, 1972. URL: https://doi.org/10.1145/800194.805852.
  27. John C. Reynolds. Definitional interpreters for higher-order programming languages. High. Order Symb. Comput., 11(4):363-397, 1998. URL: https://doi.org/10.1023/A:1010027404223.
  28. Chung-chieh Shan. A static simulation of dynamic delimited control. High. Order Symb. Comput., 20(4):371-401, 2007. URL: https://doi.org/10.1007/s10990-007-9010-4.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact