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: |
University of Bologna
2015
|
Subjects: | |
Online Access: | https://doi.org/10.6092/issn.1972-5787/5122 https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71 |
id |
ftdoajarticles:oai:doaj.org/article:3a9518f3b40240fbbed3dd4a2e902e71 |
---|---|
record_format |
openpolar |
spelling |
ftdoajarticles:oai:doaj.org/article:3a9518f3b40240fbbed3dd4a2e902e71 2023-05-15T15:41:58+02:00 Programming type-safe transformations using higher-order abstract syntax Olivier Savary Belanger Stefan Monnier Brigitte Pientka 2015-12-01T00:00:00Z https://doi.org/10.6092/issn.1972-5787/5122 https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71 EN eng University of Bologna http://jfr.unibo.it/article/view/5122 https://doaj.org/toc/1972-5787 1972-5787 doi:10.6092/issn.1972-5787/5122 https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71 Journal of Formalized Reasoning, Vol 8, Iss 1, Pp 49-91 (2015) Logical frameworks Certified Programming Type-preserving Compilation Electronic computers. Computer science QA75.5-76.95 Analytic mechanics QA801-939 article 2015 ftdoajarticles https://doi.org/10.6092/issn.1972-5787/5122 2022-12-31T09:30:03Z 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* Directory of Open Access Journals: DOAJ Articles Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
Directory of Open Access Journals: DOAJ Articles |
op_collection_id |
ftdoajarticles |
language |
English |
topic |
Logical frameworks Certified Programming Type-preserving Compilation Electronic computers. Computer science QA75.5-76.95 Analytic mechanics QA801-939 |
spellingShingle |
Logical frameworks Certified Programming Type-preserving Compilation Electronic computers. Computer science QA75.5-76.95 Analytic mechanics QA801-939 Olivier Savary Belanger Stefan Monnier Brigitte Pientka Programming type-safe transformations using higher-order abstract syntax |
topic_facet |
Logical frameworks Certified Programming Type-preserving Compilation Electronic computers. Computer science QA75.5-76.95 Analytic mechanics QA801-939 |
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 |
Olivier Savary Belanger Stefan Monnier Brigitte Pientka |
author_facet |
Olivier Savary Belanger Stefan Monnier Brigitte Pientka |
author_sort |
Olivier Savary Belanger |
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 |
University of Bologna |
publishDate |
2015 |
url |
https://doi.org/10.6092/issn.1972-5787/5122 https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga* |
genre_facet |
Beluga* |
op_source |
Journal of Formalized Reasoning, Vol 8, Iss 1, Pp 49-91 (2015) |
op_relation |
http://jfr.unibo.it/article/view/5122 https://doaj.org/toc/1972-5787 1972-5787 doi:10.6092/issn.1972-5787/5122 https://doaj.org/article/3a9518f3b40240fbbed3dd4a2e902e71 |
op_doi |
https://doi.org/10.6092/issn.1972-5787/5122 |
_version_ |
1766374852984307712 |