Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sun 3 Sep 2017 09:10 - 10:10 at L3 - Invited talk

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 [1], 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 [2]. 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 [3], and the graded TT-lifting of ordinary monads.

[1] Philip Wadler. The Marriage of Effects and Monads. ICFP 1998: 63-74

[2] Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. POPL 2014: 633-646

[3] Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès. Towards a Formal Theory of Graded Monads. FoSSaCS 2016: 513-530

Sun 3 Sep

Displayed time zone: Belfast change

09:10 - 10:00
Invited talkHOPE at L3
Invited Talk: Semantics of Effect Systems by Graded Monads
Shin-ya Katsumata National Institute of Informatics