A Mostly CPS, Partly ANF Translation of Dependent Types
Youyou Cong, Hironori Kawazoe, Hidehiko Masuhara · 2024
Type-preserving compilation is an approach to building reliable compilers.The technique has recently been extended to dependently typed languages, but existing approaches have practical and theoretical shortcomings.We present a dependent-type-preserving translation into continuation-passing style (CPS).As improvements from previous work, our translation yields no administrative redexes, and its output can be typed using standard typing rules.This is achieved by defining an auxiliary translation that produces let-represented continuations in selected cases.The unique design makes the output of the translation partly look like A-normal form (ANF).