Abstract:
Type-preserving compilation serves as a lightweight approach to building safe and correct compilers. In particular, dependent-type-preserving compilation makes it possible to preserve detailed specifications of source programs throughout the compilation process. We present a CPS translation of a dependently typed language that yields no administrative redexes and preserves types. We show that defining such a translation is non-trivial, and we solve the challenge by representing certain continuations using a let expression. The resulting translation yields terms that are mostly in CPS but partly in ANF.
Reference:
A Mostly CPS, Partly ANF Translation of Dependent Types (Youyou Cong, Hironori Kawazoe and Hidehiko Masuhara), Talk at the 36th Symposium on Implementation and Application of Functional Languages (IFL 2024), 2024.
Bibtex Entry:
@misc{cong2024ifl,
author = {Youyou Cong and Hironori Kawazoe and Hidehiko Masuhara},
title = {A Mostly CPS, Partly ANF Translation of Dependent Types},
year = {2024},
month = aug,
url = {https://ifl24.cs.ru.nl/},
pdf = {ifl2024cong.pdf},
slides = {ifl2024cong-slides.pdf},
abstract = {Type-preserving compilation serves as a lightweight approach to building safe and correct compilers. In particular, dependent-type-preserving compilation makes it possible to preserve detailed specifications of source programs throughout the compilation process. We present a CPS translation of a dependently typed language that yields no administrative redexes and preserves types. We show that defining such a translation is non-trivial, and we solve the challenge by representing certain continuations using a let expression. The resulting translation yields terms that are mostly in CPS but partly in ANF.},
howpublished = {Talk at the 36th Symposium on Implementation and Application of Functional Languages (IFL 2024)}
}