A type-preserving compiler converts a well-typed input program into a well-typed output program.
Previous studies have developed type-preserving compilers for various source languages,
including the simply-typed lambda calculus and calculi with control constructs.
Our goal is to realize type-preserving compilation of languages that have facilities for manipulating first-class continuations.
In this paper, we focus on algebraic effects and handlers, a generalization of exceptions and their handlers with resumable continuations.
Specifically, we choose an effect handler calculus and a typed stack-machine-based assembly language as the source and the target languages, respectively, and formalize the target language and a type preserving compiler.
The main challenge posed by first-class continuation is how to ensure safety of continuation capture and resumption, which involves concatenation of unknown stacks.
We solve this challenge by incorporating stack polymorphism, a technique that has been used for compilation from a language without first-class continuations to a stack-based assembly language.
To prove that our compiler is type preserving, we implemented the compiler in Agda as a function between intrinsically typed ASTs.
We believe that our contributions could lead to correct and efficient compilation of continuation-manipulating facilities in general.