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...
Main Authors: | , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Subjects: | |
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 |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.29.4071 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.29.4071 2023-05-15T16:01:28+02:00 CPS Transform for Dependent ML Hongwei Xi Carsten Schürmann The Pennsylvania State University CiteSeerX Archives application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.4071 http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.4071 http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps CPS transform Dependent ML Compilation certication text ftciteseerx 2016-01-07T21:29:27Z 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. Text DML Unknown |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
topic |
CPS transform Dependent ML Compilation certication |
spellingShingle |
CPS transform Dependent ML Compilation certication Hongwei Xi Carsten Schürmann CPS Transform for Dependent ML |
topic_facet |
CPS transform Dependent ML Compilation certication |
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 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. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Hongwei Xi Carsten Schürmann |
author_facet |
Hongwei Xi Carsten Schürmann |
author_sort |
Hongwei Xi |
title |
CPS Transform for Dependent ML |
title_short |
CPS Transform for Dependent ML |
title_full |
CPS Transform for Dependent ML |
title_fullStr |
CPS Transform for Dependent ML |
title_full_unstemmed |
CPS Transform for Dependent ML |
title_sort |
cps transform for dependent ml |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.4071 http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps |
genre |
DML |
genre_facet |
DML |
op_source |
http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.4071 http://www.ececs.uc.edu/~hwxi/academic/papers/DMLcps.ps |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397307080671232 |