Programming type-safe transformations using higher-order abstract syntax
Abstract. Compiling syntax to native code requires complex code trans-formations which rearrange the abstract syntax tree. This can be partic-ularly challenging for languages containing binding constructs, and often leads to subtle, hard to find errors. In this paper, we exploit higher-order abstrac...
Main Authors: | , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
Springer
2013
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.1614 http://www.iro.umontreal.ca/~monnier/tp-compile.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.640.1614 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.640.1614 2023-05-15T15:41:50+02:00 Programming type-safe transformations using higher-order abstract syntax Olivier Savary-belanger Stefan Monnier Brigitte Pientka The Pennsylvania State University CiteSeerX Archives 2013 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.1614 http://www.iro.umontreal.ca/~monnier/tp-compile.pdf en eng Springer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.1614 http://www.iro.umontreal.ca/~monnier/tp-compile.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.iro.umontreal.ca/~monnier/tp-compile.pdf text 2013 ftciteseerx 2016-01-08T15:55:25Z Abstract. Compiling syntax to native code requires complex code trans-formations which rearrange the abstract syntax tree. This can be partic-ularly challenging for languages containing binding constructs, and often leads to subtle, hard to find errors. In this paper, we exploit 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, in the dependently-typed language Beluga. Un-like 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 we do not have to include any lemmas about binder manipulation. Scope and type safety of the code transformations are statically guaranteed, and our imple-mentation directly mirrors the proofs of type preservation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming. 1 Text Beluga Beluga* Unknown Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
Abstract. Compiling syntax to native code requires complex code trans-formations which rearrange the abstract syntax tree. This can be partic-ularly challenging for languages containing binding constructs, and often leads to subtle, hard to find errors. In this paper, we exploit 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, in the dependently-typed language Beluga. Un-like 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 we do not have to include any lemmas about binder manipulation. Scope and type safety of the code transformations are statically guaranteed, and our imple-mentation directly mirrors the proofs of type preservation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming. 1 |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Olivier Savary-belanger Stefan Monnier Brigitte Pientka |
spellingShingle |
Olivier Savary-belanger Stefan Monnier Brigitte Pientka Programming type-safe transformations using higher-order abstract syntax |
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 |
Springer |
publishDate |
2013 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.1614 http://www.iro.umontreal.ca/~monnier/tp-compile.pdf |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
http://www.iro.umontreal.ca/~monnier/tp-compile.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.640.1614 http://www.iro.umontreal.ca/~monnier/tp-compile.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766374719472271360 |