Implementing typeful program transformations
The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct pro...
Published in: | ACM SIGPLAN Notices |
---|---|
Main Authors: | , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2003
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1145/966049.777392 https://dl.acm.org/doi/pdf/10.1145/966049.777392 |
id |
cracm:10.1145/966049.777392 |
---|---|
record_format |
openpolar |
spelling |
cracm:10.1145/966049.777392 2024-05-19T07:39:28+00:00 Implementing typeful program transformations Chen, Chiyan Xi, Hongwei 2003 http://dx.doi.org/10.1145/966049.777392 https://dl.acm.org/doi/pdf/10.1145/966049.777392 en eng Association for Computing Machinery (ACM) ACM SIGPLAN Notices volume 38, issue 10, page 20-28 ISSN 0362-1340 1558-1160 journal-article 2003 cracm https://doi.org/10.1145/966049.777392 2024-05-01T06:43:48Z The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct programs, for representing object programs, that is, the programs in the object language on which the program transformation is to be performed. In practice, most representations chosen for typed object programs are typeless in the sense that the type of an object program cannot be reflected in the type of its representation. This is unsatisfactory as such typeless representations make it impossible to capture in the type system of the meta language various invariants in a program transformation that are related to the types of object programs. In this paper, we propose an approach to implementing program transformations that makes use of a first-order typeful program representation formed in Dependent ML (DML), where the type of an object program as well as the types of the free variables in the object program can be reflected in the type of the representation of the object program. We introduce some programming techniques needed to handle this typeful program representation, and then present an implementation of a CPS transform function where the relation between the type of an object program and that of its CPS transform is captured in the type system of DML. In a broader context, we claim to have taken a solid step along the line of research on constructing certifying compilers. Article in Journal/Newspaper DML ACM Publications (Association for Computing Machinery) ACM SIGPLAN Notices 38 10 20 28 |
institution |
Open Polar |
collection |
ACM Publications (Association for Computing Machinery) |
op_collection_id |
cracm |
language |
English |
description |
The notion of program transformation is ubiquitous in programming language studies on interpreters, compilers, partial evaluators, etc. In order to implement a program transformation, we need to choose a representation in the meta language, that is, the programming language in which we construct programs, for representing object programs, that is, the programs in the object language on which the program transformation is to be performed. In practice, most representations chosen for typed object programs are typeless in the sense that the type of an object program cannot be reflected in the type of its representation. This is unsatisfactory as such typeless representations make it impossible to capture in the type system of the meta language various invariants in a program transformation that are related to the types of object programs. In this paper, we propose an approach to implementing program transformations that makes use of a first-order typeful program representation formed in Dependent ML (DML), where the type of an object program as well as the types of the free variables in the object program can be reflected in the type of the representation of the object program. We introduce some programming techniques needed to handle this typeful program representation, and then present an implementation of a CPS transform function where the relation between the type of an object program and that of its CPS transform is captured in the type system of DML. In a broader context, we claim to have taken a solid step along the line of research on constructing certifying compilers. |
format |
Article in Journal/Newspaper |
author |
Chen, Chiyan Xi, Hongwei |
spellingShingle |
Chen, Chiyan Xi, Hongwei Implementing typeful program transformations |
author_facet |
Chen, Chiyan Xi, Hongwei |
author_sort |
Chen, Chiyan |
title |
Implementing typeful program transformations |
title_short |
Implementing typeful program transformations |
title_full |
Implementing typeful program transformations |
title_fullStr |
Implementing typeful program transformations |
title_full_unstemmed |
Implementing typeful program transformations |
title_sort |
implementing typeful program transformations |
publisher |
Association for Computing Machinery (ACM) |
publishDate |
2003 |
url |
http://dx.doi.org/10.1145/966049.777392 https://dl.acm.org/doi/pdf/10.1145/966049.777392 |
genre |
DML |
genre_facet |
DML |
op_source |
ACM SIGPLAN Notices volume 38, issue 10, page 20-28 ISSN 0362-1340 1558-1160 |
op_doi |
https://doi.org/10.1145/966049.777392 |
container_title |
ACM SIGPLAN Notices |
container_volume |
38 |
container_issue |
10 |
container_start_page |
20 |
op_container_end_page |
28 |
_version_ |
1799479051488854016 |