CPS Transform for Dependent ML

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 ex...

Full description

Bibliographic Details
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
Description
Summary: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.

Similar Items