PL/SE Seminar: Coeffects: Types for tracking context-dependence
Speaker: Tomas Petricek, University of Cambridge
Date: Wednesday, February 13 2013
Time: 3:30PM to 4:30PM
Location: 32-G882 (reading room)
Host: Adam Chlipala, CSAIL
Contact: Adam Chlipala, adamc@csail.mit.edu
Relevant URL: http://tomasp.net/
TITLE: Coeffects: Types for tracking context-dependence
ABSTRACT:
Monadic typing provides 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. Since modern software runs in rich, distributed settings where each component executes on a different device, this is becoming an important problem. We need to track where a computation can run, what resources it accesses and how it uses other specific capabilities of the environment.
We consider three examples of context-dependence analysis: liveness analysis, tracking the use of resources in distributed environment, and calculating caching requirements for data-flow 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.
See other events happening in February 2013
