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 depend...
Main Authors: | , , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Alma Mater Studiorum - University of Bologna
2015
|
Subjects: | |
Online Access: | https://jfr.unibo.it/article/view/5122 https://doi.org/10.6092/issn.1972-5787/5122 |
id |
ftunivbolognaojs:oai:journals.unibo.it:article/5122 |
---|---|
record_format |
openpolar |
spelling |
ftunivbolognaojs:oai:journals.unibo.it:article/5122 2024-09-15T17:59:04+00:00 Programming type-safe transformations using higher-order abstract syntax Savary Belanger, Olivier Monnier, Stefan Pientka, Brigitte 2015-12-02 application/pdf https://jfr.unibo.it/article/view/5122 https://doi.org/10.6092/issn.1972-5787/5122 eng eng Alma Mater Studiorum - University of Bologna https://jfr.unibo.it/article/view/5122/5330 https://jfr.unibo.it/article/view/5122 doi:10.6092/issn.1972-5787/5122 Copyright (c) 2015 Brigitte Pientka Journal of Formalized Reasoning; Vol. 8 No. 1 (2015); 49-91 Journal of Formalized Reasoning; V. 8 N. 1 (2015); 49-91 1972-5787 Logical frameworks Certified Programming Type-preserving Compilation info:eu-repo/semantics/article info:eu-repo/semantics/publishedVersion 2015 ftunivbolognaojs https://doi.org/10.6092/issn.1972-5787/5122 2024-07-01T03:10:11Z 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. Article in Journal/Newspaper Beluga* AlmaDL Journals (University of Bologna) |
institution |
Open Polar |
collection |
AlmaDL Journals (University of Bologna) |
op_collection_id |
ftunivbolognaojs |
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. |
format |
Article in Journal/Newspaper |
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://jfr.unibo.it/article/view/5122 https://doi.org/10.6092/issn.1972-5787/5122 |
genre |
Beluga* |
genre_facet |
Beluga* |
op_source |
Journal of Formalized Reasoning; Vol. 8 No. 1 (2015); 49-91 Journal of Formalized Reasoning; V. 8 N. 1 (2015); 49-91 1972-5787 |
op_relation |
https://jfr.unibo.it/article/view/5122/5330 https://jfr.unibo.it/article/view/5122 doi:10.6092/issn.1972-5787/5122 |
op_rights |
Copyright (c) 2015 Brigitte Pientka |
op_doi |
https://doi.org/10.6092/issn.1972-5787/5122 |
_version_ |
1810436014830780416 |