Title: Typed Closure Conversion for the Calculus of Constructions,
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.