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

Full description

Bibliographic Details
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Subjects:
DML
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