Typed Closure Conversion for the Calculus of Constructions

TL;DR

This paper presents a novel type-preserving closure conversion for the Calculus of Constructions, enabling verified compilation of dependently typed programs from Coq-like languages into a dependently typed intermediate language.

Contribution

It introduces a new translation from CC with $ ext{Σ}$ types to a dependently typed intermediate language, ensuring type preservation and correctness of compilation.

Findings

Proved soundness of the translation in CC

Achieved type preservation during compilation

Ensured correctness of separate compilation

Abstract

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms. We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs ($\Sigma$ types)---a subset of the core language of Coq---to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.