Programming type-safe transformations using higher-order abstract syntax
When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effort. In this paper, we show how Beluga's depen...
Main Authors: | , , |
---|---|
Format: | Text |
Language: | English |
Published: |
Alma Mater Studiorum - University of Bologna
2015
|
Subjects: | |
Online Access: | https://dx.doi.org/10.6092/issn.1972-5787/5122 http://jfr.unibo.it/article/view/5122 |
id |
ftdatacite:10.6092/issn.1972-5787/5122 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.6092/issn.1972-5787/5122 2023-05-15T15:41:58+02:00 Programming type-safe transformations using higher-order abstract syntax Savary Belanger, Olivier Monnier, Stefan Pientka, Brigitte 2015 https://dx.doi.org/10.6092/issn.1972-5787/5122 http://jfr.unibo.it/article/view/5122 en eng Alma Mater Studiorum - University of Bologna This work is licensed under a Creative Commons Attribution 3.0 International License. http://creativecommons.org/licenses/by/3.0 CC-BY Logical frameworks; Certified Programming; Type-preserving Compilation Text Article article-journal ScholarlyArticle 2015 ftdatacite https://doi.org/10.6092/issn.1972-5787/5122 2021-11-05T12:55:41Z When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effort. In this paper, we show how Beluga's dependent contextual types let us use higher-order abstract syntax (HOAS) to implement a type-preserving compiler for the simply-typed lambda-calculus, including transformations such as closure conversion and hoisting. Unlike previous implementations, which have to abandon HOAS locally in favor of a first-order binder representation, we are able to take advantage of HOAS throughout the compiler pipeline, so that the compiler code stays clean and we do not need extra lemmas about binder manipulation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming. Scope and type safety of the code transformations are statically guaranteed, and our implementation nicely mirrors the paper proof of type preservation, and can hence be seen as an encoding of the proof which happens to be executable as well. : Journal of Formalized Reasoning, Vol 8, No 1 (2015) Text Beluga* DataCite Metadata Store (German National Library of Science and Technology) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
English |
topic |
Logical frameworks; Certified Programming; Type-preserving Compilation |
spellingShingle |
Logical frameworks; Certified Programming; Type-preserving Compilation Savary Belanger, Olivier Monnier, Stefan Pientka, Brigitte Programming type-safe transformations using higher-order abstract syntax |
topic_facet |
Logical frameworks; Certified Programming; Type-preserving Compilation |
description |
When verifying that compiler phases preserve some property of the compiled program, a major difficulty resides in how to represent and manipulate variable bindings, often imposing extra complexity both on the compiler writer and the verification effort. In this paper, we show how Beluga's dependent contextual types let us use higher-order abstract syntax (HOAS) to implement a type-preserving compiler for the simply-typed lambda-calculus, including transformations such as closure conversion and hoisting. Unlike previous implementations, which have to abandon HOAS locally in favor of a first-order binder representation, we are able to take advantage of HOAS throughout the compiler pipeline, so that the compiler code stays clean and we do not need extra lemmas about binder manipulation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming. Scope and type safety of the code transformations are statically guaranteed, and our implementation nicely mirrors the paper proof of type preservation, and can hence be seen as an encoding of the proof which happens to be executable as well. : Journal of Formalized Reasoning, Vol 8, No 1 (2015) |
format |
Text |
author |
Savary Belanger, Olivier Monnier, Stefan Pientka, Brigitte |
author_facet |
Savary Belanger, Olivier Monnier, Stefan Pientka, Brigitte |
author_sort |
Savary Belanger, Olivier |
title |
Programming type-safe transformations using higher-order abstract syntax |
title_short |
Programming type-safe transformations using higher-order abstract syntax |
title_full |
Programming type-safe transformations using higher-order abstract syntax |
title_fullStr |
Programming type-safe transformations using higher-order abstract syntax |
title_full_unstemmed |
Programming type-safe transformations using higher-order abstract syntax |
title_sort |
programming type-safe transformations using higher-order abstract syntax |
publisher |
Alma Mater Studiorum - University of Bologna |
publishDate |
2015 |
url |
https://dx.doi.org/10.6092/issn.1972-5787/5122 http://jfr.unibo.it/article/view/5122 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga* |
genre_facet |
Beluga* |
op_rights |
This work is licensed under a Creative Commons Attribution 3.0 International License. http://creativecommons.org/licenses/by/3.0 |
op_rightsnorm |
CC-BY |
op_doi |
https://doi.org/10.6092/issn.1972-5787/5122 |
_version_ |
1766374855865794560 |