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 effects. In particular, we demonstrate how the type derivation of...
| Other Authors: | |
|---|---|
| Format: | Text |
| Language: | English |
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.3696 http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf |
| 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 effects. 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 first 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. |
|---|