Compiling syntax to native code requires complex code transformations which rearrange the syntax tree. This can be particularly challenging for languages containing binding constructs, and often leads to subtle, hard to find errors. In this paper, we exploit higher-order 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. 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 we do not have to include any lemmas about binder manipulation. Scope and type safety of the code transformations are statically guaranteed, and our implementation directly mirrors the proofs of type preservation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming.
展开▼
