CPS Transform for Dependent ML

• Main Authors: Hongwei Xi, Carsten Schürmann
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Subjects: CPS transform; Dependent ML; Compilation certication; DML
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.4071; http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps

Dependent ML is a functional programming language that extends ML with a restricted form of dependent types. In this paper, we study a call-by-value continuation-passing style (CPS) transform for ML 0 , a core of DML that excludes eects. In particular, we demonstrate how the type derivation of an expression in ML 0 can be transformed into the type derivation of the CPS transform of the expression, lifting CPS transform from the level of expressions to the level of type derivations. This work serves as the rst step in our attempt to build a type-preserving compiler for DML by compiling the type derivation of a program instead of the program itself.