Programming type-safe transformations using higher-order abstract syntax

Authors

  • Olivier Savary Belanger School of Computer Science McGill University
  • Stefan Monnier Universite de Montreal
  • Brigitte Pientka School of Computer Science McGill University

DOI:

https://doi.org/10.6092/issn.1972-5787/5122

Keywords:

Logical frameworks, Certified Programming, Type-preserving Compilation

Abstract

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.

Downloads

Published

2015-12-02

How to Cite

Savary Belanger, O., Monnier, S., & Pientka, B. (2015). Programming type-safe transformations using higher-order abstract syntax. Journal of Formalized Reasoning, 8(1), 49–91. https://doi.org/10.6092/issn.1972-5787/5122

Issue

Section

Articles