Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control)
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 JunDisplayed time zone: Tijuana, Baja California change
16:00 - 17:30 | |||
16:00 20mTalk | Interaction Trees: Representing Recursive and Impure Programs in Coq DeepSpec Steve Zdancewic University of Pennsylvania | ||
16:20 25mTalk | Connecting Separation Logic with First-Order Reasoning on Memory DeepSpec | ||
16:45 45mTalk | Typed Programming with Algebraic Effects (in terms of ambient values, functions, and control) DeepSpec Daan Leijen Microsoft Research, USA |