Rising Stars 2020:

Ningning Xie

PhD Candidate

The University of Hong Kong

Areas of Interest

  • Programming Systems


Effect Handlers, Evidently


Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even too powerful. In this work we define a restriction of general effect handlers with scoped resumptions. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations in place (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.


Ningning Xie is a PhD candidate in the Department of Computer Science at University of Hong Kong. Prior to graduate school, she received her B.S. degree in Computer Science from Zhejiang University. Her research interests are in the field of programming languages, focusing on functional programming and type theory. Some of her research has been implemented in widely-used open-source software, such as the Glasgow Haskell Compiler, the state-of-the-art Haskell compiler; and the Koka programming language, a function-oriented language with effect inference which is being actively developed at Microsoft Research. She is a recipient of the ACM SIGPLAN Distinguished Paper Award in POPL 2020.

Personal home page