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 |
| Language: | English |
| Published: |
University of Bologna
2015-12-01
|
| Series: | Journal of Formalized Reasoning |
| Subjects: | |
| Online Access: | http://jfr.unibo.it/article/view/5122 |
| _version_ | 1818853859208986624 |
|---|---|
| author | Olivier Savary Belanger Stefan Monnier Brigitte Pientka |
| author_facet | Olivier Savary Belanger Stefan Monnier Brigitte Pientka |
| author_sort | Olivier Savary Belanger |
| collection | DOAJ |
| 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. |
| first_indexed | 2024-12-19T07:43:30Z |
| format | Article |
| id | doaj.art-3a9518f3b40240fbbed3dd4a2e902e71 |
| institution | Directory Open Access Journal |
| issn | 1972-5787 |
| language | English |
| last_indexed | 2024-12-19T07:43:30Z |
| publishDate | 2015-12-01 |
| publisher | University of Bologna |
| record_format | Article |
| series | Journal of Formalized Reasoning |
| spelling | doaj.art-3a9518f3b40240fbbed3dd4a2e902e712022-12-21T20:30:23ZengUniversity of BolognaJournal of Formalized Reasoning1972-57872015-12-0181499110.6092/issn.1972-5787/51225114Programming type-safe transformations using higher-order abstract syntaxOlivier Savary Belanger0Stefan Monnier1Brigitte Pientka2School of Computer Science McGill UniversityUniversite de MontrealSchool of Computer Science McGill UniversityWhen 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.http://jfr.unibo.it/article/view/5122Logical frameworksCertified ProgrammingType-preserving Compilation |
| spellingShingle | Olivier Savary Belanger Stefan Monnier Brigitte Pientka Programming type-safe transformations using higher-order abstract syntax Journal of Formalized Reasoning Logical frameworks Certified Programming Type-preserving Compilation |
| title | 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_short | Programming type-safe transformations using higher-order abstract syntax |
| title_sort | programming type safe transformations using higher order abstract syntax |
| topic | Logical frameworks Certified Programming Type-preserving Compilation |
| url | http://jfr.unibo.it/article/view/5122 |
| work_keys_str_mv | AT oliviersavarybelanger programmingtypesafetransformationsusinghigherorderabstractsyntax AT stefanmonnier programmingtypesafetransformationsusinghigherorderabstractsyntax AT brigittepientka programmingtypesafetransformationsusinghigherorderabstractsyntax |