Typed Closure Conversion for the Calculus of Constructions
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.
Fri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
16:10 - 17:25 | |||
16:10 25mTalk | Guarded Impredicative Polymorphism PLDI Research Papers Alejandro Serrano Utrecht University, Jurriaan Hage Utrecht University, Dimitrios Vytiniotis Microsoft Research, Cambridge, Simon Peyton Jones Microsoft Research Media Attached | ||
16:35 25mTalk | Typed Closure Conversion for the Calculus of Constructions PLDI Research Papers Media Attached | ||
17:00 25mTalk | Inferring Type Rules for Syntactic Sugar PLDI Research Papers Media Attached |