An Intrinsically Typed Compiler for Algebraic Effect Handlers
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
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.
Syllabus
Introduction
Motivation
Presentation
Discussion
Taught by
ACM SIGPLAN
Related Courses
Introduction to programming with dependent types in ScalaStepik On Voevodsky's Univalence Principle - André Joyal
Institute for Advanced Study via YouTube Univalent Foundations and the Equivalence Principle - Benedikt Ahrens
Institute for Advanced Study via YouTube A Little Taste of Dependent Types
Strange Loop Conference via YouTube Dependent Types in Haskell
Strange Loop Conference via YouTube