Invited Talk: Semantics of Effect Systems by Graded Monads
Programs cause various side effects during their execution, and the static analysis of side effects of programs is one of the important topics in program analysis. Effect systems are a type-theoretic approach to statically estimate side effects caused by programs. In a typical effect system, the estimation is done by constructing abstract representations of a program’s side effects along typing derivations. These representations are often called “effects”.
In a seminal paper , Wadler integrated monadic types and effects into the effect-annotated monadic type T(e)(t). Wadler then raises a question of which semantic structure corresponds to the effect-annotated monadic type. In response to this question, I used a structure called graded monad to interpret the effect-annotated monadic type . In this talk, I will introduce graded monads with examples and an application to the semantics of effect systems. I will also talk about algebraic operations of graded monads, the decomposition of graded monads by an adjunction and a twist , and the graded TT-lifting of ordinary monads.
 Philip Wadler. The Marriage of Effects and Monads. ICFP 1998: 63-74
 Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. POPL 2014: 633-646
 Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès. Towards a Formal Theory of Graded Monads. FoSSaCS 2016: 513-530
Sun 3 SepDisplayed time zone: Belfast change
09:10 - 10:00
|Invited Talk: Semantics of Effect Systems by Graded Monads|
Shin-ya Katsumata National Institute of Informatics