Abstracts.2020.Coeffects

Coeffects by Example

by Sandro Stucki

Abstract

Coeffect systems are a general, type-based framework for reasoning about computations under resource constraints. They have a beautiful categorical interpretation based on graded comonads over symmetric monoidal categories. In this lecture I will show a few examples of calculi where coeffects are used to reason about resources: linear and bounded computation, monotonicity, and sensitivity analysis. Then I'll show how all of these systems can be uniformly presented in the generic framework of coeffect systems. If time permits, I'll sketch the categorical semantics of the various systems and of coeffects in general.

Relevant literature:

1. Tomas Petricek, Dominic Orchard, and Alan Mycroft. Coeffects: A Calculus of Context-Dependent Computation. ICFP 2014.
2. Andreas Abel. Polarised Subtyping for Sized Types. MSCS 2008.
3. Jason Reed and Benjamin C. Pierce. Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy. ICFP 2010.
4. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining Effects and Coeffects via Grading. ICFP 2016.

Related talks:

1. Sandro Stucki. Coeffects. ITC 2018.