Document Open Access Logo

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Authors Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2016.9.pdf
  • Filesize: 0.58 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • delimited continuation
  • dynamic prompt generation
  • contextual equivalence
  • environmental bisimulation
  • up-to technique

Metrics

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

Abstract

We present sound and complete environmental bisimilarities for a
variant of Dybvig et al.'s calculus of multi-prompted
delimited-control operators with dynamic prompt generation.  The
reasoning principles that we obtain generalize and advance the
existing techniques for establishing program equivalence in calculi
with single-prompted delimited control.

The basic theory that we develop is presented using Madiot et al.'s
framework that allows for smooth integration and composition of up-to
techniques facilitating bisimulation proofs. We also generalize the
framework in order to express environmental bisimulations that support
equivalence proofs of evaluation contexts representing
continuations. This change leads to a novel and powerful up-to
technique enhancing bisimulation proofs in the presence of control
operators.

Cite As Get BibTex

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.9

Author Details

Andrés Aristizábal
Dariusz Biernacki
Sergueï Lenglet
Piotr Polesiuk

References

  1. Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental bisimulations for delimited-control operators with dynamic prompt generation. Research Report RR-8905, Inria, Nancy, France, April 2016. Available at URL: http://hal.inria.fr/hal-01305137.
  2. Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In Xavier Leroy, editor, Proceedings of the Thirty-First Annual ACM Symposium on Principles of Programming Languages, pages 64-76, Venice, Italy, January 2004. ACM Press. Google Scholar
  3. Nick Benton and Vasileios Koutavas. A mechanized bisimulation for the nu-calculus. Technical Report MSR-TR-2008-129, Microsoft Research, September 2008. Google Scholar
  4. Dariusz Biernacki and Olivier Danvy. A simple proof of a folklore theorem about delimited control. Journal of Functional Programming, 16(3):269-280, 2006. Google Scholar
  5. Dariusz Biernacki and Sergueï Lenglet. Applicative bisimulations for delimited-control operators. In Lars Birkedal, editor, Foundations of Software Science and Computation Structures, 15th International Conference (FOSSACS'12), volume 7213 of Lecture Notes in Computer Science, pages 119-134, Tallinn, Estonia, March 2012. Springer. Google Scholar
  6. Dariusz Biernacki and Sergueï Lenglet. Normal form bisimulations for delimited-control operators. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming, 13th International Symposium (FLOPS'12), volume 7294 of Lecture Notes in Computer Science, pages 47-61, Kobe, Japan, May 2012. Springer. Google Scholar
  7. Dariusz Biernacki and Sergueï Lenglet. Environmental bisimulations for delimited-control operators. In Chung-chieh Shan, editor, Proceedings of the 11th Asian Symposium on Programming Languages and Systems (APLAS'13), volume 8301 of Lecture Notes in Computer Science, pages 333-348, Melbourne, VIC, Australia, December 2013. Springer. Google Scholar
  8. Dariusz Biernacki and Piotr Polesiuk. Logical relations for coherence of effect subtyping. In Thorsten Altenkirch, editor, Typed Lambda Calculi and Applications, 13th International Conference, TLCA 2015, volume 38 of Leibniz International Proceedings in Informatics, pages 107-122, Warsaw, Poland, July 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  9. Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151-160, Nice, France, June 1990. ACM Press. Google Scholar
  10. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5):477-528, 2012. Google Scholar
  11. R. Kent Dybvig, Simon Peyton-Jones, and Amr Sabry. A monadic framework for delimited continuations. Journal of Functional Programming, 17(6):687-730, 2007. Google Scholar
  12. Matthias Felleisen. The theory and practice of first-class prompts. In Jeanne Ferrante and Peter Mager, editors, Proceedings of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 180-190, San Diego, California, January 1988. ACM Press. Google Scholar
  13. Andrzej Filinski. Representing monads. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 446-457, Portland, Oregon, January 1994. ACM Press. Google Scholar
  14. Matthew Flatt, Gang Yu, Robert Bruce Findler, and Matthias Felleisen. Adding delimited and composable control to a production programming environment. In Norman Ramsey, editor, Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP'07), pages 165-176, Freiburg, Germany, September 2007. ACM Press. Google Scholar
  15. Carl Gunter, Didier Rémy, and Jon G. Riecke. A generalization of exceptions and control in ML-like languages. In Simon Peyton Jones, editor, Proceedings of the Seventh ACM Conference on Functional Programming and Computer Architecture, pages 12-23, La Jolla, California, June 1995. ACM Press. Google Scholar
  16. Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. The marriage of bisimulations and Kripke logical relations. In John Field and Michael Hicks, editors, Proceedings of the Thirty-Ninth Annual ACM Symposium on Principles of Programming Languages, pages 59-72, Philadelphia, PA, USA, January 2012. ACM Press. Google Scholar
  17. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. A logical step forward in parametric bisimulations. Technical Report MPI-SWS-2014-003, Max Planck Institute for Software Systems (MPI-SWS), Saarbrücken, Germany, January 2014. Google Scholar
  18. Yukiyoshi Kameyama and Masahito Hasegawa. A sound and complete axiomatization of delimited continuations. In Olin Shivers, editor, Proceedings of the 2003 ACM SIGPLAN International Conference on Functional Programming (ICFP'03), pages 177-188, Uppsala, Sweden, August 2003. ACM Press. Google Scholar
  19. Oleg Kiselyov. Delimited control in OCaml, abstractly and concretely: System description. In Matthias Blume and German Vidal, editors, Functional and Logic Programming, 10th International Symposium, FLOPS 2010, volume 6009 of Lecture Notes in Computer Science, pages 304-320, Sendai, Japan, April 2010. Springer. Google Scholar
  20. Ikuo Kobori, Yukiyoshi Kameyama, and Oleg Kiselyov. ATM without tears: prompt-passing style transformation for typed delimited-control operators. In Olivier Danvy, editor, 2015 Workshop on Continuations: Pre-proceedings, London, UK, April 2015. Google Scholar
  21. Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. From applicative to environmental bisimulation. In Michael Mislove and Joël Ouaknine, editors, Proceedings of the 27th Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXVII), volume 276 of Electronic Notes in Theoretical Computer Science, pages 215-235, Pittsburgh, PA, USA, May 2011. Google Scholar
  22. Vasileios Koutavas and Mitchell Wand. Bisimulations for untyped imperative objects. In Peter Sestoft, editor, 15th European Symposium on Programming, ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 146-161, Vienna, Austria, March 2006. Springer. Google Scholar
  23. Vasileios Koutavas and Mitchell Wand. Small bisimulations for reasoning about higher-order imperative programs. In J. Gregory Morrisett and Simon L. Peyton Jones, editors, Proceedings of the 33rd Annual ACM Symposium on Principles of Programming Languages, pages 141-152, Charleston, SC, USA, January 2006. ACM Press. Google Scholar
  24. Jean-Marie Madiot. Higher-Order Languages: Dualities and Bisimulation Enhancements. PhD thesis, Université de Lyon and Università di Bologna, 2015. Google Scholar
  25. Jean-Marie Madiot, Damien Pous, and Davide Sangiorgi. Bisimulations up-to: Beyond first-order transition systems. In Paolo Baldan and Daniele Gorla, editors, 25th International Conference on Concurrency Theory, volume 8704 of Lecture Notes in Computer Science, pages 93-108, Rome, Italy, September 2014. Springer. Google Scholar
  26. Adrien Piérard and Eijiro Sumii. A higher-order distributed calculus with name creation. In Proceedings of the 27th IEEE Symposium on Logic in Computer Science (LICS 2012), pages 531-540, Dubrovnik, Croatia, June 2012. IEEE Computer Society Press. Google Scholar
  27. Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. In Andrew Gordon and Andrew Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227-273. Publications of the Newton Institute, Cambridge University Press, 1998. Google Scholar
  28. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction, chapter 6, pages 233-289. Cambridge University Press, 2011. Google Scholar
  29. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1):1-69, January 2011. Google Scholar
  30. Eijiro Sumii. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In Erich Grädel and Reinhard Kahle, editors, Computer Science Logic, CSL'09, volume 5771 of Lecture Notes in Computer Science, pages 455-469, Coimbra, Portugal, September 2009. Springer. Google Scholar
  31. Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. Theoretical Computer Science, 375(1-3):169-192, 2007. Google Scholar
  32. Eijiro Sumii and Benjamin C. Pierce. A bisimulation for type abstraction and recursion. Journal of the ACM, 54(5), 2007. Google Scholar
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