Type-Preserving CPS Translation of and Types is Not Not Possible

Type-Preserving CPS Translation of Σ and Π Types

is Not Not Possible

∗

WILLIAM J. BOWMAN, Northeastern University

YOUYOU CONG, Ochanomizu University

NICK RIOUX, Northeastern University

AMAL AHMED, Northeastern University

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 specications 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. Specically, 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 polymor-

phism, where CPS-translated computations have type

∀α.(A → α ) → α

. This type justies, 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 compi-

lation, parametricity, CPS

ACM Reference format:

William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2018. Type-Preserving CPS Translation of

and Π Types is Not Not Possible. Proc. ACM Program. Lang. 2, POPL, Article 22 (January 2018), 33 pages.

https://doi.org/10.1145/3158110

∗

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.

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 prot or commercial advantage and that copies bear this notice and

the full citation on the rst page. Copyrights for third-party components of this work must be honored. For all other uses,

contact the owner/author(s).

2475-1421/2018/1-ART22 $

https://doi.org/10.1145/3158110

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:2 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

1 INTRODUCTION

Dependently typed languages such as Coq’s Gallina have had tremendous impact on the state of

the art in fully veried software in recent years. Such languages enable verication of program

properties alongside program development, a strategy that has been used to verify full functional

correctness of a range of software, including the CompCert C compiler (Leroy 2006, 2009), the

CertiKOS OS kernel (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 veried compiler for Gallina and the work underway on

CertiCoq (Anand et al

2017) is a good rst 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

is that it becomes dicult to build a veried

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

that is compiled to C or assembly (as in CertiCoq) and linked with a target context that passes the

compiled

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 ow.

Investigating type-preserving compilation of dependently typ ed languages is critical because, in-

tuitively, the key to protecting the compiled version of

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 su-

ciently 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 specications into

the target level, so that compiled code can be independently veried by type checking.

This paper investigates type-preserving CPS for dependently typed languages. CPS translation is

an important compiler pass that makes control ow and evaluation order explicit

. 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

to CPS-translated (CPS’d) computations

of type

→ ⊥) → ⊥

(where

denotes value translation of types, as explained in Section 3). To

avoid certain technical diculties (which we discuss in Section 5), they consider only domain-free

PTSs, a variant of PTSs where

abstractions do not carry the domain of their bound variable—i.e.,

they are of the form λx. e instead of λx : A. e as in the domain-full variant.

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

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.

We discuss the popular alternative, ANF translation (Flanagan et al. 1993), in Section 7.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:3

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.

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 (specically, the application case) fails to type check.

Why is CPS’ing Dependent Types so Hard? In a dependently typed language like CC or CIC, the

power of the type system comes from the ability to express decidable equality between terms

and types. Intuitively, these equalities are decided by reducing terms to canonical forms and

checking that the resulting values are syntactically identical. In the source language—i.e., before

CPS translation—since the language is eect-free, every term can be thought of as a value since every

term reduces a value. But CPS translation converts source (terms and) values into computations

of type

(A → ⊥) → ⊥

. This changes the interface to the values—now we can only access the value

indirectly, by providing a computation that will do something with the value. In essence, ensuring

CPS translations are well typed is hard because every source value has turned into a computation

whose “underlying value” isn’t directly accessible for purposes of deciding equivalence. In particular,

with the double-negation type translation, one cannot recover the underlying value, because every

continuation must return false (⊥).

This description in terms of interfaces is just a shallow description of the problem. At a deeper

level, the problem is that dependently typed languages rely on the ability of the type system to copy

expressions from a term-level context into a type-level context, but CPS transforms expressions

into computations whose meaning, or “underlying value”, depends on its term-level context. This

copying happens in particular in the elimination rules for

and

types, and the dependent case

analysis of sum types—hence these features are at the heart of past negative results—but in general

this happens any time a type depends on an expression. After CPS, we no longer copy an expression,

whose meaning is self contained; instead we copy a computation, whose meaning depends on

its term-level context. Not only do we “forget” part of the meaning of computations, but as we

discussed before, a computation cannot run in a type-level context—it requires a term-level context.

As we describe next, our solution to these problems will be to record part of the term-level contexts

during type checking and to provide an interface that allows types to run computations.

Answer-Type Polymorphism (and a Free Theorem) to the Rescue! In this paper, we show that type-

preserving CBN and CBV CPS translations of CC, with both

and

types, are indeed possible. The

key to our result is that we abandon the standard typed CPS translation based on double negation

in favor of one that employs answer-type polymorphism (Ahmed and Blume 2011; Thielecke 2003,

2004). Specically, CPS’d computations are assigned types of the form

∀α.(A → α) → α

We use

answer-type polymorphism because it lets us choose what type of answer we want back from

a computation. This gives us the ability to locally “run” any CPS’d computation to extract the

underlying result by running the computation with the identity continuation. We use our ability to

extract the underlying result from a computation to recover the equalities needed to prove that

CPS translation is type preserving.

Personal communication, Greg Morrisett, April 2016.

In CC, ∀α .(A → α ) → α is written Πα : ∗.(A → α) → α . We switch to the latter after we introduce CC in Section 2.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:4 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Universes U ::= ∗ | □

| Σ x : A. B | ⟨e

, e

⟩ as Σ x : A. B | fst e | snd e

Environments Γ ::= · | Γ, x : A | Γ, x = e : A

Fig. 1. CC Syntax

We dene a CPS target language that extends CC with two additional rules—an equivalence rule

and a typing rule—inspired (and justied) by a free theorem for the type

∀α.(A → α ) → α

. The two

new rules are essential for type checking the previously problematic CBN/CBV CPS translations of

and

types. We show the consistency of our target language by translating it into a parametric

model of extensional CC.

Contributions. This paper makes the following contributions.

(1)

We give CBN and CBV CPS translations for the domain-full version of CC, with

as well

types, and prove that the translations are type preserving (Section 5 and Section 6).

Unlike Barthe et al

(1999), our translation is dened by induction on typing derivations

and we avoid the proof-staging diculties they discussed as their motivation for studying

CPS of domain-free CC.

(2)

We prove the consistency of our CPS target language CC

, which includes two additional

rules (that, in essence, internalize a free theorem) by showing that we can translate CC

into a parametric model of extensional CC (Section 4). The translation of the new typing

rule resembles the inverse CPS translation of Flanagan et al. (1993).

(3)

We prove separate compilation correctness of our CPS translations. Since we are in a depen-

dently typed setting, proving type preservation requires proving preservation of reduction,

which then easily yields correct separate compilation (Section 5.1 and Section 6.1).

(4)

We conjecture that our CPS translation, based on answer-type polymorphism, should

work for sum types with dependent elimination and provide a proof sketch (Section 7).

We explain why the impossibility proof by Barthe and Uustalu (2002), which applies to a

class of CPS translations, does not apply to the answer-type-polymorphism translation and

discuss how to tackle other issues we expect in scaling to CIC.

Next, we present our source language CC (Section 2), then discuss cases of the (CBN/CBV)

double-negation translation that fail to type check and how we x the problem (Section 3). Parts of

translations and proofs elided from this paper are presented in detail in the online supplementary

material (Bowman et al

2017). The supplementary material includes both a technical appendix with

the additional gures and proofs, and Coq sources for the key lemma in the proof of consistency of

our CPS target language CC

(discussed in Section 4.1).

2 THE CALCULUS OF CONSTRUCTIONS (CC)

Our source language is an extension of the intensional Calculus of Constructions (CC) with strong

dependent pairs (

types) and dependent let. We typeset this language in a non-bold, blue, sans-serif

font. We adapt this presentation from the model of the Calculus of Inductive Constructions (CIC)

given in the Coq reference manual (The Coq Development Team 2017, Chapter 4).

We present the syntax of CC in Figure 1 in the style of a Pure Type System (PTS) with no syntactic

distinction between terms, which are run-time computations, types, which statically describe terms

and compute during type checking, and kinds, which describe types. We use the phrase “expression”

to refer to a term, type, or kind in the PTS syntax. We usually use the meta-variable e to evoke a

term expression and A or B to evoke a type expression. Similarly, we use x to evoke term variables

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:5

Γ ⊢ e ▷ e

′

x ▷

e where x = e : A ∈ Γ

(λ x : A. e

) e

▷

/x]

let x = e

: A in e

▷

/x]

fst ⟨e

, e

⟩ ▷

snd ⟨e

, e

⟩ ▷

Γ ⊢ e ≡ e

′

Γ ⊢ e ▷

⋆

Γ ⊢ e

′

▷

⋆

Γ ⊢ e ≡ e

′

[≡]

Γ ⊢ e ▷

⋆

λ x : A. e

Γ ⊢ e

′

▷

⋆

Γ, x : A ⊢ e

≡ e

Γ ⊢ e ≡ e

′

[≡-η

]

Γ ⊢ e ▷

⋆

Γ ⊢ e

′

▷

⋆

λ x : A. e

Γ, x : A ⊢ e

x ≡ e

Γ ⊢ e ≡ e

′

[≡-η

]

Fig. 2. CC Convertibility and Equivalence

and

for type variables; note that we have no kind-level computation in this language. We use t

for an expression to be explicitly ambiguous about its nature as a term, type, or kind.

The language includes one impredicative universe, or sort,

∗

, and its type,

□

. The syntax of

expressions includes the universe

∗

, variables x or

types Π

x :A.

B, functions

λ x : A.

e, application

, dependent let

let

′

types Σ

x : A.

B, dependent pairs

⟨

⟩ as

x : A.

B, and rst

and second projections

fst

e and

snd

e. Note that we cannot write

□

in source programs—it is only

used by the type system. The environment Γ includes assumptions x : A and denitions x

e : A.

Denitions, introduced while type checking

let

, allow us to convert a variable x to its denition e,

called δ-reduction, and provides additional denitional equivalences compared to application.

For brevity, we omit the type annotations on pairs,

⟨

⟩

, and

let

expressions,

let

′

, when

they are clear from context. We use the notation A

→

B for a function type whose result B does not

depend on the input.

In Figure 2 we present the convertibility and equivalence relations for CC. These relations are

dened over untyped expressions and are used to decide equivalences between types during type

checking. The conversion relation can also be seen as the dynamic semantics of programs in CC. It

does not x an evaluation order, but this is not important since CC is eect-free.

We start with the small-step reductions Γ

⊢

▷

′

. Note that we label each individual reduction

rule with an appropriate subscript, such as

▷

for

-reduction. When we refer to the undecorated

transition Γ

⊢

▷

′

we mean that e reduces to e

′

using some reduction rule— i.e., using one of

▷

, or

▷

. This relation requires the environment Γ for

-reduction as mentioned previously.

For brevity, we usually write this relation as e

▷

′

, with the environment Γ as an implicit parameter.

This reduction relation is completely standard, although

-reduction may be surprising to readers

unfamiliar with dependent type theory. We can

-reduce any variable x to its denition e, written

x ▷

We dene the relation Γ

⊢

▷

⋆

′

as the reexive, transitive, compatible closure of the small-step

relation Γ

⊢

▷

′

. This relation can apply the small-step relation any number of times to any

sub-expression in any order. We usually omit the Γ and write e

▷

⋆

′

for brevity, but note that the

compatible closure rule for let introduces a new denition into Γ, as follows.

Γ, x = e : A ⊢ e

▷

⋆

Γ ⊢ let x = e : A in e

▷

⋆

let x = e : A in e

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:6 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

⊢ Γ

⊢ ·

[W-Empty]

⊢ Γ Γ ⊢ A : U

⊢ Γ, x : A

[W-Assum]

⊢ Γ Γ ⊢ e : A Γ ⊢ A : U

⊢ Γ, x = e : A

[W-Def]

Γ ⊢ e : A

⊢ Γ

Γ ⊢ ∗ : □

[Ax-*]

(x : A ∈ Γ or x = e : A ∈ Γ) ⊢ Γ

Γ ⊢ x : A

[Var]

Γ, x : A ⊢ B : ∗

Γ ⊢ Π x : A. B : ∗

[Prod-*]

Γ, x : A ⊢ B : □

Γ ⊢ Π x : A. B : □

[Prod-□]

Γ, x : A ⊢ e : B Γ ⊢ Π x : A. B : U

Γ ⊢ λ x : A. e : Π x : A. B

[Lam]

Γ ⊢ e : Π x : A

′

. B Γ ⊢ e

′

: A

′

Γ ⊢ e e

′

: B[e

′

/x]

[App]

Γ ⊢ e

′

: A Γ, x = e

′

: A ⊢ e : B

Γ ⊢ let x = e

′

: A in e : B[e

′

/x]

[Let]

Γ ⊢ A : ∗ Γ, x : A ⊢ B : ∗

Γ ⊢ Σ x : A. B : ∗

[Sigma]

Γ ⊢ e

: A Γ ⊢ e

: B[e

/x]

Γ ⊢ ⟨e

, e

⟩ as Σ x : A. B : Σ x : A. B

[Pair]

Γ ⊢ e : Σ x : A. B

Γ ⊢ fst e : A

[Fst]

Γ ⊢ e : Σ x : A. B

Γ ⊢ snd e : B [fst e/x]

[Snd]

Γ ⊢ e : A Γ ⊢ B : U Γ ⊢ A ≡ B

Γ ⊢ e : B

[Conv]

Fig. 3. CC Typing

We dene denitional equivalence Γ

⊢

≡

′

as reduction in the

▷

⋆

relation to the same expression,

up to

-equivalence. This algorithmic presentation induces symmetry and transitivity of

≡

without

explicit symmetry and transitivity rules, but requires two symmetric versions of

-equivalence. We

usually abbreviate this judgment as e ≡ e

′

, leaving Γ implicit.

The typing rules for CC, Figure 3, are completely standard. The judgment

⊢

Γ checks that the

environment Γ is well formed; it is dened by mutual recursion with the typing judgment. The

typing judgment Γ

⊢

A checks that expressions are well typed. The rule [Prod-*] implicitly

allows impredicativity in

∗

, since the domain A could be in the higher universe

□

. The rule [Lam]

for functions

λ x : A.

e gives this function the type Π

x : A.

B, binding the function’s variable x in

the result type B. The rule [App] is the standard dependent application rule. When applying a

dependent function e : Π

x : A.

B to an argument e

′

, the argument is substituted into the result type B

yielding an expression e e

′

B[e

′

/x]

. The rule [Let] is similar; however, when checking the body of

let

′

e, we also adds a denition x

′

: A to the environment. This provides strictly more

type expressivity than the application rule, since the body e is typed with respect to a particular

value for x while a function is typed with respect to an arbitrary value. The rule [Sigma] ensures

we do not allow impredicative strong

types, which are inconsistent (Coquand 1986; Hook and

Howe 1986). Note that the type of a dependent pair Σ

x : A.

B may have the rst component x free in

the type of the second component B. The rule [Snd] for the second projection of a dependent pair,

snd

e, replaces the free variable x by the rst projection, giving

snd

e the dependent type

B[(fst e)/x]

Finally, as we have computation in types, the rule [Conv] allows typing an expression e : A as e : B

when A

≡

B. Note that while the equivalence relation is untyped, we ensure decidability by only

using equivalence in [Conv] after type checking both A and B.

To make our upcoming CPS translation easier to follow, we present a second version of the

syntax for CC in which we make the distinction between terms, types, and kinds explicit (see

Figure 4). The two presentations are equivalent (Barthe et al

1999). Distinguishing terms from types

and kinds is useful since we only want to CPS translate terms, because our goal is to internalize

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:7

Kinds κ ::= ∗ | Π α : κ. κ | Π x : A. κ

| Π α : κ. B | let x = e : A in B | let α = A : κ in B | Σ x : A. B

| let α = A : κ in e | ⟨e

, e

⟩ as Σ x : A. B | fst e | snd e

Environment Γ ::= · | Γ, x : A | Γ, x = e : A, | Γ, α : κ | Γ, α = A : κ

Fig. 4. CC Explicit Syntax

only run-time evaluation contexts. (We discuss per vasive translation, which also internalizes the

type contexts, in Section 7.)

3 MAIN IDEAS: HOW DOUBLE-NEGATION CPS FAILS AND HOW TO FIX IT

In Section 1 we informally explained why CPS translation of dependent types causes type preser-

vation to fail. We now make that intuition concrete by studying two examples. We focus on two

cases of the double-negation CPS translation that fail to type check: the CBN translation of

snd

(reported by Barthe and Uustalu (2002)) and the CBV translation of e e

′

(noticed by Morrisett).

Consider the CBN CPS translation. We translate a term e of type A into a CPS’d computation,

written

, of type

. Given a type A, we dene its computation translation

and its value

translation

. Below, we dene the translations for Σ and Π. (Technically, the translations are dened

by induction on typing derivations, but we present them less formally in this section.) We write

our target language in a

bold, red, serif font

, but for now it is identical to the

source language CC.

= (A

→ ⊥) → ⊥ (Σ x : A. B)

= Σ x : A

. B

(Π x : A. B)

= Π x : A

. B

Note that since this is the CBN translation, the translated argument type for Π is a computation

type A

instead of a value type A

, and the translated component types for Σ are computation types

and B

As a warm-up, consider the CBN translation of fst e (where e : Σ x : A. B):

(fst e : A)

= λ k : A

→ ⊥. e

(λ y : (Σ x : A

. B

). let z = (fst y) : A

in z k)

It is easy to see that the above type checks (checking the types of y, z, and k).

Next, consider the CBN translation of snd e (where e : Σ x : A. B):

(snd e : B[fst e /x])

= λ k : B

[(fst e)

/x] → ⊥. e

(λ y : (Σ x : A

. B

). let z = (snd y) : B

[fst y/x] in z k)

The above does not type check because

expects a continuation of type

[fst y/x] → ⊥

but

has

type

[(fst e)

/x] → ⊥

. Somehow we need to show that

fst y ≡ (fst

)

. But what is the relationship

between

and e? Intuitively, e

: A

is a computation that will pass its result—i.e., the underlying

value of type A

inside e

, which corresponds to the value produced by evaluating the source term

e—to its continuation. So when e

’s continuation is called, its argument

will always be equal

to the unique “underlying value” inside e

. However, since we have used a function to describe a

continuation, we must type check the body of the continuation assuming that

is any value of the

appropriate type instead of the exactly one underlying value from e

Even if we could communicate that

is equal to exactly one value, we have no way to extract the

underlying A

value from e

since the latter takes a continuation that never returns (since it must

return a term of type

⊥

). To extract the underlying value from a computation, we need a means

of converting from A

to A

. In essence, after CPS, we have an interoperability problem between

the term language (where computations have type A

) and the type language (which needs values

of type A

). In the source language, before CPS, we are able to pretend that the term and type

languages are the same because all computations of type A reduce to values of type A. However,

the CPS translation creates a gap between the term and type languages; it changes the interface to

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:8 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

terms so that the only way to get a value out of a computation is to have a continuation, which can

never return, ready to receive that value.

The solution to both of the above problems requires a CPS translation based on answer-type

polymorphism. That is, we change the computation translation to A

= Π α : ∗. (

→ α ) → α

. Now,

to extract the underlying A

value from e

: A

, we can run e

with the identity continuation as

follows: e

. Moreover, we can now justify type checking the body of e

’s continuation under

the assumption that

y ≡

thanks to a free theorem we get from the type A

. The free theorem

says that running some

: A

with continuation

A → B

is equivalent to running

with the

identity continuation and then passing the result to k, i.e., e B k ≡ k (e A id).

To formalize this intuition in our target language, we rst add new syntax for the application of a

computation to its answer type and continuation:

e @ A e

′

. Next, we internalize the aforementioned

free theorem by adding two rules to our target language. The rst is the following typing rule

which records (a representation of) the value of a computation while type checking a continuation.

That is, it allows us to assume y ≡ e

id when type checking the body of e

’s continuation.

Γ ⊢ e : Π α : ∗. (A → α ) → α Γ ⊢ B : ∗ Γ, x = e A id ⊢ e

′

: B

Γ ⊢ e @ B (λ x : A. e

′

) : B

[T-Cont]

The second is the following equivalence rule, which is justied by the free theorem. Intuitively,

this rule normalizes CPS’d computations to the “value” e

id.

Γ ⊢ (e

@ B (λ x : A. e

)) ≡ (λ x : A. e

) (e

A id)

[≡-Cont]

Here is the updated CPS translation

(snd

e :

B[fst e/x])

that leverages answer-type polymorphism:

λ α : ∗. λ k : B

[(fst e)

/x] → α . e

@ α (λ y : (Σ x : A

. B

). let z = (snd y) : B

[fst y/x] in z α k)

To type check e

@ α . . .

we use [T-Cont]. When type checking the body of e

’s continuation,

we have that

y ≡

(Σ x : A

) id

and recall that we need to show that

fst y ≡ (fst

)

. This requires

expanding

(fst

)

and making use of the [

≡

-Cont] rule we now have available in the target language.

Here is an informal sketch of the proof—we give the detailed proof in Section 5.1.

(fst e)

≡ e

@ α

′

(λ y. fst y) by (roughly) the translation of fst and by η-equivalence (1)

≡ (λ y. fst y) (e

(Σ x : A

. B

) id) by [≡-Cont] (2)

≡ fst (e

(Σ x : A

. B

) id) by reduction (3)

≡ fst y by y ≡ e

(Σ x : A

. B

) id (4)

The astute reader will have noticed that our CPS translation—as well as the new rules [T-Cont]

and [

≡

-Cont]—only uses the new

syntax for certain applications. Intuitively, we use

only

when type checking requires the free theorem.

Next, let’s look at the translation of Π types. Again, we start with a warm-up; consider the

following CBN double-negation CPS translation of e e

′

(where e : Π x : A. B and e

′

: A):

(e e

′

: B[e

′

/x])

= λ k : (B

′÷

/x]) → ⊥. e

(λ f : Π x : A

. B

. (f e

′÷

) k)

The above type checks (as seen by inspecting the types of

and

). Notice that e

′÷

appears as an

argument to f so the type of f e

′

: B

′

/x].

Now consider the CBV CPS translation based on double negation, which fails to type check. We

dene the CBV computation translation A

and value translation A

as follows.

= (A

→ ⊥) → ⊥ (Σ x : A. B)

= Σ x : A

. B

(Π x : A. B)

= Π x : A

. B

Since we’re doing a CBV translation, the translated argument Π is a value of type A

and the

translated component types for Σ are values of types A

and B

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:9

Here is the CBV CPS translation e e

′

(where e : Π x : A. B and e

′

: A):

(e e

′

: B[e

′

/x])

= λ k : (B

′+

/x]) → ⊥. e

(λ f : Π x : A

. B

. e

′÷

(λ x : A

. (f x) k))

For the moment, ignore that our type annotation on

′+

/x])

, seems to requires a value

translation of terms e

′+

, which we can’t normally dene. Instead, notice that unlike in the CBN

translation, we now evaluate the argument

′

before calling

, so in CBV we have the application

f x

[x/x]

. This translation fails to type check since the computation

f x

expects a continuation

of type

[x/x]) → ⊥

but

has type

′+

/x]) → ⊥

. Somehow we need to show that

x ≡ e

′

. This

situation is almost identical to what we saw with the failing CBN translation of

snd

e. Analogously,

this time we ask what is the relationship between

and

′

, or

′

? As before, we note that the

only value that can ow into x is the unique underlying value in e

′

Hence, fortunately, the solution is again to do what we did for the CBN translation: adopt a CPS

translation based on answer-type polymorphism. As before, we change the computation translation

to A

= Π α : ∗. (A

→ α ) → α . Here is the updated CBV CPS translation of (e e

′

: B[e

′

/x])

λ α : ∗. λ k : (B

[(e

′

id)/x]) → α . e

α (λ f : Π x : A

. B

. e

′÷

@ α (λ x : A

. (f x) α k))

First, notice that we use the new

form when evaluating the argument

′

, which tells us we’re

using our new typing rule to record the value of e

′÷

while we type check its continuation. Second,

notice the type annotation on

. Earlier we observed that the type annotation for

′+

/x])

seemed to require a value translation on terms

′

that cannot normally be dened. Our translation

gives us a sensible way of modeling the value translation of a term by invoking a computation

with the identity continuation—so

′

is just the underlying value in

′

, i.e.,

′

id)

. This is an

important point to note: unlike CBN CPS, where we can substitute computations for variables, in

CBV CPS we must nd a way to extract the underlying value from computations of type A

since

variables expect values of type A

. Without answer-type polymorphism, CBV CPS is, in some sense,

much more broken than CBN CPS! Indeed, Barthe et al

(1999) already gave a CBN double-negation

CPS translation for CC’s Π types, but typed CBV double-negation CPS of Π types fails.

Using the new typing rule and equivalence rule that we already added to our target languages,

we are able to type check the above translation of e e

′

in essentially the same way as we did for the

CBN translation of snd e. We show the detailed proof in Section 6.1.

The reader may worry that our CBV CPS translation produces many terms of the form

k (

id)

which aren’t really in CPS since e

must return. However, notice that these only appear

in type annotations, not as run-time expressions. We only run a computation with the identity

continuation to convert a CPS expression into a value in the types for deciding type equivalence. The

run-time terms are all in CPS and can be run in a machine-like semantics in which computations

do not return.

4 THE CALCULUS OF CONSTRUCTIONS WITH CPS AXIOMS (CC

)

Our target language CC

is CC extended with a syntax for parametric reasoning about computations

in CPS form, as discussed in Section 3. We present these extensions formally in Figure 5. We add

the form

e @ A e

′

to the syntax of CC

. This form represents a computation

applied to the

answer type

and the continuation

′

. The dynamic semantics are the same as standard application.

The equivalence rule [

≡

-Cont] states that a computation

applied to its continuation

λ x : B. e

′

is equivalent to the application of that continuation to the underlying value of

. We extract the

underlying value by applying

to the “halt continuation”, encoded as the identity function in our

system. The rule [T-Cont] is used to type check applications that use our new

syntax. This typing

rule internalizes the fact that a continuation will be applied to one particular input, rather than

an arbitrary value. It tells the type system that the application of a computation to a continuation

e @ A (λ x : B. e

′

)

jumps to the continuation

′

after evaluating

to a value and binding the result

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:10 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Extensions to Syntax, Figure 1

e ::= · · · | e @ A e

′

Extensions to Convertibility and Equivalence, Figure 2

Γ ⊢ e ▷ e

′

. . .

λ α : ∗. e

@ A e

▷

[A/α ]) e

Γ ⊢ e ≡ e

′

. . . Γ ⊢ (e

@ A (λ x : B. e

)) ≡ (λ x : B. e

) (e

B id)

[≡-Cont]

Extensions to Typing, Figure 3

Γ ⊢ e : A

. . .

Γ ⊢ e : Π α : ∗. (B → α ) → α Γ ⊢ A : ∗ Γ, x = e B id ⊢ e

′

: A

Γ ⊢ e @ A (λ x : B. e

′

) : A

[T-Cont]

Fig. 5. CC

: CC with extensions

. We check the body of the continuation

′

under the assumption that

x = e B id

, i.e., with the

equality that the name

refers to the underlying value in the computation

, which we access using

the interface given by the polymorphic answer type.

The rule [

≡

-Cont] is a declarative rule that requires explicit symmetry and transitivity rules

to complete the denition (elided here, but included in the supplementary material). We give a

declarative presentation of this rule for clarity.

Note that [

≡

-Cont] and [T-Cont] internalize a specic “free theorem” that we need to prove type

preservation of the CPS translation. In particular, [

≡

-Cont] only holds when the CPS’d term

has the expected parametric type

Π α : ∗. (A → α ) → α

given in [T-Cont]. Notice, however, that our

statement of [

≡

-Cont] does not put any requirements on the type of

. This is because we use

an untyped equivalence based on the presentation of CIC in Coq (The Coq Development Team

2017, Chapter 4), and this untyped equivalence is necessary in our type-preservation proof (see

Section 5.1). Therefore, we cannot simply add typing assumptions directly to [

≡

-Cont]. Instead,

we rely on the fact that the term

e @ A e

′

has only one introduction rule, [T-Cont]. Since there is

only one applicable typing rule, anytime

e @ A e

′

appears in our type system,

has the required

parametric type. Furthermore, while our equivalence is untyped, we never appeal to equivalence

with ill-typed terms; we only refer to the equivalence

′

≡ B

′

in [Conv] after checking that both

′

and

′

are well-typed. For example, suppose the term

e @ A e

′

occurs in type

′

, and to prove

that

′

≡ B

′

requires our new rule [

≡

-Cont]. Because

′

is well-typed, we know that its subterms,

including

e @ A e

′

, are well-typed. Since

e @ A e

′

can only be well-typed by [T-Cont], we know

has the required parametric type.

Finally, notice that in [T-Cont] and [

≡

-Cont] we use standard application syntax for the term

e B id

. We only use the

syntax in our CPS translation when we require one of our new rules. The

type of the identity function doesn’t depend on any value, so we never need [T-Cont] to type-check

the identity continuation. In a sense,

e B id

is the normal form of a CPS’d “value” so we never need

[

≡

-Cont] to rewrite this term—i.e., using [

≡

-Cont] to rewrite

e B id

id (e B id)

would just evaluate

the original term.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:11

Γ ⊢ e

≡ e

. . .

Γ ⊢ p : e

= e

Γ ⊢ e

≡ e

[≡-Ext]

Fig. 6. Additional Equivalence Rule for Extensional CC

4.1 Consistency of CC

We prove that CC

is consistent by giving a model of CC

in the extensional Calculus of Construc-

tions. Boulier et al. (2017) provide a detailed explanation of this standard technique.

The idea behind the model is that we can translate each use of [

≡

-Cont] in CC

to a propositional

equivalence in extensional CC. Next, we translate any term that is typed by [T-Cont] into a

dependent let. Finally, we establish that if there were a proof of

False

in CC

, our translation would

construct a proof of

False

in extensional CC. But since extensional CC is consistent, there can be

no proof of False in CC

. We construct the model in three parts.

(1)

produce proofs (in extensional CC) of all propositional equivalences introduced by our

translation of [≡-Cont],

(2) show False in CC

is translated to False in extensional CC,

(3)

show our translation is type preserving, i.e., it translates a proof of

to a proof of its

translation A

◦

As our model is in the extensional CC, it is not clear that type checking in CC

is decidable. We

believe that type checking should be decidable for all programs produced by our compiler, since type

checking in our source language CC is decidable. In the worst case, to ensure decidability we could

change our translation to use a propositional version of [

≡

-Cont]. The denitional presentation

is simpler, but it should be possible to change the translation so that, in any term that currently

relies on [

≡

-Cont], we insert type annotations that compute type equivalence using a propositional

version of [≡-Cont]. We leave the issue of decidability of type checking in CC

for future work.

4.1.1 Modeling [

≡

-Cont]. The extensional Calculus of Constructions diers from our source

language CC in only one way: it allows using the existence of a propositional equivalence as a

denitional equivalence, as shown in Figure 6. The syntax and typing rules are exactly the same as

in CC presented in Section 2. We write terms in extensional CC using a italic, black, serif font.

In extensional CC we can model each use of the denitional equivalence [

≡

-Cont] by [

≡

-Ext],

as long as there exists a proof

(e A k) = (k (e B id))

, i.e., a propositional proof of [

≡

-Cont]; we

prove this propositional proof always exists by using the parametricity translation of Keller and

Lasson (2012). This translation gives a parametric model of CC in itself. This translation is based

on prior translations that apply to all Pure Type Systems (Bernardy et al

2012), but includes an

impredicative universe and provides a Coq implementation that we use.

The translation of a type

, written

, essentially transforms the type into a relation on terms

of that type. On terms

of type

, the translation

produces a proof that

is related to itself in the

relation given by

. For example, a type

∗

is translated to the relation

∗

= λ (x, x

′

: ∗). x → x

′

→ ∗

The translation of a polymorphic function type

Π α : ∗. A

is the following.

λ (f , f

′

: (Π α : ∗. A)). Π (α, α

′

: ∗). Π α

∗

α α

′

. (

(f α ) (f

′

))

This relation produces a proof that the bodies of functions

and

′

are related when provided a

relation

for the two types of

and

′

. This captures the idea that functions at this type must

behave parametrically in the abstract type

. This translation gives us Theorem 4.1 (Parametricity

for extensional CC), i.e., that every expression in extensional CC is related to itself in the relation

given by its type.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:12 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Γ ⊢ e : A {

◦

. . .

Γ ⊢ e : _ {

◦

e Γ ⊢ B : _ {

◦

B Γ ⊢ A : _ {

◦

A Γ, x = e B id ⊢ e

′

: A {

◦

′

Γ ⊢ e @ A (λ x : B. e

′

) : A {

◦

let x = e B id : B in e

′

[Un-Cont]

Fig. 7. Translation from CC

to Extensional CC (excerpt)

Theorem 4.1 (Parametricity for extensional CC). If Γ ⊢ t : t

′

then

⊢

′

t t

We apply Theorem 4.1 to our CPS type

Π α : ∗. (B → α ) → α

to prove Lemma 4.1. Since a CPS’d

term is a polymorphic function, we get to provide a relation

for the type

. The translation

then gives us a proof that

e A k

and

e B id

are related by

, so we simply choose

to be a relation

that guarantees

e A k = k (e B id)

. We formalize part of the proof in Coq in our supplementary

materials (Bowman et al

2017). By [

≡

-Ext], Theorem 4.1, and the relation just described, we arrive

at a proof of Lemma 4.1 for CPS’d computations encoded in the extensional CC.

Lemma 4.1 (Continuation Shuffling). If

Γ ⊢ A : ∗

Γ ⊢ B : ∗

Γ ⊢ e : Π α : ∗. (B → α ) → α

Γ ⊢ k : B → A, and Γ ⊢ e : Π α : ∗. (B → α) → α then Γ ⊢ e A k ≡ k (e B id)

Note that this lemma relies on the type of the term

. We must only appeal to this lemma, and

the equivalence justied by it, when

has the right type. In CC

, this is guaranteed by the typing

rule [T-Cont], as discussed earlier in this section.

4.1.2 Modeling [T-Cont]. In Figure 7 we present the key translation rule for modeling CC

extensional CC. All other rules are inductive on the structure of typing derivations. Note that since

we only need to justify the additional typing rule [T-Cont], this is the only rule that is changed

by the translation. This translation rule is essentially the same rule from the inverse CPS given

by Flanagan et al

(1993), although we do not necessarily produce output in A-normal form (ANF)

since we only translate uses of this one typing rule. We discuss CPS and ANF in detail in Section 7.

For brevity in our proofs, we dene the following notation for the translation of terms and types

from CC

into extensional CC.

◦

def

= e where Γ ⊢ e : A {

◦

By writing

◦

, we refer to the term produced by the translation with the typing derivation

Γ ⊢ e : A

as an implicit parameter.

First, we show that the denition of False is preserved. We dene

False

Π α : ∗. α

, i.e., the

function that accepts any proposition and returns a proof that the proposition holds. It is simple

to see that this type has type

∗

in CC

by the rule [Prod-*]. Note that

Π α : ∗. α

is translated to

Π α : ∗. α of type ∗, i.e., False is translated to False.

Lemma 4.2 (False Preservation). Γ ⊢ (Π α : ∗. α ) : ∗ {

◦

Π α : ∗. α

Next, to show type preservation, we must rst show that equivalence is preserved since the

type system appeals to equivalence. A crucial lemma to both equivalence preservation and type

preservation is compositionality, which says that the translation commutes with substitution. The

proof is straightforward by induction on the typing derivation of

. See our technical appendix for

details (Bowman et al. 2017).

Lemma 4.3 (Compositionality). (e[e

′

/x])

◦

≡ e

◦

′◦

/x]

The equivalence rules of extensional CC with the addition of Lemma 4.1 (Continuation Shuing)

are the same as CC

. Therefore, to show that equivalence is preserved, it suces to show that

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:13

reduction sequences are preserved. We rst show that single-step reduction is preserved, Lemma 4.4,

which easily implies preservation of reduction sequences, Lemma 4.5.

Lemma 4.4 (Preservation of One-Step Reduction). If e

▷ e

, then e

◦

▷

⋆

′

and e

◦

≡ e

′

Proof. By cases on the reduction step e

▷ e

. There is one interesting case.

Case e = (λ α : ∗. e

) @ B (λ x

′

: A. e

) ▷

[B/α ]) (λ x

′

: A. e

)

By denition e

◦

= (let x

′

= ((λ α : ∗. e

)

◦

id) in e

◦

) ▷

◦

[((λ α : ∗. e

)

◦

id)/x

′

]

We must show ((e

[B/α ]) (λ x

′

: A. e

))

◦

≡ e

◦

[((λ α : ∗. e

)

◦

id)/x

′

((e

[B/α ]) (λ x

′

: A. e

))

◦

(5)

≡ ((e

◦

/α]) (λ x

′

: A

◦

. e

◦

)) by Lemma 4.3 and denition of

◦

(6)

≡ (λ α : ∗. e

◦

) B

◦

(λ x

′

: A

◦

. e

◦

) by [≡] and ▷

(7)

≡ (λ x

′

: A

◦

. e

◦

) ((λ α : ∗. e

◦

) A

◦

id) by Lemma 4.1 (Continuation Shuing) (8)

≡ e

◦

[((λ α : ∗. e

◦

) A

◦

id)/x

′

] by [≡] and ▷

(9)

≡ e

◦

[((λ α : ∗. e

)

◦

id)/x

′

] by Lemma 4.3 (10)

□

Lemma 4.5 (Preservation of Reduction Seqences). If e

▷

⋆

, then e

◦

▷

⋆

′

and e

◦

≡ e

′

Lemma 4.6 (Eqivalence Preservation). If e

≡ e

, then e

◦

≡ e

◦

Finally, we can show type preservation, which completes our proof of consistency. Since the

translation is homomorphic on all typing rules except [T-Cont], there is only one interesting case

in the proof of Lemma 4.7. We must show that [Un-Cont] is type preserving. Note that the case for

[Conv] appeals to Lemma 4.6.

Lemma 4.7 (Type Preservation). If Γ ⊢ e : A then Γ

◦

⊢ e

◦

: A

◦

Proof. By induction on the derivation Γ ⊢ e : A. There is one interesting case.

Case [T-Cont]

We have the following.

Γ ⊢ e

: Π α : ∗. (B → α ) → α Γ ⊢ A : ∗ Γ, x

′

= e

B id ⊢ e

: A

Γ ⊢ e

@ A (λ x

′

: B. e

) : A

We must show Γ

◦

⊢ let x

′

= (e

◦

id) in e

◦

: A

◦

By [Let], it suces to show

• Γ

◦

⊢ (e

◦

id) : B

◦

, which follows easily by the induction hypothesis applied to the

premises of [T-Cont].

• Γ

◦

, x

′

= (e

◦

id)

◦

⊢ e

◦

: A

◦

, which follows immediately by the induction hypothesis.

□

Theorem 4.2 (Consistency of CC

). There does not exist a close d term e such that · ⊢ e : False.

5 CALL-BY-NAME CPS TRANSLATION OF CC

We now present our call-by-name CPS translation (CPS

) of CC. The main dierences between our

translation and the one by Barthe and Uustalu (2002) are that we use a locally polymorphic answer

type instead of a xed answer type, which enables our type-preservation proof of

snd

e, and that

we use a domain-full target language, which supports decidable type-checking.

As we discussed in Section 3, we need a computation translation and a value translation on

types. But in addition to types, we will need to translate universes, kinds, and terms as well. All

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:14 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

of our translations are dened by induction on the typing derivations. This is important when

translating to a domain-full target language, since the domain annotations we generate come from

the type of the term we are translating. However, as in Section 3, we nd it useful to abbreviate

these with t

(for computation) and t

(for value translation). Below we give abbreviations for all

of the translation judgments we dene for our CPS translation. Note that anywhere we use this

notation, we require the typing derivation as an implicit parameter.

def

= A where Γ ⊢ A : ∗ {

def

= e where Γ ⊢ e : A {

def

= U where Γ ⊢ U {

def

= κ where Γ ⊢ κ : U {

def

= A where Γ ⊢ A : κ {

The CPS

translations on universes, kinds, and types are dened in Figure 8. We dene the

translation for kinds CPS

and universe CPS

, which we abbreviate with

. There is no separate

computation translation for kinds or universes. We only have separate computation and value

translations for types since we only internalize the concept of evaluation at the term-level, and

types describe term-level computations and term-level values. Recall that this is the call-by-name

translation, so function arguments, even type-level functions, are still computations. Note, therefore,

that the rule [CPS

-ProdA] uses the computation translation on the domain annotation A of Π

x:A. κ

—

i.e., the kind describing a type-level function that abstracts over a term of type A.

For types, we dene a value translation CPS

and a computation translation CPS

. Most rules

are straightforward. We translate type-level variables

in-place in rule [CPS

-Var]. Again, since this

is the CBN translation, we use the computation translation on domain annotations. The rule [CPS

Constr] for the value translation of type-level functions that abstract over a term,

λ x :A.

B, translates

the domain annotation A using the computation translation. The rule for the value translation of a

function type, [CPS

-Prod], translates the domain annotation A using the computation translation.

This means that a function is a value when it accepts a computation as an argument. The rule

[CPS

-Sigma] produces the value translation of a pair type by translating both components of a

pair using the computation translation. This means we consider a pair a value when it contains

computations as components. Note that since our translation is dened on typing derivations, we

have an explicit translation of the conversion rule [CPS

-Conv].

There is only one rule for the computation translation of a type, [CPS

-Comp], which is the

polymorphic answer type translation described in Section 3. Notice that [CPS

-Comp] is dened

only for types of kind

∗

, since only types of kind

∗

have inhabitants. For example, we cannot apply

[CPS

-Comp] to type-level function since no term inhabits a type-level function.

The CPS

translation on terms is dened in Figure 9. Intuitively, we translate each term e of type

A to

of type

Π α : ∗. (A → α ) → α

, where

is the value translation of A. This type represents a

computation that, when given a continuation

that expects a value of type

, promises to call

with a value of type

. Since we have only two value forms in the call-by-name translation, we do

not explicitly dene a separate value translation, but inline that translation. Note that the value

cases, [CPS

-Fun] and [CPS

-Pair], feature the same pattern: produce a computation

λ α . λ k. k v

that expects a continuation and then immediately calls that continuation on the value

. In the

case of [CPS

-Fun], the value

is the function

λ x : A. e

produced by translating the source function

λ x :A.

e using the computation type translation from A

{

and the computation term translation

{

. In the case of [CPS

-Pair], the value we produce

⟨e

, e

⟩

contains computations, not values.

The rest of the translation rules are for computations. Notice that while all terms produced by

the term translation have a computation type, all continuations take a value type. Since this is a

CBN translation, we consider variables as computations in [CPS

-Var]. We translate term variables

as an

-expansion of a CPS’d computation. We must

-expand the variable case to guarantee CBN

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:15

Γ ⊢ U {

Γ ⊢ ∗ {

∗

[CPS

-Star]

Γ ⊢ □ {

□

[CPS

-Box]

Γ ⊢ κ : U {

κ Lemma 5.5 will show Γ

⊢ κ

: U

Γ ⊢ ∗ : □ {

∗

[CPS

-Ax]

Γ ⊢ κ : U {

κ Γ, α : κ ⊢ κ

′

: U

′

{

′

Γ ⊢ Π α : κ. κ

′

: U

′

{

Π α : κ . κ

′

[CPS

-ProdK]

Γ ⊢ A : κ

′

{

A Γ, x : A ⊢ κ : U {

Γ ⊢ Π x : A. κ : U {

Π x : A. κ

[CPS

-ProdA]

Γ ⊢ A : κ {

A Lemma 5.5 will show Γ

⊢ A

: κ

. . . Γ ⊢ α : κ {

[CPS

-Var]

Γ ⊢ A : κ

′

{

A Γ, x : A ⊢ B : κ {

Γ ⊢ λ x : A. B : Π x : A. κ {

λ x : A. B

[CPS

-Constr]

Γ ⊢ A : Π x : B. κ {

A Γ ⊢ e : B {

Γ ⊢ A e : κ[e/x] {

A e

[CPS

-AppConstr]

Γ ⊢ A : κ {

A Γ, x : A ⊢ B : κ

′

{

Γ ⊢ Π x : A. B : κ

′

{

Π x : A. B

[CPS

-Prod]

Γ ⊢ κ : U {

κ Γ, x : A ⊢ B : κ

′

{

Γ ⊢ Π α : κ. B : κ

′

{

Π α : κ . B

[CPS

-ProdK]

Γ ⊢ e : A {

e Γ ⊢ A : κ {

A Γ, x = e : A ⊢ B : κ

′

{

Γ ⊢ let x = e : A in B : κ

′

{

let x = e : A in B

[CPS

-Let]

Γ ⊢ A : ∗ {

A Γ, x : A ⊢ B : ∗ {

Γ ⊢ Σ x : A. B : ∗ {

Σ x : A. B

[CPS

-Sigma]

Γ ⊢ A : κ

′

Γ ⊢ κ ≡ κ

′

Γ ⊢ A : κ

′

{

Γ ⊢ A : κ {

[CPS

-Conv]

Γ ⊢ A : ∗ {

A Lemma 5.5 will show Γ

⊢ A

: ∗

Γ ⊢ A : ∗ {

Π α : ∗. (A → α ) → α

[CPS

-Comp]

Fig. 8. CPS

of Universes, Kinds, and Types (excerpts)

evaluation order, as we discuss shortly. In [CPS

-App] we encode the CBN evaluation order for

function application e e

′

in the usual way. We translate the computations e

{

and e

′

{

′

First we evaluate

to a value

, then apply

to the computation

′

. The application

f e

′

is itself a

computation, which we call with the continuation k.

Notice that only the translation rules [CPS

-Fst] and [CPS

-Snd] use the new

form. As discussed

in Section 3, to type check the translation of

snd

e produced by [CPS

-Snd], we require the rule

[T-Cont] when type checking the continuation that performs the second projection. While type

checking the continuation, we know that the value

that the continuation receives is equivalent to

α id

. Now, the reason we must use the

syntax in the in the translation [CPS

-Fst] is so that

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:16 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Γ ⊢ e : A {

A Lemma 5.5 will show Γ

⊢ e

: A

. . .

Γ ⊢ A : κ {

Γ ⊢ x : A {

λ α : ∗. λ k : A → α . x α k

[CPS

-Var]

Γ ⊢ A : κ {

A Γ, x : A ⊢ B : κ

′

{

B Γ, x : A ⊢ e : B {

Γ ⊢ λ x : A. e : Π x : A. B {

λ α : ∗. λ k : (Π x : A. B) → α . k (λ x : A. e)

[CPS

-Fun]

Γ ⊢ e : Π x : A. B {

e Γ ⊢ A : κ {

Γ, x : A ⊢ B : κ

′

{

Γ, x : A ⊢ B : κ

′

{

Γ ⊢ e

′

: A {

′

Γ ⊢ e e

′

: B[e

′

/x] {

λ α : ∗. λ k : (B

′

/x]) → α .

e α (λ f : Π x : A

. B

. (f e

′

) α k)

[CPS

-App]

Γ ⊢ e : A {

Γ ⊢ A : κ {

A Γ, x = e : A ⊢ B : κ

′

{

B Γ, x = e : A ⊢ e

′

: B {

′

Γ ⊢ let x = e : A in e

′

: B[e/x] {

λ α : ∗. λ k : B[e/x] → α . let x = e : A in e

′

α k

[CPS

-Let]

Γ ⊢ e

: A {

Γ ⊢ e

: B[e

/x] {

Γ ⊢ A : ∗ {

A Γ, x : A ⊢ B : ∗ {

Γ ⊢ ⟨e

, e

⟩ : Σ x : A. B {

λ α : ∗. λ k : Σ x : A. B → α . k ⟨e

, e

⟩ as Σ x : A. B

[CPS

-Pair]

Γ ⊢ A : ∗ {

Γ, x : A ⊢ B : ∗ {

Γ ⊢ A : ∗ {

Γ ⊢ e : Σ x : A. B {

Γ ⊢ fst e : A {

λ α : ∗. λ k : A

→ α .

e @ α (λ y : Σ x : A

. B

. let z = fst y in z α k)

[CPS

-Fst]

Γ ⊢ A : ∗ {

Γ, x : A ⊢ B : ∗ {

Γ ⊢ (fst e) : A {

(fst e)

Γ ⊢ e : Σ x : A. B {

Γ ⊢ snd e : B [(fst e)/x] {

λ α : ∗. λ k : B

[(fst e)

/x] → α .

e @ α (λ y : Σ x : A

. B

. let z = snd y in z α k)

[CPS

-Snd]

Γ ⊢ e : B {

Γ ⊢ e : A {

[CPS

-Conv]

⊢ Γ {

Γ Lemma 5.5 will show ⊢ Γ

⊢ · {

[CPS

-Empty]

⊢ Γ {

Γ Γ ⊢ A : κ {

⊢ Γ, x : A {

Γ, x : A

[CPS

-AssumT]

⊢ Γ {

Γ Γ ⊢ κ : U {

⊢ Γ, α : κ {

Γ, α : κ

[CPS

-AssumK]

⊢ Γ {

Γ Γ ⊢ A : κ {

A Γ ⊢ e : A {

⊢ Γ, x = e : A {

Γ, x = e : A

[CPS

-Def]

⊢ Γ {

Γ Γ ⊢ A : κ {

A Γ ⊢ κ : U {

⊢ Γ, α = A : κ {

Γ, α = A : κ

[CPS

-DefT]

Fig. 9. CPS

of Terms and Environments (excerpts)

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:17

we can apply the [

≡

-Cont] rule to resolve the equivalence of the two rst projections in the type

of the second projection. That is, as we saw in Section 3, type preservation fails because we must

show equivalence between

(fst

)

and

fst y

. Since these are the only two cases that require our new

rules, these are the only cases where we use the

form in our translation; all other translation

rules use standard application. In Section 6, we will see that the CBV translation must use the

form much more frequently since, intuitively, our new equivalence rule recovers a notion of “value”

in our CPS’d language, and in call-by-value types can only depend on values.

Our CPS translation encodes the CBN evaluation order explicitly so that the evaluation order

of compiled terms is independent of the target language’s evaluation order. This property is not

immediately obvious since the [CPS

-Let] rule binds a variable

to an expression

, making it

seem like there are two possible evaluation orders: either evaluate

rst, or substitute

for

rst.

Note, however, that our CBN translation always produces a

term—even in the variable case since

[CPS

-Var] employs

-expansion as noted above. Therefore, in the [CPS

-Let] rule

will always be

a value, which means it doesn’t evaluate in either CBN or CBV. Therefore, there is no ambiguity in

how to evaluate the translation of let.

The translation rule [CPS

-Conv] is deceptively simple. We could equivalently write this transla-

tion as follows, which makes its subtlety apparent.

Γ ⊢ e : B Γ ⊢ A ≡ B Γ ⊢ e : B {

e Γ ⊢ A : κ {

A Γ ⊢ B : κ {

Γ ⊢ e : A {

λ α : ∗. λ k : A → α . e α (λ x : B. k x)

[CPS

-Conv]

Notice now that while the continuation

expects a term of type

, we call

with a term of type

Intuitively, this should be ne since

and

should be equivalent, but formally this introduces a

subtlety in the staging of our proof of type preservation, which we discuss next in Section 5.1.

We lift the translations to environments in the usual way, at the bottom of Figure 9. Since this is

the CBN translation, we recur over the environment applying the computation translation.

5.1 Proof of Type Preservation for CPS

In a dependent type system, type preservation requires coherence, which essentially tells us that

the translation preserves denitional equivalence. Since equivalence is dened by reduction, we

rst have to show that reduction sequences are preserved. Since reduction relies on substitution,

we rst must show compositionality, i.e., that the translation commutes with substitution.

However, there is a problem with the proof architecture for CPS. Typed CPS for a domain-

full target language inserts the type of every term into the output as a type annotation on the

continuation. For example, e : A is compiled to

λ α : ∗. λ k :A

→ α . (. . . )

. Therefore, the translation is

dened on typing derivations, not on syntax. This introduces a problem in the case of the translation

of the typing rule [Conv]. As alluded to above when describing [CPS

-Conv], in order to preserve

typing, we must rst show coherence, i.e., that we preserve equivalence. Working with the second

denition we gave for the [CPS

-Conv] rule, we need to show that the following term is well-typed.

λ k : A

→ α . e

α (λ x : B

. k x)

Note that this term seems to only make sense when A

≡

. While we have A

≡

B from the source

typing derivation, we don’t know that A

≡

unless we have coherence. But if equivalence is only

dened on well-typed terms, as is the case in some dependently typed languages, we must rst prove

type preservation to know that A

and B

are well typed before we can prove coherence. So we

have a circularity: type preservation requires coherence, but coherence requires type preservation.

A similar problem arises in other dependent typing rules, like the translation of application.

In the case of application, to show type preservation we must show compositionality, i.e., that

the translation commutes with substitution up to equivalence. Again we have a circularity: we

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:18 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

need type preservation to prove compositionality, but to prove compositionality we need type

preservation.

Barthe et al

(1999) explain this in detail, and their solution is to use a domain-free target language.

This avoids the circularity because when there are no type annotations to generate, the translation

can be dened on the syntax instead of typing derivations.

We solve the problem by using an untyped equivalence, which is based on the equivalence for

the Calculus of Inductive Constructions from the Coq reference manual (The Coq Development

Team 2017, Chapter 4). Since the equivalence is untyped, we can show equivalence between terms

with dierent domain annotations as long as their behavior is equivalent. This allows us to stage

the proof: we can prove compositionality before coherence, and prove coherence before type

preservation. While it seems surprising that we can prove equivalence between possibly ill-typed

terms, recall that in the type system, we only appeal to the equivalence after checking that the

terms we wish to prove equivalent are well typed. We can think of this equivalence as proving

a stronger equivalence than we provide for well-typed terms, allowing us to prove a stronger

form of coherence: in addition to preserving all well-typed equivalences, we also preserve certain

equivalences that are valid according to their dynamic behavior, but conservatively ruled out by

the strong type system. From this version of coherence, we are able to prove type preservation.

The proofs in this section are staged as follows. First we show compositionality (Lemma 5.1),

since reduction is dened in terms of substitution. Then we show that the translation preserves

reduction sequences (Lemma 5.2 and Lemma 5.3), which allows us to show coherence (Lemma 5.4).

Using compositionality and coherence, we prove that the translation is type preserving (Lemma 5.5).

We now show Lemma 5.1, which states that the CPS

translation commutes with substitution.

The formal statement of the lemma is somewhat complicated since we have the cross product of

four syntactic categories and two translations. However, the intuition is simple: rst substituting

and then translating is equivalent to translating and then substituting.

This lemma is critical to our proofs. Since reduction is essentially dened by substitution, this

lemma does most of the work in showing that the translation preserves reduction. However, it is

also necessary in type preservation when showing that a dependent type is preserved. A dependent

type, such as

B[e

′

/x]

produced by the rule [App], occurs when we perform substitution into a type.

We want to show, for example, that if e :

B[e

′

/x]

then the translation of e has the type translation

(B[e

′

/x])

. Since our translation is compositional, i.e., commutes with substitution, we know how

to translate B[e

′

/x] by simply translating B and e

′

Lemma 5.1 (CPS

Compositionality).

(1) (κ[A/α])

≡ κ

/α ]

(2) (κ[e/x])

≡ κ

/x]

(3) (A[B/α])

≡ A

/α ]

(4) (A[e/x])

≡ A

/x]

(5) (A[B/α])

≡ A

/α ]

(6) (A[e/x])

≡ A

/x]

(7) (e[A/α])

≡ e

/α ]

(8) (e[e

′

/x])

≡ e

′÷

/x]

Proof.

In the PTS syntax, we represent source expressions as

t[t

′

/x]

. The proof is by induction on

the typing derivations for t. Note that our

and

notation implicitly require the typing derivations

as premises. The proof is completely straightforward.

Case

[Conv]. The proof is trivial, now that we have staged the proof appropriately. We give

part 8 as an example.

Γ ⊢ e : B Γ ⊢ A : U Γ ⊢ A ≡ B

Γ ⊢ e : A

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:19

We must show that

(e[e

′

/x])

≡ e

′÷

/x]

(at type A). Note that by part 8 of the induction

hypothesis, we know that

(e[e

′

/x])

≡ e

′÷

/x]

(at the smaller derivation for type B). But

recall that our equivalence cares nothing for types, so the proof is complete. □

We next prove that the translation preserves reduction sequences, Lemma 5.2 and Lemma 5.3.

Note that kinds do not take steps in the one step reduction, but can in the

▷

⋆

relation since it

reduces under all contexts. As mentioned earlier, this is necessary to show equivalence is preserved,

since equivalence is dened in terms of reduction.

Lemma 5.2 (CPS

Preserves One-Step Reduction).

• If Γ ⊢ e : A and e ▷ e

′

then e

▷

⋆

′

and e

′

≡ e

′÷

• If Γ ⊢ A : κ and A ▷ A

′

then A

▷

⋆

′

and A

′

≡ A

′+

• If Γ ⊢ A : ∗ and A ▷ A

′

then A

▷

⋆

′

and A

′

≡ A

′÷

Proof. The proof is straightforward by cases on the ▷ relation. □

Lemma 5.3 (CPS

Preserves Reduction Seqences).

• If Γ ⊢ e : A and e ▷

⋆

′

then e

▷

⋆

′

and e

′

≡ e

′÷

• If Γ ⊢ A : κ and A ▷

⋆

′

then A

▷

⋆

′

and A

′

≡ A

′+

• If Γ ⊢ A : ∗ and A ▷

⋆

′

then A

▷

⋆

′

and A

′

≡ A

′÷

• If Γ ⊢ κ : U and κ ▷

⋆

′

then κ

▷

⋆

′

and κ

′

≡ κ

′+

Proof.

The proof is straightforward by induction on the length of the reduction sequence. The

base case is trivial and the inductive case follows by Lemma 5.2 and the inductive hypothesis.

□

Lemma 5.4 (CPS

Coherence).

• If e ≡ e

′

then e

≡ e

′÷

• If A ≡ A

′

then A

≡ A

′+

• If A ≡ A

′

then A

≡ A

′÷

• If κ ≡ κ

′

then κ

≡ κ

′+

Proof.

The proof is by induction on the derivation of e

≡

′

. The base case follows by Lemma 5.3,

and the cases of

-equivalence follow from Lemma 5.3, the induction hypothesis, and the fact that

we have the same η-equivalence rules in the CC

. □

We rst prove type preservation, Lemma 5.5, using the explicit syntax on which we dened

CPS

. This proof is our central contribution to the call-by-name translation. In this lemma, proving

that the translation of

snd

e preserves typing requires both the new typing rule [T-Cont] and the

equivalence rule [

≡

-Cont]. The rest of the proof is straightforward. For full details, see our online

supplementary materials (Bowman et al. 2017).

Lemma 5.5 (CPS

is Type Preserving (Explicit Syntax)).

(1) If ⊢ Γ then ⊢ Γ

(2) If Γ ⊢ e : A then Γ

⊢ e

: A

(3) If Γ ⊢ A : κ then Γ

⊢ A

: κ

(4) If Γ ⊢ A : ∗ then Γ

⊢ A

: ∗

(5) If Γ ⊢ κ : U then Γ

⊢ κ

: U

Proof.

All cases are proven simultaneously by mutual induction on the type derivation and

well-formedness derivation. Part 4 follows easily by part 3 in every case, so we elide its proof. Most

cases follow easily from the induction hypotheses.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:20 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Case [Snd] Γ ⊢ snd e : B[fst e/x]

We must show that λ α : ∗. λ k : B

[(fst e)

/x] → α .

@ α (λ y : Σ x : A

. B

. let z = snd y in z α k)

has type (B[fst e/x])

By part 6 of Lemma 5.1, and denition of the translation, this type is equivalent to

Π α : ∗. (B

[(fst e)

/x] → α ) → α

By [Lam], it suces to show that

, α : ∗, k : B

[(fst e)

/x] → α ⊢ e

@ α (λ y : Σ x : A

. B

. let z = snd y in z α k) : α

This is the key diculty in the proof. Recall from Section 3 that the term

z α

has type

[fst y/x] → α ) → α

while the term

has type

[(fst e)

/x] → α

. To show that

z α k

well-typed, we must show that

(fst

)

≡ fst y

. We proceed by our new typing rule [T-Cont],

which will help us prove this.

First, note that e

(Σ x : A

) id

is well-typed. By part 4 of the induction hypothesis we

know that Γ

⊢

: ∗

and Γ

, x

: A

⊢

: ∗

. By part 2 of the induction hypothesis applied

to Γ ⊢ e : Σ x : A. B, we know Γ

⊢ e

: Π α : ∗. (Σ x : A

. B

→ α ) → α .

Now, by [T-Cont], it suces to show that

, α : ∗, k : B

[(fst e)

/x] → α , y = e

Σ x : A

. B

id ⊢ let z = snd y in z α k : α

Note that we now have the denitional equivalence

y = e

(Σ x : A

. B

) id

. By [Let] it

suces to show

, α : ∗, k : B

[(fst e)

/x] → α , y = e

Σ x : A

. B

id, z = snd y : B

[fst y/x] ⊢ z α k : α

Note that

z : B

[fst y/x] (11)

= Π α : ∗. (B

[fst y/x] → α ) → α by denition of B

(12)

≡ Π α : ∗. (B

[fst (e

_ id)/x] → α ) → α by δ reduction on y (13)

The Equation (13) above, in which we δ reduce y, is impossible without [T-Cont].

By [Conv], and since

[(fst e)

/x] → α

, to show

z α k

it suces to show that

(fst e)

≡ fst (e

_ id).

Note that (fst e)

= λ α : ∗. λ k

′

: (A

→ α ).

@ α (λ y : Σ x : A

. B

. let z

′

= fst y : A

in z

′

α k

′

)

by denition of the translation.

By [≡-η], it suces to show that

@ α (λ y : Σ x : A

. B

. let z

′

= fst y : A

in z

′

α k

′

) (14)

≡ (λ y : Σ x : A

. B

. let z

′

= fst y in z

′

α k

′

) (e

_ id) [≡-Cont] (15)

≡ (fst (e

_ id)) α k

′

by reduction (16)

Notice that Equation (15) requires our new equivalence rule applied to the translation of

the fst.

Case [Conv] Γ ⊢ e : A such that Γ ⊢ e : B and A ≡ B.

We must show that e

has type A

= Π α : ∗. (A

→ α ) → α .

By the induction hypothesis, we know that e

= Π α : ∗. (B

→ α ) → α

. By [Conv] it

suces to show that A

≡ B

, which follows by Lemma 5.4. □

To recover a simple statement of the type-preservation theorem over the PTS syntax, we dene

two meta-functions for translating terms and types depending on their use. We dene

cps

translate a PTS expression in “term” position, i.e., when used on the left side of a type annotation

as in t : t

′

, and we dene

cpsT

′

to translate an expression in “type” position, i.e., when used on

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:21

the right side of a type annotation. We dene these in terms of the translation shown above, noting

that for every t : t

′

in the PTS syntax, one of the following is true: t is a term e and t

′

is a type A in

the explicit syntax; t is a type A and t

′

is a kind

in the explicit syntax; or t is a kind

and t

′

is a

universe U in the explicit syntax.

cps

def

= e

when t is a term

cps

def

= A

when t is a type

cps

def

= κ

when t is a kind

cpsT

′

def

= A

when t

′

is a type

cpsT

′

def

= κ

when t

′

is a kind

cpsT

′

def

= U

when t

′

is a universe

This notation is based on Barthe and Uustalu (2002).

Theorem 5.1 (CPS

is Type Preserving (PTS syntax)). Γ ⊢ t : t

′

then Γ

⊢ cps

: cpsT

′

5.2 Proof of Correctness for CPS

Since type preservation in a dependently typed language requires preserving reduction sequences,

we have already done most of the work to prove two other compiler correctness properties: cor-

rectness of separate compilation, and whole-program compiler correctness. To specify compiler

correctness, we need an independent specication that tells us how source values—or, more gen-

erally, observations—are related to target values. For instance, when compiling to C we might

specify that the number 5 is related to the bits 0

101. Without a specication, independent of the

compiler, there is no denition that the compiler can be correct with respect to. In our setting, such

an independent specication is simple to construct. We can add ground values such as booleans to

our language with the obvious cross-language relation: True ≈ Tr ue and False ≈ False.

Next, to dene separate compilation, we need a denition of linking. We can dene linking as

substitution, and dene valid closing substitutions γ as follows.

Γ ⊢ γ

def

= ∀x : A ∈ Γ. ⊢ γ (x) : γ(A)

We extend the compiler in a straightforward way to compile closing substitutions, written

and allow compiled code to be linked with the compilation of any valid closing substitution

This denition supports a separate compilation theorem that allows linking with the output of our

compiler, but not with the output of other compilers.

Now we can show that the compiler is correct with respect to separate compilation: if we rst link

and run to a value, we get a related value when we compile and then link with the compiled closing

substitution. Since our target language is in CPS form, we should apply the halt continuation,

and compare the ground values.

Theorem 5.2 (Separate Compilation Correctness). If Γ

⊢

A where A is ground, and

γ (

) ▷

⋆

then γ

) A

id ▷

⋆

v and v ≈ v.

Proof.

Since reduction implies equivalence, we reason in terms of equivalence. By Lemma 5.3,

(γ (

))

▷

⋆

and v

≡ e

. By Lemma 5.1,

(γ (

))

≡ γ

(

)

, hence

(

) ▷

⋆

and v

≡ e

. Since the

translation on all ground values is v

= λ α . λ k. k v

, where v

≈ v

, we know v

id ▷

⋆

such that

≈ v

. Since v

≡ e ≡ γ

(

)

, we also know that

(

)

id ▷

⋆

′

and

′

≡ v

. Since

is ground,

′

= v and v ≈ v

′

. □

Corollary 5.1 (Whole-Program Compiler Correctness). If

⊢

A and e

▷

⋆

v then e

id ▷

⋆

v and v ≈ v.

Our separate-compilation correctness theorem is similar to the guarantees provided by SepCom-

pCert (Kang et al

2016) in that it supports linking with only the output of the same compiler. We

could support more exible notions of linking—such as linking with code produced by dierent

compilers, from dierent source languages, or code written directly in the target language—by

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:22 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Γ ⊢ κ : U {

κ Lemma 6.3 will show Γ

⊢ κ

: U

. . .

Γ ⊢ A : κ

′

{

A Γ, x : A ⊢ κ : U {

Γ ⊢ Π x : A. κ : U {

Π x : A. κ

[CPS

-ProdA]

Γ ⊢ A : κ {

A Lemma 6.3 will show Γ

⊢ A

: κ

. . .

Γ ⊢ A : κ

′

{

A Γ, x : A ⊢ B : κ {

Γ ⊢ λ x : A. B : Π x : A. κ {

λ x : A. B

[CPS

-Constr]

Γ ⊢ A : Π x : B. κ {

A Γ, x : A ⊢ B : κ

′

{

B Γ ⊢ e : B {

Γ ⊢ A e : κ[e/x] {

A (e B id)

[CPS

-AppConstr]

Γ ⊢ A : κ

′

{

A Γ, x : A ⊢ B : κ {

Γ ⊢ Π x : A. B : κ {

Π x : A. B

[CPS

-Prod]

Γ ⊢ κ : U

′

{

κ Γ, x : A ⊢ B : U {

Γ ⊢ Π α : κ. B : U {

Π α : κ . B

[CPS

-ProdK]

Γ ⊢ e : A {

e Γ ⊢ A : κ

′

{

A Γ, x = e : A ⊢ B : κ {

Γ ⊢ let x = e : A in B : κ {

let x = e A id : A in B

[CPS

-Let]

Γ ⊢ A : ∗ {

A Γ, x : A ⊢ B : ∗ {

Γ ⊢ Σ x : A. B : ∗ {

Σ x : A. B

[CPS

-Sigma]

Fig. 10. CPS

of Kinds and Types (excerpts)

dening an independent specication for when closing substitutions are related across languages

(e.g., (Ahmed and Blume 2011; Neis et al. 2015; New et al. 2016; Perconti and Ahmed 2014)).

6 CALL-BY-VALUE CPS TRANSLATION OF CC

In this section, we present the call-by-value CPS translation (CPS

) of CC. First, we redene our

short-hand from Section 5 to refer to call-by-value translation.

def

= A where Γ ⊢ A : ∗ {

def

= e where Γ ⊢ e : A {

def

= U where Γ ⊢ U {

def

= e where Γ ⊢ κ : U {

def

= A where Γ ⊢ A : κ {

Unlike CBN, the CBV translation forces every computation to a value. Therefore, every dependent

elimination requires our new [T-Cont] typing rule. Moreover, all substitutions of a term into a type

must substitute values instead of computations so all dependent type annotations must explicitly

convert computations to values by supplying the identity continuation.

We present our call-by-value translation CPS

in Figures 10 and 11. In general, CPS

diers

from CPS

in two ways. First, all term variables must have value types, so the translation rules for

all binding constructs now use the value translation for type annotations. Second, we change the

denition of value types so that functions must receive values and pairs must contain values.

The universe translation is unchanged from CPS

, so we omit it here. The kind translation

(Figure 10) has changed in only one place. Now the translation rule [CPS

-ProdA] translates the

kind of type-level functions Π x : A. κ to accept a value as argument x : A

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:23

Γ ⊢ e : A {

e Lemma 6.3 will show Γ

⊢ e

: A

. . .

Γ ⊢ A : κ {

Γ ⊢ x : A {

λ α : ∗. λ k : A → α . k x

[CPS

-Var]

Γ ⊢ A : κ

′

{

A Γ, x : A ⊢ B : κ {

B Γ, x : A ⊢ e : B {

Γ ⊢ λ x : A. e : Π x : A. B {

λ α : ∗. λ k : (Π x : A. B) → α . k (λ x : A. e)

[CPS

-Fun]

Γ ⊢ e : Π x : A. B {

Γ, x : A ⊢ B : κ {

Γ ⊢ e

′

: A {

′

Γ ⊢ A : κ

′

{

Γ ⊢ e e

′

: B[e

′

/x] {

λ α : ∗. λ k : (B

[(e

′

A id)/x]) → α .

e α (λ f : Π x : A. B

′

@ α (λ x : A. (f x) α k))

[CPS

-App]

Γ ⊢ e : A {

e Γ ⊢ A : κ

′

{

A Γ ⊢ B : κ {

B Γ, x = e : A ⊢ e

′

: B {

′

Γ ⊢ let x = e : A in e

′

: B[e/x] {

λ α : ∗. λ k : B[(e A id)/x] → α .

e @ α (λ x : A. e

′

α k)

[CPS

-Let]

Γ ⊢ e

: A {

Γ ⊢ e

: B[e

/x] {

Γ ⊢ A : ∗ {

A Γ, x : A ⊢ B : ∗ {

Γ ⊢ ⟨e

, e

⟩ : Σ x : A. B {

λ α : ∗. λ k : Σ x : A. B → α .

@ α (λ x

: A. e

@ α (λ x

: B[(e

A id)/x].

k ⟨x

, x

⟩ as Σ x : A. B))

[CPS

-Pair]

Γ ⊢ A : ∗ {

A Γ ⊢ e : Σ x : A. B {

Γ ⊢ fst e : A {

λ α : ∗. λ k : A

→ α .

e @ α (λ y : Σ x : A. B. let z = fst y in k z)

[CPS

-Fst]

Γ ⊢ A : ∗ {

Γ, x : A ⊢ B : ∗ {

B Γ ⊢ (fst e) : A {

(fst e)

Γ ⊢ e : Σ x : A. B {

Γ ⊢ snd e : B [fst e/x] {

λ α : ∗. λ k : B[((fst e)

A id)/x] → α .

e @ α (λ y : Σ x : A. B. let z = snd y in k z)

[CPS

-Snd]

Γ ⊢ e : B {

Γ ⊢ e : A {

[CPS

-Conv]

⊢ Γ {

Γ Lemma 6.3 will show ⊢ Γ

⊢ · {

[CPS

-Empty]

⊢ Γ {

Γ Γ ⊢ A : κ {

⊢ Γ, x : A {

Γ, x : A

[CPS

-AssumT]

⊢ Γ {

Γ Γ ⊢ κ : U {

⊢ Γ, α : κ {

Γ, α : κ

[CPS

-AssumK]

⊢ Γ {

Γ Γ ⊢ A : κ {

A Γ ⊢ e : A {

⊢ Γ, x = e : A {

Γ, x = e A id : A

[CPS

-Def]

⊢ Γ {

Γ Γ ⊢ A : κ {

A Γ ⊢ κ : U {

⊢ Γ, α = A : κ {

Γ, α = A : κ

[CPS

-DefT]

Fig. 11. CPS

of Terms and Environments (excerpts)

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:24 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

The type translation (Figure 10) has multiple rules with variable annotations that have changed

from CBN. The computation translation of types is unchanged. In the value translation, similar to

the kind translation, dependent function types that abstract over terms now translate the argument

annotation x : A using the value translation. Dependent pair types Σ

x : A.

B now translate to

pairs of values

Σ x : A

. When terms appear in the type language, such as in [CPS

-AppConstr]

and [CPS

-Let], we must explicitly convert the computation to a value to maintain the invariant

that all term variables refer to term values. Hence in [CPS

-AppConstr] we translate a type-level

application with a term argument A e to A

(

id)

. We similarly translate let-bound terms

[CPS

-Let] by casting the computation to a value. Recall from Section 3 that while expressions of

the form A

(

id)

are not in CPS form, this expression is a type and will be evaluated during

type checking. Terms that evaluate at run time are always in proper CPS form and do not return.

The term translation (Figure 11) changes in three major ways. As in Section 5, we implicitly

have a computation and a value translation on term values, with the latter inlined into the former.

First, unlike in CPS

, variables are values, whereas the translation must produce a computation.

Therefore, we translate x by “value

-expansion” into

λ α . λ k. k x

, a computation that immediately

applies the continuation to the value. Second, as discussed above, we change the translation of

application [CPS

-App] to force the evaluation of the function argument. Third and nally, in the

translation of pairs [CPS

-Pair], we force the evaluation of the components of the pair and produce

a pair of values for the continuation. Note that in cases of the translation where we have types

with dependency—[CPS

-App], [CPS

-Let], [CPS

-Pair], and [CPS

-Snd]—we cast computations to

values in the types by applying the identity continuation, and require the @ form to use our new

typing rule.

Given the translation of binding constructs in the language, the translation of the environment

(Figure 11)

should be unsurprising. Since all variables are values, we translate term variables x : A

using the value translation on types to produce

: A

instead of

: A

. We must also translate term

denitions x = e : A by casting the computation to a value, producing x = e

id : A

6.1 Proof of Type-Preser vation for CPS

The structure of the type-preservation proof is the same as in Section 5. First we prove that

the translation commutes with substitution, then that reduction sequences are preserved, then

that equivalence is preserved, and nally that typing is preserved. Except for Lemma 6.2 (CPS

Compositionality), the proofs of the supporting lemmas are essentially the same as in Section 5.

We elide these lemmas and their proofs for brevity. For full details, see our online supplementary

materials (Bowman et al. 2017).

We begin with a technical lemma that is essentially an

principle for CPS’d computations. In

the CPS

setting, we must frequently reason about normal forms of CPS’d computations. This

lemma provides a useful abstraction for doing so.

The lemma states that any CPS’d computation

is equivalent to a new CPS’d computation that accepts a continuation

simply applies e

The proof is straightforward. Note the type annotations are mismatched, as in our explanation of

coherence in Section 5.1, but the behaviors of the terms are the same and equivalence is untyped.

Lemma 6.1 (CPS

Computation η). e

≡ λ α : ∗. λ k : A → α . e

@ α (λ x : B. k x)

Since variables are values in call-by-value, we adjust the statement of Lemma 6.2 to cast compu-

tations to values. Proving this lemma now requires our new equivalence rule [

≡

-Cont] for cases

involving substitution of terms. By convention, all terms being translated have an implicit typing

derivation, so the omitted types are easy to reconstruct.

The proofs for the CBN setting only require a specialized instance of this property although the general form holds.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:25

Lemma 6.2 (CPS

Compositionality).

(1) (κ[A/α])

≡ κ

/α ]

(2) (κ[e/x])

≡ κ

_ id/x]

(3) (A[B/α])

≡ A

/α ]

(4) (A[e/x])

≡ A

_ id/x]

(5) (A[B/α])

≡ A

/α ]

(6) (A[e/x])

≡ A

_ id/x]

(7) (e[A/α])

≡ e

/α ]

(8) (e[e

′

/x])

≡ e

′÷

_ id/x]

Proof.

The proof is straightforward by induction on the typing derivation of the expression t

being substituted into. We give one representative case.

Case [Var] Part 8, (x[e/x

′

])

We must show (x[e/x

′

])

= x

_ id/x

′

W.l.o.g., assume x = x

′

(x[e/x])

(17)

= e

by denition of substitution (18)

≡ λ α . λ k. (e

@ α λ x. k x) by Lemma 6.1 (19)

≡ λ α . λ k. (λ x. k x) (e

_ id) by [≡-Cont] (20)

= (λ α . λ k. (λ x. k x) x)[(e

_ id)/x] by substitution (21)

≡ (λ α . λ k. k x)[(e

_ id)/x] by ▷

(22)

= x

[(e

_ id)/x] by denition of translation (23)

□

Lemma 6.3 (CPS

is Type Preserving (Explicit Syntax)).

(1) If ⊢ Γ then ⊢ Γ

(2) If Γ ⊢ e : A then Γ

⊢ e

: A

(3) If Γ ⊢ A : κ then Γ

⊢ A

: κ

(4) If Γ ⊢ A : ∗ then Γ

⊢ A

: ∗

(5) If Γ ⊢ κ : U then Γ

⊢ κ

: U

Proof.

All cases are proven simultaneously by mutual induction on the typing derivation and

well-formedness derivation. Part 4 follows easily by part 3 in every case, so we elide its proof. Most

cases follow easily from the induction hypotheses.

Case [W-Def] ⊢ Γ, x = e : A

We give the case for when A is a type; the case when A is a kind is similar.

We must show ⊢ Γ

, x = e

id : A

It suces to show that Γ

⊢ e

id : A

By part 2 of the induction hypothesis and denition of the translation, we know that

⊢ e

: Π α : ∗. (A

→ α ) → α , easily which implies the goal.

Case [Var] Γ ⊢ x : A

We give the case for when A is a type; the case when A is a kind is simple since the

translation on type variables is the identity.

We must show that Γ

⊢ λ α : ∗. λ k : A

→ α . k x : A

By the part 1 of the induction hypothesis, we know Γ

⊢ x : A

, which implies the goal.

Case [App] Γ ⊢ e

: B[e

/x].

We must show that

⊢ λ α : ∗. λ k : (B

[(e

id)/x]) → α .

α (λ f : Π x : A

. B

. e

@ α (λ x : A

. (f x) α k))

: (B[e

/x])

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:26 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Note that,

(B[e

/x]) (24)

≡ B

id/x] by Lemma 6.2 (25)

≡ Π α : ∗. ((B

id/x]) → α ) → α by translation (26)

Hence it suces to show that

, α

∗, k

[(e

id)/x]) → α ⊢

α (λ f : Π x : A

. B

. e

@ α (λ x : A

. (f x) α k)) : α

By part 2 of the induction hypothesis, we know that Γ

⊢

: Π α : ∗. ((Π x : A

) → α ) →α

hence it suces to show that

, α : ∗, k : (B

[(e

id)/x]) → α , f : Π x : A

. B

⊢ e

@ α (λ x : A

. (f x) α k) : α

By [T-Cont], we must show

, α : ∗, k : (B

[(e

id)/x]) → α , f : Π x : A

. B

, x = e

id, ⊢ (f x) α k : α

Note that f x : B

[x/x] and B

[x/x] = Π α : ∗. (B

[x/x]) → α → α .

But k : (B

[(e

id)/x]) → α .

Hence it suces to show that

[x/x]) ≡ (B

[(e

id)/x])

, which follows by

reduction

on x since we have x = e

id by our new typing rule [T-Cont].

Note that without our new typing rule, we would be here stuck. However, thanks to

[T-Cont], we have the equality that

x =

, and we are able to complete the proof.

□

Theorem 6.1 (CPS

is Type Preserving (PTS syntax)). If Γ ⊢ e : A then Γ

⊢ cps

: cpsT

6.2 Proof of Correctness for CPS

To prove correctness of separate compilation for CPS

, we follow the same recipe as in Section 5.2.

We use the same cross-language relation

≈

on values of ground type. However, note that in CBV

we should only link with values, so we restrict closing substitutions

to values and use the value

translation on substitutions γ

. The proofs follow exactly the same structure as in Section 5.2.

Theorem 6.2 (Separate Compilation Correctness). If Γ

⊢

A where A is ground, and

γ (

) ▷

⋆

then γ

) A

id ▷

⋆

v and v ≈ v.

Corollary 6.1 (Whole-Program Compiler Correctness). If

⊢

A and e

▷

⋆

v then e

id ▷

⋆

v and v ≈ v.

7 DISCUSSION AND FUTURE WORK

Dependent Sums. In addition to showing that the traditional double-negation CPS for

types is

not type preserving, Barthe and Uustalu (2002) demonstrate an impossibility result for CPS and

sums with dependent case analysis. They prove that no type-correct CPS translation can exist for

sums with dependent case. However, careful inspection of their proof reveals that this impossibility

result does not apply to our CPS translation. Furthermore, we can dene a CPS translation for

dependent case that appears to be type preserving, although we do not give a formal proof.

The impossibility result by Barthe and Uustalu (2002) relies on the ability to implement

call/cc

via the CPS translation. Assuming there is a type-preserving CPS translation, they construct a

model of CC extended with

call/cc

and sum types (CC

∆+

) in CC with sum types (CC+). Since

CC+ is consistent, this model proves that CC

∆+

is consistent. However, it is known that CC

∆+

inconsistent (Coquand 1989). Therefore, the type-preserving CPS translation of CC

∆

+ cannot exist.

Their proof is valid; however, it is well known that the polymorphic answer type CPS translation

that we use cannot implement

call/cc

(Ahmed and Blume 2011). Therefore, our translation does

not give a model of CC∆+ in CC+.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:27

We go further and conjecture a positive result, that our CPS translation is type preserving for

dependent case. The typing rule for dependent case is the following.

Γ, y : A + B ⊢ A

′

: ∗ Γ, x : A ⊢ e

: A

′

[inj

x/y] Γ, x : B ⊢ e

: A

′

[inj

x/y]

Γ ⊢ case e of x. e

| x. e

: A

′

[e/y]

We would extend our CPS

with the following rule.

(case e of x. e

| x. e

)

= λ α : ∗. λ k : A

′+

/y] → α .

@ α (λ y : A

+ B

. case y of x. (e

α k) | x. (e

α k))

Focusing on the rst branch of the

case

above, note that e

′+

[(inj

/y]→α ) →α

, however

′+

/y] → α

. We need to show that e

≡ (inj

)

, similar to the problem with the second

projection of dependent pairs. This time, however, to show e

≡ (inj

)

we need to reason about

the ow of the underlying value of e

into

and also about the relationship between

and

Specically, we need to rst use our new [T-Cont] rule, which allows us to assume

y =

α id

. Next,

we need to know that since the case analysis is on the value

, in the rst branch

y ≡ inj

(and

similarly for the other branch), but the problem is that our existing typing rule for dependent case

does not let us assume that. Nonetheless, past work on dependent elimination in Agda suggests that

we can modify the typing rule for dependent case to have the equality e

≡ inj

x while typing the

rst branch, and similarly for the second branch (Cockx et al

2016). With this additional equality

in hand, some simple computation with the translation of

(inj

)

gives us the desired equivalence.

Hence, with the aforementioned modication to the typing rule for dependent case in our target

language CC

, we can type check the above translation of dependent case. The part of the proof

that we have not yet carried out is showing the consistency of our target language CC

once it is

extended with this modied typing rule for dependent case.

The Calculus of Inductive Constructions. We haven’t yet completed the above proof for sums with

dependent elimination because ultimately we want to extend our translation to the Calculus of

Inductive Constructions (CIC). Inductive types have a similar structure to sums with dependent

case, but much more involved typing rules. We believe that the sketch presented for dependent

case on sums extends to general inductive types and intend to extend our translation in the future.

However, CIC presents several other challenges.

The rst is to handle the innite hierarchy of universes. In this work, we have a single impredica-

tive universe

∗

, and the locally polymorphic answer type

lives in that universe. With an innite

hierarchy, it is not clear what the universe of

should be. Furthermore, our work relies on impred-

icativity in

∗

. We can only use impredicativity at one universe level and the locally polymorphic

answer-type translation has not been studied in the context of predicative polymorphism, so it’s

unclear how to adapt our translation to the innite predicative hierarchy.

The right solution for handling universes seems to be universe polymorphism (Sozeau and

Tabareau 2014). Since the type is provided by the calling context, it seems sensible that the calling

context should also provide the universe. We could modify the type translation to be

Π ℓ : Level. Π α :

Type

ℓ

. (

→ α ) → α

. However, it is not clear how universe polymorphism would aect the rest of

the CPS translation.

Finally, CIC also features guarded recursive functions. As the guard condition is purely syntactic,

it seems likely to be disrupted by CPS translation. We either need to compile the guard condition to

something more semantic, like sized types, before the CPS translation, or adapt the guard condition

to the new CPS syntax.

CPS vs ANF. ANF (Flanagan et al

1993), which is based on a structured use of

let

, is a popular

alternative to CPS for compiler intermediate languages. It is natural to wonder whether ANF would

be easier than CPS in CC, especially given the complexity of CPS in CC and the fact that our proof

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:28 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

of consistency performs a translation similar to the inverse CPS translation of Flanagan et al

(1993).

We conjecture that, while the ANF translation on its own may be simpler owing to the additional

expressivity

let

, using ANF in practice will not be signicantly simpler than using our CPS

translation. Kennedy (2007) points out that ANF is not preserved under

-reduction, and that ANF

in the presence of conditional expressions can result in considerable code duplication; neither

problem arises in CPS. Recently, Maurer et al

(2017) formalize a notion of join-points to solve the

latter problem, observing that this simplies certain optimizations that are dicult in CPS. We may

be able to adapt this work to the dependently typed setting, but we conjecture that formalizing

dependent join-points will require an analog of [≡-Cont], and ANF will complicate β-reduction.

Implementing call/cc, or Predicative or Non-parametric Models. Our work relies on parametricity

to recover type preservation, but avoiding parametricity has certain benets, such as the ability to

implement restricted forms of

call/cc

, or using predicative or non-parametric models of dependent

type theory. We use parametricity as a type-based mechanism to enforce a condition known as

naturality—i.e., the equivalence given by [

≡

-Cont]—but naturality can be dened in non-parametric

or even untyped settings. For instance, Thielecke (2003) gives a denition of naturality in terms of

a delimited continuations: a term

is natural if

M ≡

(where % is the continuation delimiter

prompt

). Using parametricity to enforce naturality limits the scope of our CPS translation. We cannot

use our translation to implement

call/cc

. This restriction is unnecessary in principle—restricted

uses of

call/cc

are consistent with dependent type theory (Herbelin 2012). Our translation requires

impredicativity and parametricity in the target language type theory, and these two features are

not always admitted in type theory. For instance, Agda is predicative, and Boulier et al

(2017) give

some non-parametric models of type theory. Thielecke (2003) studies how to recover properties like

naturality in the presence of

call/cc

using a source language with type-and-eect system, although

using a CPS translation based on answer-type polymorphism. As future work, investigating how

to extend that work to dependent type theory may let us broaden the scope of our CPS translation.

Weak Normalization Implies Strong Normalization. In this paper, we only CPS translate terms,

i.e., run-time expressions. However, other work (Barthe et al

2001) studies pervasive translation of

PTSs. A pervasive CPS translation internalizes evaluation order for all expressions: terms, types,

and kinds. A pervasive CPS translation has been used to give a partial solution to the Barendregt-

Geuvers-Klop conjecture (Geuvers 1993) which essentially states that every weakly normalizing

PTS is also strongly normalizing. The conjecture has been solved for non-dependent PTSs, but

the solution for dependent PTSs remains open. As future work, we intend to extend our work

to a pervasive translation. This may allow us to make progress on the Barendregt-Geuvers-Klop

conjecture. However, as our translation requires additional axioms, it’s not clear to what class of

dependent PTSs the result might apply.

8 RELATED WORK

Type-Preserving Compilation of Dependent Types. The challenges of extending CPS translations

to dependently typed languages were rst pointed out by Barthe et al

(1999). As discussed in

Section 5.1, a diculty arises when working in the domain-full lambda calculus with a typed

equivalence: we cannot stage the proofs of compositionality, coherence, and type preservation.

Barthe et al. solve this problem using domain-free lambda abstractions, and successfully dene

a type-preserving call-by-name CPS translation for CC (without

types). Unfortunately, type

Unfortunately, we lack a formal system for discussing the relative expressiveness of type features along the same lines as

macro expressibility used to discuss expressiveness of runtime features (Felleisen 1991). We therefore appeal to the reader’s

intuition.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:29

checking becomes undecidable in the domain-free calculus. We avoid the circularity by using an

untyped equivalence, which allows us to use a domain-full calculus, eliminating one source of

undecidability. Recall from Section 4.1 that since we provide a model of our target language CC

the extensional CC, we do not yet have a proof that type checking in CC

is decidable.

Other approaches to type-preserving compilation for dependent types avoid the diculties

we’ve seen with CPS by avoiding full spectrum dependent types, i.e.,

and

with no explicit

distinctions between terms and types. (Full spectrum dependent types support code reuse across

terms and types, and avoid the need for programmers to marshall between dierent term and type

representations.) Shao et al

(2005) develop type-preserving CPS and closure-conversion passes for

a language that uses CIC as an extrinsic type system, for use in developing certied binaries. In

their language, types cannot depend on run-time expressions. Instead, certain expressions have

a second, type-level representation, and CIC specications and proofs can be written for these

type-level representations. One motivation for this design was exactly the problem with CPS we

have solved. Chen et al

(2010) develop a type-preserving compiler from Fine, an ML-like language

with renement types instead of full spectrum dependent types, to DCIL, a typed variant of the

.NET Common Intermediate Language with type-level computation. The type system in DCIL was

used to encode security and verication conditions, also supporting certied binaries.

Control Operators and Dep endent Types. There is a line of work combining dependent types

and control operators. Herbelin (2005) shows that unrestricted use of

call/cc

and

throw

in a

language with

types and equality leads to an inconsistent system. The inconsistency is caused

by type dependency on terms involving control eects. Herbelin (2012) solves the inconsistency

by constraining types to depend only on negative-elimination-free (NEF) terms, which are free of

eects. This restriction makes dependent types compatible with classical reasoning enabled by the

control operators. Our CPS translation doesn’t allow implementing control operators, but this line

of work leads us to suspect that there exists a less restricted translation that preserves typing.

Recent work by Miquey (2017) uses the NEF restriction to soundly extend the

λµ

-calculus

of Curien and Herbelin (2000), a computational classic calculus, with dependent types. He then

extends the language with delimited continuations, and denes a type-preserving CPS to a standard

intuitionistic dependent type theory. By comparison, our source language CC is eect-free, therefore

we do not need the NEF condition to restrict dependency. Our use of the identity function serves a

similar role to their delimited continuations—allowing local evaluation of a CPS’d computation.

Miquey (2017) makes an interesting observation that certain evaluation contexts in dependently

typed languages are not well typed, and we conjecture that our work oers a solution. As the

λµ

-calculus has explicit evaluation contexts in the syntax, he observes that subject reduction

fails, and calls this “desynchronization of typing with respect to the execution.” We can see this

problem in CC evaluation contexts as well, although evaluation contexts are purely meta-theoretic

features and do not exist in the syntax of CC. Consider a well-typed CBN context representing a

function application,

E e

(Γ

′

⊢ A

′

) ⇒ (Γ ⊢ B[e/x])

, which says that when we plug a term of type

′

into the hole of

, this context yields a term of type

B[e/x]

. In general, contexts can capture

variables, so we include in the type the environment

′

of the hole and remaining free variables

after plugging a term. This works for a CBN application context, but in CBV we have an additional

evaluation context for application,

v E

, which evaluates the argument. The type of

v E

now depends

on the context

, not on a term, so it is not clear how to proceed:

v E

(Γ

′

⊢ A

′

) ⇒ (Γ ⊢ B[???/x])

. In

both CBN and CBV, the same problem arises in the evaluation context for the second projection:

snd E

(Γ

′

⊢ A

′

) ⇒ (Γ ⊢ B[fst ???/x])

. As our CPS translation produces well-typed continuations from

these apparently ill-typed contexts, it should be possible to design a source syntax for well-typed

CC evaluation contexts that is realized by our translation.

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:30 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Eects and Dependent Types. Pédrot and Tabareau (2017) dene the weaning translation, a monadic

translation for adding eects to dependent type theory. The weaning translation allows us to

represent self-algebraic monads, i.e., monads whose algebras’ universe itself forms an algebra, such

as exception and non-determinism monads. However, it does not apply to the standard continuation

monad, which is not self-algebraic. The paper extends the translation to inductive types, with a

restricted form of dependent elimination. Full dependent elimination can be implemented only

for terms whose type is rst-order, and this comes at the cost of inconsistency, although one can

recover consistency by requiring that every inductive term be parametric. Our translation does

not lead to inconsistency, and requires no restrictions on the type to be translated. However, our

translation appears to impose the self-algebraic structure on our computation types, and our use of

parametricity to cast computations to values is similar to their parametricity restriction.

Multi-language Semantics. A full spectrum dependently typed language resembles a multi-

language system (Matthews and Findler 2007) between a (compile time) type language and a

(run time) term language. In CC, the two languages happen to be the same, but the distinction

between them is made clear via CPS. We recover type preservation for CPS translations by dening

interoperability between the CPS’d terms and the direct-style types. To dene interoperability,

we allow types to run a CPS’d term to a value by supplying the halt, or identity, continuation.

This is exactly the interoperability semantics dened by Ahmed and Blume (2011) between a CPS

and direct-style language. Their work also makes use of answer-type polymorphism to enforce

naturality. A similar strategy appears in the multi-language semantics given by Patterson et al

(2017) for interoperability between a direct-style functional language and a continuation-based

assembly language. Their work does not use answer-type polymorphism, but enforces naturality

by augmenting the type system to track return addresses and adding a special halt instruction to

interpret assembly components as values.

Applications of the Polymorphic Answer Type. The polymorphic answer type has proven useful in

other work on CPS translations as well. Thielecke (2003) studies the connection between control

eects and answer-type polymorphism in a call-by-value language with

call/cc

. He denes an

eect system that tells us whether we can regard a term as a pure term. Then he shows pure terms

use their continuation linearly, and that their answer type is polymorphic. Using the latter property,

he proves that enclosing a pure term with a control delimiter does not aect its meaning, i.e.,

naturality. Thielecke (2004) extends this study to the call-by-name setting, showing that answer-

type polymorphism holds not only for pure functions, but also for eectful functions.

Ahmed and Blume (2011) give a full-abstraction proof of a call-by-value CPS translation that uses

polymorphic answer types. Full abstraction is an important property for secure compilation, which

ensures that a translation converts two terms that are indistinguishable in any source context into

two terms that are indistinguishable in any target context. Their proof relies on exactly the free

theorem we proved in Section 4.1. We conjecture therefore that our CPS translation is fully abstract.

Internalizing Parametricity. Our work internalizes a specic free theorem, but ongoing work

focuses on how to internalize parametricity more generally in a dependent type theory. Krish-

naswami and Dreyer (2013) develop a technique for adding new rules to the extensional CC. They

present a logical relation for terms that are not syntactically well typed, but are semantically well

behaved and equivalent at a particular type. Using this logical relation, they prove the consistency

of several extensions to extensional CC, including sum types, dependent records, and natural

numbers. Bernardy et al

(2012); Keller and Lasson (2012) give translations from one dependent type

theory into another that yield a parametric model of the original theory. These essentially encode

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:31

the logical relation in the target type theory, similar to the approach we took in Section 4.1 (Consis-

tency of CC

). Recent work by Nuyts et al

(2017) develops a theory that internalizes parametricity,

including the important concept of identity extension, and gives a thorough comparison of the

literature. By building a target language based on one of these systems, it’s possible that we could

eliminate the rule [≡-Cont] as an axiom and instead derive it internally.

Veried Compilation. CertiCoq is a mechanically veried optimizing compiler currently under

development (Anand et al

2017). It compiles Coq’s Gallina to CompCert’s Clight. As mentioned

in Section 1, CertiCoq is not a type-preserving compiler: it erases types before CPS conversion,

optimizations, and closure conversion. CertiCoq’s current compiler correctness theorem aims to

prove separate compilation correctness. We have proved similar separate-compilation correctness

theorems, Theorem 5.2 and Theorem 6.2, but our typed target language can statically enforce

these guarantees via type checking. Our theorems dier in a few key aspects. First, we only show

correctness for the CPS translation of CC. Second, our relation on ground terms is impoverished;

we only prove that booleans are related, while CertiCoq has an abstract relation that is preserved

on all ground types. Finally, our long-term goals are dierent from CertiCoq’s current goal of

correct separate compilation. We are interested in type-preserving compilation of Coq as a means

of supporting correct and secure (fully abstract) compilation even when the compiled code is

linked with code compiled from dierent, possibly eectful, languages. By picking the right type

translation for each phase of the compiler, we wish to use the target-level type specication to—

statically, or dynamically via gradual typing—rule out unsafe or insecure interactions with target

code. In our CPS translation, the polymorphic answer type does the work to rule out interaction

with computations that have control eects. Therefore, even if we could encode

call/cc

in the target

language (which is type safe when restricted to Herbelin’s negative-elimination-free fragment), it

would not interoperate with the output of our compiler.

ACKNOWLEDGMENTS

We gratefully acknowledge the valuable feedback provided by Greg Morrisett, Karl Crary, and the

anonymous reviewers. Part of this work was done at Inria Paris in Fall 2017, while Amal Ahmed

was a Visiting Professor and William J. Bowman held an internship.

This material is based upon work supported by the National Science Foundation under grants

CCF-1422133 and CCF-1453796, and a Northeastern University Scholars’ Independent Research

Fellowship. Any opinions, ndings, and conclusions or recommendations expressed in this material

are those of the authors and do not necessarily reect the views of the National Science Foundation.

REFERENCES

Martín Abadi. 1998. Protection in Programming-language Translations. In International Colloquium on Automata, Languages,

and Programming. DOI:http://dx.doi.org/10.1007/bfb0055109

Amal Ahmed. 2015. Veried Compilers for a Multi-Language World. In 1st Summit on Advances in Programming Languages

(SNAPL 2015). DOI:http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.15

Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International

Conference on Functional Programming (ICFP). DOI:http://dx.doi.org/10.1145/1411203.1411227

Amal Ahmed and Matthias Blume. 2011. An Equivalence-preserving CPS Translation Via Multi-language Semantics. In

International Conference on Functional Programming (ICFP). DOI:http://dx.doi.org/10.1145/2034773.2034830

Abhishek Anand, A. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Bélanger, Matthieu Sozeau,

and Matthew Weaver. 2017. CertiCoq: A Veried Compiler for Coq. In The International Workshop on Coq for Programming

Languages (CoqPL). http://www.cs.princeton.edu/~appel/papers/certicoq-coqpl.pdf

Andrew W. Appel. 2015. Verication of a Cryptographic Primitive: SHA-256. ACM Transactions on Programming Languages

and Systems 37, 2 (April 2015). DOI:http://dx.doi.org/10.1145/2701415

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

22:32 William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-béguelin. 2009. Formal Certication of Code-based Cryptographic

Proofs. In Symposium on Principles of Programming Languages (POPL). DOI:http://dx.doi.org/10.1145/1480881.1480894

Gilles Barthe, John Hatcli, and Morten Heine Sørensen. 2001. Weak Normalization Implies Strong Normalization in a

Class of Non-dependent Pure Type Systems. Theoretical Computer Science 269, 1-2 (Oct. 2001).

DOI:

http://dx.doi.org/10.

1016/s0304-3975(01)00012-3

Gilles Barthe, John Hatcli, and Morten Heine B. Sørensen. 1999. CPS Translations and Applications: The Cube and Beyond.

Higher-Order and Symbolic Computation 12, 2 (Sept. 1999). DOI:http://dx.doi.org/10.1023/a:1010000206149

Gilles Barthe and Tarmo Uustalu. 2002. CPS Translating Inductive and Coinductive Types. In Workshop on Partial Evaluation

and Semantics-based Program Manipulation (PEPM). DOI:http://dx.doi.org/10.1145/509799.503043

Jean-philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for Free: Parametricity for Dependent Types.

Journal of Functional Programming 22, 02 (March 2012). DOI:http://dx.doi.org/10.1017/S0956796812000056

Simon Boulier, Pierre-marie Pédrot, and Nicolas Tabareau. 2017. The Next 700 Syntactical Models of Type Theory. In

Conference on Certied Programs and Proofs (CPP). DOI:http://dx.doi.org/10.1145/3018610.3018620

William J. Bowman and Amal Ahmed. 2015. Noninterference for Free. In International Conference on Functional Programming

(ICFP). DOI:http://dx.doi.org/10.1145/2784731.2784733

William J. Bowman, Youyou Cong, Nick Rioux, and Amal Ahmed. 2017. Type-Preserving CPS Translation of

and

Types

Is Not Not Possible (Supplementary Materials. (Oct. 2017). https://williamjbowman.com/resources/cps-sigma.tar.gz

Juan Chen, Ravi Chugh, and Nikhil Swamy. 2010. Type-preserving Compilation of End-to-end Verication of Security

Enforcement. In International Conference on Programming Language Design and Implementation (PLDI).

DOI:

http:

//dx.doi.org/10.1145/1806596.1806643

Jesper Cockx, Dominique Devriese, and Frank Piessens. 2016. Uniers As Equivalences: Proof-relevant Unication of

Dependently Typed Data. In International Conference on Functional Programming (ICFP).

DOI:

http://dx.doi.org/10.1145/

2951913.2951917

Thierry Coquand. 1986. An Analysis of Girard’s Paradox. In Symposium on Logic in Computer Science (LICS). https:

//hal.inria.fr/inria-00076023

Thierry Coquand. 1989. Metamathematical Investigations of a Calculus of Constructions. Ph.D. Dissertation. INRIA. https:

//hal.inria.fr/inria-00075471

Pierre-louis Curien and Hugo Herbelin. 2000. The Duality of Computation. In International Conference on Functional

Programming (ICFP). DOI:http://dx.doi.org/10.1145/357766.351262

Matthias Felleisen. 1991. On the Expressive Power of Programming Languages. Science of Computer Programming 17, 1-3

(Dec. 1991). DOI:http://dx.doi.org/10.1016/0167-6423(91)90036-W

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling with Continuations.

In International Conference on Programming Language Design and Implementation (PLDI).

DOI:

http://dx.doi.org/10.1145/

155090.155113

Cedric Fournet, Nikhil Swamy, Juan Chen, Pierre-evariste Dagand, Pierre-yves Strub, and Benjamin Livshits. 2013. Fully

Abstract Compilation to JavaScript. In Symposium on Principles of Programming Languages (POPL).

DOI:

http://dx.doi.

org/10.1145/2480359.2429114

Jan Herman Geuvers. 1993. Logics and Type Systems. Ph.D. Dissertation. University of Nijmegen. http://www.ru.nl/publish/

pages/682191/geuvers_jh.pdf

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (newman) Wu, Shu-chun Weng, Haozhong

Zhang, and Yu Guo. 2015. Deep Specications and Certied Abstraction Layers. In Symposium on Principles of Programming

Languages (POPL). DOI:http://dx.doi.org/10.1145/2775051.2676975

Hugo Herbelin. 2005. On the Degeneracy of

-Types in Presence of Computational Classical Logic. In International

Conference on Typed Lambda Calculi and Applications. DOI:http://dx.doi.org/10.1007/11417170_16

Hugo Herbelin. 2012. A Constructive Proof of Dependent Choice, Compatible with Classical Logic. In Symposium on Logic

in Computer Science (LICS). DOI:http://dx.doi.org/10.1109/lics.2012.47

James G. Hook and Douglas J. Howe. 1986. Impredicative Strong Existential Equivalent to Type:type. Technical Report.

Cornell University. http://hdl.handle.net/1813/6600

Jeehoon Kang, Yoonseung Kim, Chung-kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight Verication of

Separate Compilation. In Symposium on Principles of Programming Languages (POPL).

DOI:

http://dx.doi.org/10.1145/

2837614.2837642

Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In International Workshop on Computer

Science Logic (CSL). https://hal.inria.fr/hal-00730913

Andrew Kennedy. 2006. Securing the .NET Programming Model. Theoretical Computer Science 364, 3 (Nov. 2006).

DOI:

http://dx.doi.org/10.1016/j.tcs.2006.08.014

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.

Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible 22:33

Andrew Kennedy. 2007. Compiling with Continuations, Continued. In International Conference on Functional Programming

(ICFP). DOI:http://dx.doi.org/10.1145/1291220.1291179

Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of

Constructions. In International Workshop on Computer Science Logic (CSL).

DOI:

http://dx.doi.org/10.4230/LIPIcs.CSL.

2013.432

Xavier Leroy. 2006. Formal Certication of a Compiler Back-end or: Programming a Compiler with a Proof Assistant. In

Symposium on Principles of Programming Languages (POPL). DOI:http://dx.doi.org/10.1145/1111037.1111042

Xavier Leroy. 2009. A Formally Veried Compiler Back-end. Journal of Automated Reasoning 43, 4 (Nov. 2009).

DOI:

http://dx.doi.org/10.1007/s10817-009-9155-4

Jacob Matthews and Robert Bruce Findler. 2007. Operational semantics for multi-language programs. In Symposium on

Principles of Programming Languages (POPL). DOI:http://dx.doi.org/10.1145/1190216.1190220

Luke Maurer, Paul Downen, Zena M. Ariola, and Simon L. Peyton Jones. 2017. Compiling without Continuations. In

International Conference on Programming Language Design and Implementation (PLDI).

DOI:

http://dx.doi.org/10.1145/

3062341.3062380

Étienne Miquey. 2017. A Classical Sequent Calculus with Dependent Types. In European Symposium on Programming (ESOP).

DOI:http://dx.doi.org/10.1007/978-3-662-54434-1_29

Georg Neis, Chung-kil Hur, Jan-oliver Kaiser, Craig Mclaughlin, Derek Dreyer, and Viktor Vafeiadis. 2015. Pilsner: A

Compositionally Veried Compiler for a Higher-order Imperative Language. In International Conference on Functional

Programming (ICFP). DOI:http://dx.doi.org/10.1145/2784731.2784764

Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully Abstract Compilation Via Universal Embedding. In

International Conference on Functional Programming (ICFP). DOI:http://dx.doi.org/10.1145/2951913.2951941

Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. 2017. Parametric Quantiers for Dependent Type Theory.

Proceedings of the ACM on Programming Languages 1, ICFP (Aug. 2017). DOI:http://dx.doi.org/10.1145/3110276

Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. 2015. Secure Compilation to

Protected Module Architectures. ACM Transactions on Programming Languages and Systems 37, 2, Article 6 (April 2015).

DOI:http://dx.doi.org/10.1145/2699503

Daniel Patterson and Amal Ahmed. 2017. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In

2nd Summit on Advances in Programming Languages (SNAPL 2017).

DOI:

http://dx.doi.org/10.4230/LIPIcs.SNAPL.2017.12

Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. 2017. FunTAL: Reasonably Mixing a Functional

Language with Assembly. In International Conference on Programming Language Design and Implementation (PLDI).

http://www.ccs.neu.edu/home/amal/papers/funtal.pdf

Pierre-marie Pédrot and Nicolas Tabareau. 2017. An Eectful Way to Eliminate Addiction to Dependence. In Symposium on

Logic in Computer Science (LICS). DOI:http://dx.doi.org/10.1109/lics.2017.8005113

James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In European

Symposium on Programming (ESOP). DOI:http://dx.doi.org/10.1007/978-3-642-54833-8_8

Zhong Shao, Valery Trifonov, Bratin Saha, and Nikolaos Papaspyrou. 2005. A Type System for Certied Binaries. ACM

Transactions on Programming Languages and Systems 27, 1 (Jan. 2005). DOI:http://dx.doi.org/10.1145/1053468.1053469

Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In International Conference on Interactive

Theorem Proving (ITP). DOI:http://dx.doi.org/10.1007/978-3-319-08970-6_32

The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. (Oct. 2017). https://coq.inria.fr/doc/

Reference-Manual006.html

Hayo Thielecke. 2003. From Control Eects to Typed Continuation Passing. In Symposium on Principles of Programming

Languages (POPL). DOI:http://dx.doi.org/10.1145/604131.604144

Hayo Thielecke. 2004. Answer Type Polymorphism in Call-by-name Continuation Passing. In European Symposium on

Programming (ESOP). DOI:http://dx.doi.org/10.1007/978-3-540-24725-8_20

Proc. ACM Program. Lang., Vol. 2, No. POPL, Article 22. Publication date: January 2018.