Wed 10 Jan 2018 16:15 - 16:40 at Watercourt - Types Chair(s): Thorsten Altenkirch

Dependently typed languages such as Coq are used to specify and prove functional correctness of source programs, but what we ultimately need are guarantees about correctness of compiled code. By preserving dependent types through each compiler pass, we could preserve source-level specifications and correctness proofs into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In 2002, Barthe and Uustalu showed that type-preserving CPS is \emph{not possible} for languages such as Coq. Specifically, they showed that for strong dependent pairs ($\Sigma$ types), the standard typed call-by-name CPS is \emph{not type preserving}. They further proved that for dependent case analysis on sums, a class of typed CPS translations—including the standard translation—is \emph{not possible}. In 2016, Morrisett noticed a similar problem with the standard call-by-value CPS translation for dependent functions ($\Pi$ types). In essence, the problem is that the standard typed CPS translation by double-negation, in which computations are assigned types of the form $(A \rightarrow \bot) \rightarrow \bot$, disrupts the term/type equivalence that is used during type checking in a dependently typed language.

In this paper, we prove that type-preserving CPS translation for dependently typed languages is \emph{not} not possible. We develop both call-by-name and call-by-value CPS translations from the Calculus of Constructions with both $\Pi$ and $\Sigma$ types (CC) to a dependently typed target language, and prove type preservation and compiler correctness of each translation. Our target language is CC extended with an additional equivalence rule and an additional typing rule, which we prove consistent by giving a model in the extensional Calculus of Constructions. Our key observation is that we can use a CPS translation that employs \emph{answer-type polymorphism}, where CPS-translated computations have type $\forall \alpha. (A \rightarrow \alpha) \rightarrow \alpha$. This type justifies, by a \emph{free theorem}, the new equality rule in our target language and allows us to recover the term/type equivalences that CPS translation disrupts. Finally, we conjecture that our translation extends to dependent case analysis on sums, despite the impossibility result, and provide a proof sketch.

#### Wed 10 JanDisplayed time zone: Tijuana, Baja California change

 15:50 - 17:30 TypesResearch Papers at Watercourt Chair(s): Thorsten Altenkirch University of Nottingham 15:5025mTalk A Principled approach to Ornamentation in MLResearch PapersThomas Williams Inria, Didier Rémy Inria 16:1525mTalk Type-Preserving CPS Translation of Σ and Π Types is Not Not PossibleResearch PapersWilliam J. Bowman Northeastern University, USA, Youyou Cong Ochanomizu University, Japan, Nick Rioux Northeastern University, USA, Amal Ahmed Northeastern University, USA Link to publication DOI Pre-print 16:4025mTalk Safety and Conservativity of Definitions in HOL and Isabelle/HOLResearch PapersOndřej Kunčar Technische Universität München, Germany, Andrei Popescu Middlesex University, London 17:0525mTalk Univalent Higher Categories via Complete Semi-Segal TypesResearch PapersPaolo Capriotti University of Nottingham, Nicolai Kraus University of Nottingham