Abstracts.2018.Coeffects

Coeffects and Comonads

by Sandro Stucki

I will give three examples of coeffects: quantity [1]; variance [2]; and secrecy [3], and show how these can be tracked through a unified coeffect system [4]. Then, I'll show how this system can be given a categorical interpretation in terms of graded comonads — dual to graded monads [7] [8], which have traditionally been used to model computational effects [5] [6].

1. R. Atkey. The Syntax and Semantics of Quantitative Type Theory. LICS'18. ^{^}
2. A. Abel. Polarized Subtyping for Sized Types. MSCS'08. ^{^}
3. M. Algehed. A Perspective on the Dependency Core Calculus. PLAS'18. ^{^}
4. T. Petricek, D. Orchard, and A. Mycroft. Coeffects: A calculus of context-dependent computation. ICFP'14. ^{^}
5. E. Moggi. Computational lambda-calculus and monads. LICS'89. ^{^}
6. E. Moggi. Notions of computation and monads. INFCOMP'91. ^{^}
7. S. Katsumata. Parametric effect monads and semantics of effect systems. POPL'14. ^{^}
8. D. Orchard, T. Petricek, and A. Mycroft. The semantic marriage of monads and effects. CORR'14. ^{^}