Skip to content

Abstracts.2020.Coeffects

Jump to bottom
Carlos Tomé edited this page Feb 8, 2021 · 2 revisions

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. Polarized Subtyping for Sized Types. MSCS 18, Special Issue 05, 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:

Clone this wiki locally