Fri 22 Jun 2018 16:35 - 17:00 at Grand Ballroom CD - Types Chair(s): Kathleen Fisher

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 Jun
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

16:10 - 17:25: PLDI Research Papers - Types at Grand Ballroom CD
Chair(s): Kathleen FisherTufts University
pldi-2018-papers16:10 - 16:35
Alejandro SerranoUtrecht University, Jurriaan HageUtrecht University, Dimitrios VytiniotisMicrosoft Research, Cambridge, Simon Peyton JonesMicrosoft Research
Media Attached
pldi-2018-papers16:35 - 17:00
William J. BowmanNortheastern University, USA, Amal AhmedNortheastern University, USA
Media Attached
pldi-2018-papers17:00 - 17:25
Justin PombrioBrown University, USA, Shriram KrishnamurthiBrown University, USA
Media Attached