Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Ohad Kammar

LFCS Seminar: Ohad Kammar

— filed under:

Title: Algebraic Foundations to Effect-Dependent Optimisations

  • LFCS Seminar
When Jan 10, 2012
from 04:00 PM to 05:00 PM
Add event to calendar vCal


We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated, imperative, functional language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).

Joint work with Gordon Plotkin, to appear in POPL'12.

Document Actions