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 |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.69.3696 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.69.3696 2023-05-15T16:01:28+02:00 The Pennsylvania State University CiteSeerX Archives application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.3696 http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.3696 http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf CPS transform Dependent ML Compilation certification text ftciteseerx 2016-01-08T18:19:23Z 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. Text DML Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
topic |
CPS transform Dependent ML Compilation certification |
spellingShingle |
CPS transform Dependent ML Compilation certification |
topic_facet |
CPS transform Dependent ML Compilation certification |
description |
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. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.3696 http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf |
genre |
DML |
genre_facet |
DML |
op_source |
http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.69.3696 http://www.cs.bu.edu/~hwxi/academic/papers/DMLcps.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397306052018176 |