Pyrosome: Verified Compilation for Modular Metatheory

TL;DR

Pyrosome is a Coq-based framework enabling modular, verified language compilation that supports incremental extension of semantics and correctness proofs through an inductive equivalence preservation approach.

Contribution

It introduces a novel inductive formulation for equivalence preservation, allowing verified compilers to be extended modularly with reusable correctness proofs.

Findings

Built a multipass compiler from System F to CPS and closure conversion.

Demonstrated incremental extension of language features and correctness proofs.

Showed handling of substructural typing and imperative features in the framework.

Abstract

We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniques for semantic reasoning are often tied to the specific structures of the languages and compilers that they support. In Pyrosome, verified compilers are fully extensible, meaning that to extend a language (even with a new kind of effect) simply requires defining and verifying the compilation of the new feature, reusing the old correctness theorem for all other cases. The novel enabling idea is an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler. Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by dependently sorted equational theories, so all compiler-correctness proofs boil down to type-checking and equational reasoning. We support vertical composition of any compilers expressed in our framework in addition to feature extension. As a case study, we present a multipass compiler from System F with simple references, through CPS translation and closure conversion. Specifically, we demonstrate how we can build such a compiler incrementally by starting with a compiler for simply typed lambda-calculus and adding natural numbers, the unit type, recursive functions, and a global heap, then extending judgments with a type environment and adding type abstraction, all while reusing the original theorems. We also present a linear version of the simply typed CPS pass and compile a small imperative language to the simply typed target to show how Pyrosome handles substructural typing and imperative features.