Coeffects Unified static analysis of context-dependence

Tomas Petricek, Dominic Orchard and Alan Mycroft

In Proceedings of ICALP 2013

Monadic effect systems provide a unified way of tracking effects of computations, but there is no unified mechanism for tracking how computations rely on the environment in which they are executed. This is becoming an important problem for modern software - we need to track where distributed computations run, which resources a program uses and how they use other capabilities of the environment.

We consider three examples of context-dependence analysis: liveness analysis, tracking the use of implicit parameters (similar to tracking of resource usage in distributed computation), and calculating caching requirements for dataflow programs. Informed by these cases, we present a unified calculus for tracking context dependence in functional languages together with a categorical semantics based on indexed comonads. We believe that indexed comonads are the right foundation for constructing context-aware languages and type systems and that following an approach akin to monads can lead to a widespread use of the concept.

Paper and more information


If you want to cite the paper, you can use the following BibTeX information, or get full details from the paper page on ACM.

  author    = {Petricek, Tomas and Orchard, Dominic and Mycroft, Alan},
  title     = {Coeffects: unified static analysis of context-dependence},
  booktitle = {Proceedings of International Conference on Automata,
               Languages, and Programming - Volume Part II},
  series    = {ICALP 2013},
  location  = {Riga, Latvia},
  year      = {2013}

If you have any comments, suggestions or related ideas, I'll be happy to hear from you! Send me an email at or get in touch via Twitter at @tomaspetricek.

Published: Monday, 17 June 2013, 12:00 AM
Author: Tomas Petricek
Typos: Send me a pull request!