A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs

TL;DR

This paper presents a method for simplifying the implementation and verification of functional language compilers by using Higher-Order Abstract Syntax (HOAS), demonstrated through a verified compiler in lambda Prolog and Abella.

Contribution

It introduces a HOAS-based framework for verified compilation, combining rule-based specifications with proof systems to simplify handling of binding structures.

Findings

HOAS simplifies compiler implementation and verification.

The approach reduces complexity in reasoning about binding structures.

Verified compiler transformations demonstrate the effectiveness of HOAS.

Abstract

We argue that the implementation and verification of compilers for functional programming languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying idea of HOAS is to use a meta-language that provides a built-in and logical treatment of binding related notions. By embedding the meta-language within a larger programming or reasoning framework, it is possible to absorb the treatment of binding structure in the object language into the meta-theory of the system, thereby greatly simplifying the overall implementation and reasoning processes. We develop the above argument in this thesis by presenting and demonstrating the effectiveness of an approach to the verified implementation of compiler transformations for functional programs that exploits HOAS. In this approach, transformations on functional programs are first articulated in the form of rule-based relational specifications. These specifications are rendered into programs in the language lambda Prolog. On the one hand, these programs serve directly as implementations. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. Both lambda Prolog and Abella support the use of the HOAS approach. Thus, they constitute a framework that can be used to test out the benefits of the HOAS approach in verified compilation. We use them to implement and verify a compiler for a representative functional programming language that embodies the transformations that form the core of many compilers for such languages. In both the programming and the reasoning phases, we show how the use of the HOAS approach significantly simplifies the representation, manipulation, analysis and reasoning of binding structure.