Programming Type-Safe Transformations Using Higher-Order Abstract Syntax

• Main Authors: Olivier Savary-belanger, Stefan Monnier, Brigitte Pientka
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Published: Springer-Verlag 2013
• Subjects: Lambda; Beluga; Beluga*
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.671.6517; http://www.cs.mcgill.ca/%7Ebpientka/papers/cc.pdf

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