CPS Transform and Type Derivations in Dependent ML (Extended Abstract)

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
Published: 2001
Subjects:
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.9075
http://www.cs.yale.edu/~carsten/papers/cpsdml.ps.gz
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.