One-Pass CPS Translation of Dependent Types (bibtex)

Abstract:

Type preservation is an important property of compilers, especially in the case where the source and target languages are dependently typed. Our goal is to define a type-preserving, one-pass CPS translation of the Calculus of Constructions with dependent pair types. In this talk proposal, we first review the existing techniques for preserving dependent types in ordinary CPS translations, and then describe our attempt to adapt those techniques to an optimizing translation that yields no administrative redexes.

Reference:

One-Pass CPS Translation of Dependent Types (Youyou Cong), Talk at ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2024), 2024.

Bibtex Entry:

@misc{cong2024pepm,
  author = {Youyou Cong},
  title = {One-Pass CPS Translation of Dependent Types},
  howpublished = {Talk at ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2024)},
  month = jan,
  year = 2024,
  date = {2024-01-16},
  url = {https://popl24.sigplan.org/home/pepm-2024},
  pdf = {pepm2024cps.pdf},
  slides = {pepm2024cps-slides.pdf},
  abstract = {Type preservation is an important property of compilers, especially in the case where the source and target languages are dependently typed. Our goal is to define a type-preserving, one-pass CPS translation of the Calculus of Constructions with dependent pair types. In this talk proposal, we first review the existing techniques for preserving dependent types in ordinary CPS translations, and then describe our attempt to adapt those techniques to an optimizing translation that yields no administrative redexes.}
}