Sat 22 Jun 2019 16:45 - 17:30 at 106B - Interaction Trees and Algebraic Effects I Chair(s): Andrew W. Appel

Algebraic Effect Handlers are a powerful abstraction mechanism that can express many complex control-flow mechanisms. But this power makes it also hard to reason about such effectful programs. In this talk I will use a novel way of explaining algebraic effects in terms of ambient values, functions, and control. Ambient values are a typed form of dynamic binding, while ambient functions are dynamically bound but statically scoped. Finally, ambient control gives the full power of algebraic effects. We argue that understanding algebraic effects in terms of ambients is easier, and enables better reasoning about effects since ambient values and functions do not modify control.

I am a member of the Research In Software Engineering (RISE) group and chair of the Programming Languages working group (PLX). Currently, I am interested in the design and application of strong type systems and declarative programming languages, like Haskell. In particular, I am interested in programming with Effect inference in the Koka project. Furthermore, I work on domain specific embedded languages, language design, and compiler technology.

Sat 22 Jun

Displayed time zone: Tijuana, Baja California change

16:00 - 17:30
Interaction Trees and Algebraic Effects IDeepSpec at 106B
Chair(s): Andrew W. Appel Princeton
Interaction Trees: Representing Recursive and Impure Programs in Coq
Steve Zdancewic University of Pennsylvania
Connecting Separation Logic with First-Order Reasoning on Memory
William Mansky University of Illinois at Chicago, Wolf Honore
Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
Daan Leijen Microsoft Research, USA