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 not possible for languages such as Coq. Specifically, they showed that for strong dependent pairs (Σ types), the standard typed call-by-name CPS is not type preserving. They further proved that for dependent case analysis on sums, a class of typed CPS translationsÐincluding the standard translationÐis not possible. In 2016, Morrisett noticed a similar problem with the standard call-by-value CPS translation for dependent functions (Π 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 → ⊥) → ⊥, 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 not not possible. We develop both call-by-name and call-by-value CPS translations from the Calculus of Constructions with both Π and Σ 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 answer-type polymorphism, where CPS-translated computations have type ∀α .(A → α) → α. This type justifies, by a 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. CCS Concepts: · Software and its engineering → Correctness; Functional languages; Polymorphism; Control structures; Compilers; · Theory of computation → Type theory; Additional Key Words and Phrases: Dependent types, type theory, secure compilation, type-preserving compilation, parametricity, CPS * We use a non-bold blue sans-serif font to typeset the source language, and a bold red serif font for the target language. The languages are distinguishable in black-and-white, but the paper is easier to read when viewed or printed in color. Authors' addresses: William J. Bowman, Northeastern University, USA, wjb@williamjbowman.com; Youyou Cong, Ochanomizu University, Japan, so.yuyu@is.ocha.ac.jp; Nick Rioux, Northeastern University, USA, rioux.n@husky.neu.edu; Amal Ahmed, Northeastern University, USA, amal@ccs.neu.edu. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s [Gu et al. 2015] , and implementations of cryptographic protocols [Appel 2015; Barthe et al. 2009 ]. But, while dependently typed languages make it easier to verify properties of source (Gallina) programs, what is ultimately needed is a guarantee that the same properties hold of compiled low-level code. This calls for a verified compiler for Gallina and the work underway on CertiCoq [Anand et al. 2017 ] is a good first step. However, CertiCoq erases Gallina types and then performs transformations such as CPS and closure conversion on untyped code. The problem with erasing types too early in the compilation pipeline 1 is that it becomes difficult to build a verified compiler that supports safe/secure linking of compiled code with code from other languages [Ahmed 2015; Patterson and Ahmed 2017]. For instance, consider a (pure) higher-order Gallina function f that is compiled to C or assembly (as in CertiCoq) and linked with a target context that passes the compiled f an impure C or assembly łfunctionž as input. This impure function may break Gallina's type-abstraction or security guarantees or modify f's control flow. Investigating type-preserving compilation of dependently typed languages is critical because, intuitively, the key to protecting the compiled version of f from contexts that provide ill-behaved inputs is to ensure that compiled code can only be linked with target-level contexts that correspond to well-typed source-level contexts. By translating types during compilation, we can encode that correspondence in the types. Then, at link time, we allow linking a well-typed compiled component with other well-typed target language components. With type-preserving compilation and sufficiently rich types at the target level, we can statically rule out linking with ill-behaved/insecure contexts. Thus, type-preserving compilation provides a path to building secure (fully abstract) compilers [Abadi 1998; Ahmed and Blume 2008, 2011; Bowman and Ahmed 2015; Fournet et al. 2013; Kennedy 2006; New et al. 2016; Patrignani et al. 2015] without the overhead of dynamic checks. By preserving dependent types, we can even preserve the full functional specifications into the target level, so that compiled code can be independently verified by type checking. This paper investigates type-preserving CPS for dependently typed languages. CPS translation is an important compiler pass that makes control flow and evaluation order explicit 2 . However, it is a transformation that presents nontrivial problems in a dependently typed setting, as discussed next. Prior Work. Barthe et al. [1999] showed how to scale typed call-by-name (CBN) CPS translation to a large class of Pure Type Systems (PTSs), including the Calculus of Constructions (CC) without Σ types. They used the standard double-negation translation, i.e., the typed variant of Plotkin's original CPS translation, translating source computations of type A to CPS-translated (CPS'd) computations of type (A + → ⊥) → ⊥ (where + denotes value translation of types, as explained in Section 3). To avoid certain technical difficulties (which we discuss in Section 5), they consider only domain-free 1 Here łtoo earlyž means łbefore we have a whole programžÐi.e., before the stage in the compilation pipeline where we link with low-level libraries and code compiled from other languages to form a whole program. 2 We discuss the popular alternative, ANF translation [Flanagan et al. 1993] Barthe and Uustalu [2002] tried to extend these results to the Calculus of Inductive Constructions (CIC), but ended up reporting a negative result, namely that the standard typed CBN CPS translation is not type preserving for Σ types. They go on to prove a general impossibility result: for sum types with dependent case analysis, type preservation is not possible for the class of CPS translations that can implement call/cc. We return to this latter impossibility result, which does not apply to our translation, in Section 7. The problem of CPS translation for Σ types has been revisited by others over the years, but without positive results. In 2016, Greg Morrisett attempted typed call-by-value (CBV) CPS translation of an A-normalized variant of CC, again using the double-negation translation. 3 He alerted us to the fact that typed CBV CPS translation of Σ seems to work when translating from A-normal form, but the CBV CPS translation of Π types (specifically, the application case) fails to type check.
A variant of this translation has been extended recently by Bowman et al. REF to dependent sums using answer-type polymorphism Πα : .
Type-preserving CPS translation of Σ and Π types is not not possible
PACMPL
Mathematics Computer Science