An Intrinsically Typed Compiler for Algebraic Effect Handlers

Explore a 16-minute video presentation from the PEPM 2024 conference on developing an intrinsically typed compiler for algebraic effect handlers. Delve into the challenges of type-preserving compilation for languages with first-class continuation manipulation facilities. Learn how the researchers tackle the safety issues of continuation capture and resumption using stack polymorphism. Discover the implementation of this compiler in Agda as a function between intrinsically typed ASTs, demonstrating its type-preserving nature. Gain insights into potential applications for correct and efficient compilation of continuation-manipulating facilities in programming languages.