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, which have traditionally been used to model computational effects.

• [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.