Parametric effect monads and semantics of effect systems

Shin-ya Katsumata

Research Institute for Mathematical Science (RIMS)
Kyoto University

Thursday, 28 November 2013, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: We introduce a generalisation of monads called parametric effect monads, and apply them to the interpretation of general effect systems whose effects have sequential composition operators. We show that parametric effect monads admit analogues of the structures and concepts that exist for monads, such as Kleisli triples, the state monad and the continuation monad, Plotkin and Power's algebraic operations, and the categorical TT-lifting. We also show a systematic method to generate both effects and a parametric effect monad from a monad morphism. Finally, we introduce two effect systems with explicit and implicit subeffecting, and discuss their denotational semantics and the soundness of effect systems.

ERDF
Tarmo Uustalu
Last update 23.11.2013