?

Log in

No account? Create an account

_xacid_

A Contextual Reconstruction of Monadic Reflection

A Contextual Reconstruction of Monadic Reflection

Previous Entry Share Next Entry
http://drops.dagstuhl.de/opus/volltexte/2018/9694/pdf/LIPIcs-CSL-2018-27.pdf

Toru Kawata
Department of Computer Science, The University of Tokyo, Tokyo, Japan kawata@lyon.is.s.u-tokyo.ac.jp

Abstract
With the help of an idea of contextual modal logic, we define a logical system λrefl that in-
corporates 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 λrefl , a restriction of λrefl, has exactly the same provability as λs/r , a system that incorpo- 2cont pure rates shift/reset. Our reconstruction of monadic reflection opens up a path for investigation of delimited continuations with familiar monadic language.
Powered by LiveJournal.com