Document Open Access Logo

A Contextual Reconstruction of Monadic Reflection

Author Toru Kawata

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2018.27.pdf
  • Filesize: 381 kB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Monadic Reflection
  • Delimited Continuations
  • shift/reset
  • Contextual Modal Logic
  • Curry-Howard Isomorphism

Metrics

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

Abstract

With the help of an idea of contextual modal logic, we define a logical system lambda^{refl} that incorporates monadic reflection, and then investigate delimited continuations through the lens of monadic reflection. Technically, we firstly prove a certain universality of continuation monad, making the character of monadic reflection a little more clear. Next, moving focus to delimited continuations, we present a macro definition of shift/reset by monadic reflection. We then prove that lambda^{refl}_{2cont}, a restriction of lambda^{refl}, has exactly the same provability as lambda^{s/r}_{pure}, a system that incorporates shift/reset. Our reconstruction of monadic reflection opens up a path for investigation of delimited continuations with familiar monadic language.

Cite As Get BibTex

Toru Kawata. A Contextual Reconstruction of Monadic Reflection. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.27

Author Details

Toru Kawata
  • Department of Computer Science, The University of Tokyo, Tokyo, Japan

References

  1. Zena Ariola, Hugo Herbelin, and Amr Sabry. A Type-Theoretic Foundation of Delimited Continuations. Higher-Order and Symbolic Computation, 2007. Google Scholar
  2. Kenichi Asai. On typing delimited continuations: three new solutions to the printf problem. Higher-Order and Symbolic Computation, 22(3):275-291, Sep 2009. URL: http://dx.doi.org/10.1007/s10990-009-9049-5.
  3. Kenichi Asai and Yukiyoshi Kameyama. Polymorphic delimited continuations. In Programming Languages and Systems, pages 239-254. Springer Berlin Heidelberg, 2007. URL: http://dx.doi.org/10.1007/978-3-540-76637-7_16.
  4. Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical report, Institute of Datalogy,University of Copenhagen, 1989. Google Scholar
  5. Matthias Felleisen, Daniel Friedman, Eugene Kohlbecker, and Bruce Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52(3):205-237, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90109-5.
  6. Mattias Felleisen. The theory and practice of first-class prompts. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '88, pages 180-190, New York, NY, USA, 1988. ACM. URL: http://dx.doi.org/10.1145/73560.73576.
  7. Andrzej Filinski. Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '94, pages 446-457. ACM, 1994. URL: http://dx.doi.org/10.1145/174675.178047.
  8. Andrzej Filinski. Monads in action. SIGPLAN Not., 45(1):483-494, 2010. URL: http://dx.doi.org/10.1145/1707801.1706354.
  9. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. Proceedings of the ACM on Programming Languages, 1(ICFP):13:1-13:29, 2017. URL: http://dx.doi.org/10.1145/3110257.
  10. Timothy Griffin. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '90, pages 47-58, New York, NY, USA, 1990. ACM. URL: http://dx.doi.org/10.1145/96709.96714.
  11. Gregory Johnson. GL - a denotational testbed with continuations and partial continuations as first-class objects. SIGPLAN Not., 22(7):165-176, 1987. URL: http://dx.doi.org/10.1145/960114.29668.
  12. Yukiyoshi Kameyama. Towards logical understanding of delimited continuations. In Continuations Workshop, pages 27-33, 2001. Google Scholar
  13. Yukiyoshi Kameyama. Axioms for delimited continuations in the CPS hierarchy. In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, pages 442-457, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30124-0_34.
  14. Yukiyoshi Kameyama and Kenichi Asai. Strong normalization of polymorphic calculus for delimited continuations. In Symbolic Computation in Software Science, 2008. Google Scholar
  15. Oleg Kiselyov and Chung-chieh Shan. A substructural type system for delimited continuations. In Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings, pages 223-239, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73228-0_17.
  16. Saul Kripke. A completeness theorem in modal logic. The Journal of Symbolic Logic, 24(1):1-14, 1959. URL: http://www.jstor.org/stable/2964568.
  17. Saul Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16(1963):83-94, 1963. Google Scholar
  18. Yuito Murase. Kripke-style contextual modal type theory. Work-in-progress report at Logical Frameworks and Meta-Languages, 2017. Google Scholar
  19. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):23:1-23:49, 2008. URL: http://dx.doi.org/10.1145/1352582.1352591.
  20. Yuichi Nishiwaki, Yoshihiko Kakutani, and Yuito Murase. Modality via iterated enrichment, 2018. arXiv:1804.02809. URL: http://arxiv.org/abs/arXiv:1804.02809.
  21. Michel Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. Lecture Notes in Computer Science, 624:190-201, 1992. URL: http://dx.doi.org/10.1007/BFb0013061.
  22. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511-540, aug 2001. URL: http://dx.doi.org/10.1017/S0960129501003322.
  23. Willard Quine. Reference and modality. In Journal of Symbolic Logic, pages 139-159. Harvard University Press, 1953. Google Scholar
  24. Noam Zeilberger. Polarity and the logic of delimited continuations. In Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science, LICS '10, pages 219-227, Washington, DC, USA, 2010. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.2010.23.
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