PL/SE Seminar: An algebraic theory of type and effect systems

Speaker: Ohad Kammar , University of Cambridge

Date: Monday, September 30, 2013

Time: 3:00 PM to 4:30 PM Note: all times are in the Eastern Time Zone

Refreshments: 3:00 PM

Public: Yes

Location: 32-D463 (Star)

Event Type:

Room Description:

Host: Adam Chlipala, CSAIL

Contact: Adam Chlipala, adamc@csail.mit.edu

Relevant URL: http://www.cl.cam.ac.uk/~ok259/

Speaker URL: None

Speaker Photo:
None

Reminders to: pl@csail.mit.edu, seminars@csail.mit.edu

Reminder Subject: TALK: PL/SE Seminar: An algebraic theory of type and effect systems

We present a theory of Gifford-style type-and-effect annotations, where effect annotations are sets of effects, such as memory accesses or exceptions. Our theory accounts for effect-dependent program transformations for functional-imperative languages, as used in optimizing compilers. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi's monadic theory of computational effects that emphasizes the operations causing the effects at hand. The key observation is that annotation effects denote algebraic operations.

After presenting our general type-and-effect system and its semantics, we validate and generalize existing optimizations and add new ones. Our theory also suggests a classification of these optimizations into three classes, structural, local, and global: structural optimizations always hold; local ones depend on the effect theory at hand; and global ones depend on the global nature of that theory, such as idempotency or absorption laws. We also give modularly-checkable necessary and sufficient conditions for validating the optimizations.

Joint work with Gordon Plotkin.

Research Areas:

Impact Areas:

This event is not part of a series.

Created by Adam Chlipala at Monday, September 23, 2013 at 5:56 PM.