|
Chiyan Chen and Hongwei Xi
Implementing typeful program
transformation
In Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and
Semantics Based Program Manipulation, San Diego, CA, June 2003
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.
[ bib |
.ps |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
