One-Pass CPS Translation of Dependent Types
Offered By: ACM SIGPLAN via YouTube
Course Description
Overview
Explore a talk proposal on type-preserving, one-pass Continuation-Passing Style (CPS) translation for dependently typed languages. Delve into the challenges of preserving dependent types during compilation, focusing on the Calculus of Constructions with dependent pair types. Review existing techniques for maintaining dependent types in standard CPS translations and examine the speaker's approach to adapting these methods for an optimizing translation that eliminates administrative redexes. Gain insights into the importance of type preservation in compilers, especially when working with dependently typed source and target languages.
Syllabus
[PEPM'24] One-Pass CPS Translation of Dependent Types (Talk Proposal)
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