Coeffects: Context-aware programming languages

Add to your list(s) Download to your calendar using vCal

• Tomas Petricek (University of Cambridge)
• Friday 20 March 2015, 16:00-17:00
• CS 245.

If you have a question about this talk, please contact Neel Krishnaswami.

The development of programming languages needs to reflect important changes in the way programs execute. One such recent change is the growing importance of execution environment or context in which applications execute. In this talk, I argue that programming languages should provide abstractions for programming with context and verifying how it is accessed.

I identify a number of program properties that were not connected before, but model some notion of context. The examples include tracking different execution platforms (and their versions) in cross-platform development, resources available in different execution environments (e.g. GPS sensor on a phone and database on the server), but also more traditional notions such as variable usage (e.g. in liveness analaysis and in linear logics) or past values in stream-based data-flow programming.

I will present two coeffect systems that highlight the relationship between different notions of context. In particular, the flat coeffect calculus models languages with contextual properties of the execution environment and the structural coeffect calculus models languages where the contextual properties are attached to the variable usage. Although the focus of this talk is on the syntactic properties of the presented systems, I will also briefly discuss their category-theoretical motivation – I will introduce the notion of an graded comonad (based on dualisation of the well-known monad structure) that provides semantics of the two coeffect calculi.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• CS 245
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.