eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-08-29
27:1
27:14
10.4230/LIPIcs.CSL.2018.27
article
A Contextual Reconstruction of Monadic Reflection
Kawata, Toru
1
Department of Computer Science, The University of Tokyo, Tokyo, Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol119-csl2018/LIPIcs.CSL.2018.27/LIPIcs.CSL.2018.27.pdf
Monadic Reflection
Delimited Continuations
shift/reset
Contextual Modal Logic
Curry-Howard Isomorphism