Reasoning About Code-Generation in Two-Level Languages
DOI:
https://doi.org/10.7146/brics.v7i46.20213Resumé
We show that two-level languages are not only a good tool for describing code-generation algorithms, but a good tool for reasoning about them
as well. Indeed, some general properties of two-level languages capture common proof obligations of code-generation algorithms in the form of two-level programs.
- To prove that the generated code behaves as desired, we use an erasure property, which equationally relates the generated code to an erasure of the original two-level program in the object language, thereby reducing the two-level proof obligation to a simpler one-level obligation.
- To prove that the generated code satisfies certain syntactic constraints, e.g., that it is in some normal form, we use a type-preservation property for a refined type system that enforces these constraints.
In addition, to justify concrete implementations of code-generation algorithms in one-level languages, we use a native embedding of a two-level language into a one-level language. We present two-level languages with these properties both for a call-by-name object language and for a call-by-value object language with computational effects. Indeed, it is these properties that guide our language design in the call-by-value case. We consider two classes of non-trivial applications:
one-pass transformations into continuation-passing style and
type-directed partial evaluation for call-by-name and for call-by-value.
Keywords. Two-level languages, erasure, type preservation, native implementation,
partial evaluation.
Downloads
Publiceret
Citation/Eksport
Nummer
Sektion
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
