A Type System for Certified Binaries
ZHONG SHAO and VALERY TRIFONOVYale University
BRATIN SAHAIntel Corporation
and
NIKOLAOS PAPASPYROUNational Technical University of Athens
A certified binary is a value together with a proof that the value satisfies a given specification.
Existing compilers that generate certified code have focused on simple memory and control-flow
safety rather than more advanced properties. In this paper, we present a general framework for
explicitly representing complex propositions and proofs in typed intermediate and assembly languages. The new framework allows us to reason about certified programs that involve effects
while still maintaining decidable typechecking. We show how to integrate an entire proof system (the calculus of inductive constructions) into a compiler intermediate language and how theintermediate language can undergo complex transformations (CPS and closure conversion) while
preserving proofs represented in the type system. Our work provides a foundation for the process
of automatically generating certified binaries in a type-theoretic framework.
Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying andVerifying and Reasoning about Programs—mechanical verification; F.3.3 [Logics and Meanings
of Programs]: Studies of Program Constructs—type structure
General Terms: Languages, Verification
Additional Key Words and Phrases: Certified code, proof-preserving compilation, typed intermediate languages

A preliminary version of this paper appeared in the Proceedings of the 29th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL’02).
This work was supported in part by DARPA OASIS grant F30602-99-1-0519, NSF grant CCR9901011, NSF ITR grant CCR-0081590, and NSF grant CCR-0208618. Any opinions, findings,
and conclusions contained in this document are those of the authors and do not reflect the viewsof these agencies.
Authors’ addresses: Zhong Shao and Valery Trifonov, Department of Computer Science, Yale
University, P.O. Box 208285, New Haven, CT 06520; email: {shao, trifonov}@cs.yale.edu;
Bratin Saha, Microprocessor Technology Lab, Intel Corporation, Santa Clara, CA 95054; email:bratin.saha@intel.com; Nikolaos Papaspyrou, National Technical University of Athens, Department of Electrical and Computer Engineering, Software Engineering Laboratory, 15780 Zografou,
Athens, Greece; email: nickie@softlab.ntua.gr.
Permission to make digital/hard copy of all or part of this material without fee for personal orclassroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice
is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on
servers, or to redistribute to lists requires prior specific permission and/or a fee.
c 2004 ACM . . .

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year, Pages 1–46.

2·

Z. Shao et al.

1. INTRODUCTION
Proof-carrying code (PCC), as pioneered by Necula and Lee [1996] [Necula1997], allows a code producer to provide a machine-language program to ahost, along with a formal proof of its safety. The proof can be mechanicallychecked by the host; the producer need not be trusted because a valid proof isincontrovertible evidence of safety.
The PCC framework is general because it can be applied to certify arbitrary
data objects with complex specifications [Necula 1998; Appel and Felten 2001].
For example, the Foundational PCC system [Appel and Felty 2000] can certify
any property expressible in Church’s higher-order logic. Harper [2000] andBurstall and McKinna [1991] call all these proof-carrying constructs certified
binaries (or deliverables). A certified binary is a value (which can be a function,
a data structure, or a combination of both) together with a proof that the value
satisfies a given specification.
Unfortunately, little is known on how to construct or generate certified binaries. Most existing certifying compilers [Necula and Lee 1998; Colby et al.
2000] have focused on simple memory and control-flow safety only. Typed intermediate languages [Harper and Morrisett 1995] and typed assembly languages [Morrisett et al. 1998] are effective techniques for automatically generating certified code; however, none of these type systems can rival the expressiveness of the actual higher-order predicate logic (which could be used in any
Foundational PCC system).
In this paper, we present a type-theoretic framework for constructing, composing, and reasoning about certified binaries. Our plan is to use the formulaeas-types principle [Howard 1980] to represent propositions and proofs in a
general type system, and then to investigate their relationship with compiler
intermediate and assembly languages. We show how to integrate an entire
proof system (the calculus of inductive constructions [Paulin-Mohring 1993;
Coquand and Huet 1988]) into an intermediate language, and how to definecomplex transformations (CPS and closure conversion) of programs in this language so that they preserve proofs represented in the type system. Our paperbuilds upon a large body of previous work in the logic and theorem-proving
community (see [Barendregt and Geuvers 1999; Barendregt 1991] for a goodsummary), and makes the following new contributions:—We show how to design new typed intermediate languages that are capableof representing and manipulating propositions and proofs. In particular, weshow how to maintain decidability of typechecking when reasoning aboutcertified programs that involve effects. This is different from the work donein the logic community which focuses on strongly normalizing (primitive recursive) programs.
—We maintain a phase distinction between compile-time typechecking andrun-time evaluation. This property is often lost in the presence of dependent types (which are necessary for representing proofs in predicate logic).
We achieve this by never having the type language (see Section 3) dependent on the computation language (see Section 4). Proofs are instead always
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

3

represented at the type level using dependent kinds.
—We show how to use propositions to express program invariants and how to
use proofs to serve as static capabilities. Following Xi and Pfenning [1999],
we use singleton types [Hayashi 1991] to support the necessary interaction
between the type and computation languages. We can assign an accurate
type to unchecked vector (or array) access (see Section 4.3). Xi and Pfenning[1999] can achieve the same using constraint checking, but their system does
not support arbitrary propositions and (explicit) proofs, so it is less generalthan ours.
—We use a single type language to typecheck different compiler intermediate
languages. This is crucial because it is impractical to have separate proof
libraries for each intermediate language. We achieve this by using inductive
definitions to define all types used to classify computation terms. This inturn nicely fits our work on (fully reflexive) intensional type analysis [Trifonov et al. 2000] into a single system.
—We show how to perform CPS and closure conversion on our intermediate
languages while still preserving proofs represented in the type system. Existing algorithms [Morrisett et al. 1998; Harper and Lillibridge 1993; Minamide et al. 1996; Barthe et al. 1999] all require that the transformation
be performed on the entire type language. This is impractical because proofs
are large in size; transforming them can alter their meanings and break thesharing among different languages. We present new techniques that completely solve these problems (Sections 5–6).
—Our type language is a variant of the calculus of inductive constructions ofPaulin-Mohring [1993] and Coquand and Huet [1988]. Following Werner[1994], we give rigorous proofs for its meta-theoretic properties (subject reduction, strong normalization, confluence, and consistency of the underlying logic). We also give the soundness proof for our sample computation
language. See Sections 3–4, the appendix, and the companion technical report [Shao et al. 2001] for details.
As far as we know, our work is the first comprehensive study on how to incorporate higher-order predicate logic (with inductive terms and predicates) into
typed intermediate languages. Our results are significant because they open
up many new exciting possibilities in the area of type-based language designand compilation. The fact that we can internalize a very expressive logic into
our type system means that formal reasoning traditionally done at the meta
level can now be expressed inside the actual language itself. For example,
much of the past work on program verification using Hoare-like logics may
now be captured and made explicit in a typed intermediate language.
From the standpoint of type-based language design, recent work [Harperand Morrisett 1995; Xi and Pfenning 1999; Crary et al. 1999; Walker 2000;
Crary and Weirich 2000; Trifonov et al. 2000] has produced many specialized,
increasingly complex type systems, each with its own meta-theoretical proofs,
yet it is unclear how they will fit together. We can hope to replace them with
one very general type system whose meta theory is proved once and for all, and
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

4·

Z. Shao et al.

that allows the definition of specialized type operators via the general mechanism of inductive definitions. For example, inductive definitions subsume andgeneralize earlier systems for intensional type analysis [Harper and Morrisett
1995; Crary and Weirich 1999; Trifonov et al. 2000].
We have a prototype implementation of our new type system in the FLINT
compiler [Shao 1997; Shao et al. 1998], but making the implementation realistic still involves solving many remaining problems (e.g., efficient proof representations). Nevertheless, we believe our current contributions constitute asignificant step toward the goal of providing a practical end-to-end compiler
that generates certified binaries.
2. APPROACH
Our main objectives are to design typed intermediate and low-level languages
that can directly manipulate propositions and proofs, and then to use them tocertify realistic programs. We want our type system to be simple but general;
we also want to support complex transformations (CPS and closure conversion) that preserve proofs represented in the type system. In this section, we
describe the main challenges involved in achieving these goals and give a highlevel overview of our main techniques.
Before diving into the details, we first establish a few naming conventions
that we will use in the rest of this paper. Typed intermediate languages areusually structured in the same way as typed λ-calculi. Figure 1 gives a fragment of a richly typed λ-calculus, organized into four levels: kind schema(kscm) u, kind κ, type τ , and expression (exp) e. If we ignore kind schema andother extensions, this is just the higher-order polymorphic λ-calculus Fω [Girard 1972].
We divide each typed intermediate language into a type sub-language anda computation sub-language. The type language contains the top three levels.
Kind schemas classify kind terms while kinds classify type terms. We often
say that a kind term κ has kind schema u, or a type term τ has kind κ. We
assume all kinds used to classify type terms have kind schema Kind, and alltypes used to classify expressions have kind Ω. Both the function type τ1 → τ2and the polymorphic type ∀t : κ. τ have kind Ω. Following the tradition, we
sometimes say “a kind κ” to imply that κ has kind schema Kind, “a type τ ” toimply that τ has kind Ω, and “a type constructor τ ” to imply that τ has kind“κ → · · · → Ω.” Kind terms with other kind schemas, or type terms with otherkinds are strictly referred to as “kind terms” or “type terms.”
The computation language contains just the lowest level which is where wewrite the actual program. This language will eventually be compiled into machine code. We often use names such as computation terms, computation values, and computation functions to refer to various constructs at this level.
2.1 Representing propositions and proofs
The first step is to represent propositions and proofs for a particular logic in a
type-theoretic setting. The most established technique is to use the formulaeas-types principle (a.k.a. the Curry-Howard correspondence) [Howard 1980] to
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

5

The type language:(kscm) u ::= Kind | . . .
(kind) κ ::= κ1 → κ2 | Ω | . . .
(type)

τ ::= t | λt : κ. τ | τ1 τ2 | τ1 → τ2 | ∀t : κ. τ | . . .

The computation language:(exp)

e ::= x | λx : τ. e | e1 e2 | Λt : κ. e | e[τ ] | . . .
Fig. 1. Typed λ-calculi—a skeleton

map propositions and proofs into a typed λ-calculus. The essential idea, whichis inspired by constructive logic, is to use types (of kind Ω) to represent propositions, and expressions to represent proofs. A proof of an implication P ⊃ Q isa function object that yields a proof of proposition Q when applied to a proof of
proposition P . A proof of a conjunction P ∧ Q is a pair (e1 , e2 ) such that e1 is a
proof of P and e2 is a proof of Q. A proof of disjunction P ∨ Q is a pair (b, e)—atagged union—where b is either 0 or 1 and if b = 0, then e is a proof of P ; if b = 1
then e is a proof of Q. There is no proof for the false proposition. A proof ofa universally quantified proposition ∀x∈B.P (x) is a function that maps every
element b of the domain B into a proof of P (b) where P is a unary predicate
on elements of B. Finally, a proof of an existentially quantified proposition∃x∈B.P (x) is a pair (b, e) where b is an element of B and e is a proof of P (b).
Proof-checking in the logic now becomes typechecking in the corresponding
typed λ-calculus. There has been a large body of work done along this line in
the last 30 years; most type-based proof assistants are based on this fundamental principle. Good surveys of the previous work in this area can be foundin Barendregt [1991] and Barendregt and Geuvers [1999].
2.2 Representing certified binaries
Under the type-theoretic setting, a certified binary S is just a pair (v, e) thatconsists of:—a value v of type τ where v could be a function, a data structure, or any
combination of both;—and a proof e of P (v) where P is a unary predicate on elements of type τ .
Here e is just an expression with type P (v). The predicate P is a dependent
type constructor with kind τ → Ω. The entire package S has a dependent
strong-sum type Σx : τ.P (x).
For example, suppose Nat is the domain for natural numbers and Prime
is a unary predicate that asserts an element of Nat as a prime number; we
introduce a type nat representing Nat, and a type constructor prime (of kind
nat → Ω) representing Prime. We can build a certified prime-number package bypairing a value v (a natural number) with a proof for the proposition prime(v);the resulting certified binary has type Σx : nat. prime(x).
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

6·

Z. Shao et al.

Function values can be certified in the same way. Given a function f thattakes a natural number and returns another one as the result (i.e., f has typenat → nat), in order to show that f always maps a prime to another prime, weneed a proof for the following proposition:∀x∈Nat . Prime(x) ⊃ Prime(f (x))
In a typed setting, this universally quantified proposition is represented as adependent product type:Πx : nat. prime(x) → prime(f (x))
The resulting certified binary has type
Σf : nat → nat. Πx : nat. prime(x) → prime(f (x))
Here the type is not only dependent on values but also on function applications
such as f (x), so verifying the certified binary, which involves typechecking theproof, in turn requires evaluating the underlying function application.
2.3 The problems with dependent types
The above scheme unfortunately fails to work in the context of typed intermediate (or assembly) languages. There are at least four problems with dependent types; the third and fourth are present even in the general context.
First, real programs often involve effects such as assignment, I/O, or nontermination. Effects interact badly with dependent types. In our previous
example, suppose the function f does not terminate on certain inputs; thenclearly, typechecking—which could involve applying f —would become undecidable. It is possible to use the effect discipline [Sheldon and Gifford 1990] toforce types to be dependent on pure computation only, but this does not work insome typed λ-calculi; for example, a “pure” term in Girard’s λU [Girard 1972]
could still diverge.
Even if applying f does not involve any effects, we still have more serious problems. In a type-preserving compiler, the body of the function f has
to be compiled down to typed low-level languages. A few compilers perform
typed CPS conversion [Morrisett et al. 1998], but in the presence of dependent
types, this is a very difficult problem [Barthe et al. 1999]. Also, typechecking in low-level languages would now require performing the equivalent of
β-reductions on the low-level (assembly) code; this is awkward and difficult to
support cleanly.
Third, it is important to maintain a phase distinction between compile-time
typechecking and run-time evaluation. But having dependent strong-sum andproduct types makes it harder to preserve this property, especially if the typedependent values are first-class citizens (certified binaries are used to validate
arbitrary data structures and program functions so they should be allowed tobe passed as arguments, returned as results, or stored in memory).
Finally, supporting subset types in the presence of dependent strong-sum
and product types is difficult if not impossible [Constable 1985; Nordstrom
et al. 1990]. A certified binary of type Σx : nat. prime(x) contains a natural
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

7

number v and a proof that v is a prime. However, in many cases, we just wantv to belong to a subset type {x : nat | prime(x)}, i.e., v is a prime number but
the proof of this is not together with v; instead, it can be constructed from thecurrent context.
2.4 Separating the type and computation languages
We solve these problems by making sure that our type language is never dependent on the computation language. Because the actual computation term has
to be compiled down to assembly code in any case, it is a bad idea to treat it aspart of types. This separation immediately gives us back the phase-distinction
property.
To represent propositions and proofs, we lift everything one level up: we use
kinds to represent propositions, and type terms for proofs. The domain Nat isrepresented by a kind Nat; the predicate Prime is represented by a dependentkind term Prime which maps a type term of kind Nat to a proposition. A proof
for proposition Prime(n) certifies that the type term n is a prime number.
To maintain decidable typechecking, we insist that the type language isstrongly normalizing and free of side effects. This is possible because the typelanguage no longer depends on any runtime computation. Given a type-level
function g of kind Nat → Nat, we can certify that it always maps a prime toanother prime by building a proof τp for the following proposition, now represented as a dependent product kind:Πt : Nat.Prime(t) → Prime(g(t)).
Essentially, we circumvent the problems with dependent types by replacing
them with dependent kinds and by lifting everything (in the proof language)
one level up.
To reason about actual programs, we still have to connect terms in the typelanguage with those in the computation language. We follow Xi and Pfenning[1999] and use singleton types [Hayashi 1991] to relate computation values totype terms. In the previous example, we introduce a singleton type constructor
snat of kind Nat → Ω. Given a type term n of kind Nat, if a computation value v
has type snat(n), then v denotes the natural number represented by n.
A certified binary for a prime number now contains three parts: a type termn of kind Nat, a proof for the proposition Prime(n), and a computation valueof type snat(n). We can pack it up into an existential package and make it afirst-class value with type:∃n : Nat.∃t : Prime(n).snat(n).
Here we use ∃ rather than Σ to emphasize that types and kinds are no longer
dependent on computation terms. Under the erasure semantics [Crary et al.
1998], this certified binary is just an integer value of type snat(n) at run time.
Because there are strong separation between types and computation terms,
a value v of type ∃n : Nat.∃t : Prime(n).snat(n) is still implemented as a single
integer at runtime thus achieving the effect of the subset type.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

8·

Z. Shao et al.

We can also build certified binaries for programs that involve effects. Returning to our example, assume again that f is a function in the computation
language which may not terminate on some inputs. Suppose we want to certifythat if the input to f is a prime, and the call to f does return, then the result isalso a prime. We can achieve this in two steps. First, we construct a type-level
function g of kind Nat → Nat to simulate the behavior of f (on all inputs where
f does terminate) and show that f has the following type:∀n : Nat. snat(n) → snat(g(n))
Here following Figure 1, we use ∀ and → to denote the polymorphic and function types for the computation language. The type for f says that if it takes aninteger of type snat(n) as input and does return, then it will return an integerof type snat(g(n)). Second, we construct a proof τp showing that g always mapsa prime to another prime. The certified binary for f now also contains threeparts: the type-level function g, the proof τp , and the computation function f
itself. We can pack it into an existential package with type:∃g : Nat → Nat. ∃p : (Πt : Nat.Prime(t) → Prime(g(t))).
∀n : Nat. snat(n) → snat(g(n))
Notice this type also contains function applications such as g(n), but g is a
type-level function which is always strongly normalizing, so typechecking is
still decidable.
It is important to understand the difference between typechecking and “typeinference.” The main objective of this paper is to develop a fully explicit framework where proofs and assertions can be used to certify programs that may
contain side effects—the most important property is that typechecking (andproof-checking) in the new framework must be decidable. Type inference (i.e.,
finding the proofs), on the other hand, could be undecidable: given an arbitrarily complex function f , we clearly cannot hope to automatically construct thecorresponding g. In practice, however, it is often possible to first write down
the specification g and then to write the corresponding program f . Carryingout this step and constructing the proof that f follows g is a challenging task,
as in any other PCC system [Necula 1998; Appel and Felty 2000].
2.5 Designing the type language
We can incorporate propositions and proofs into typed intermediate languages,
but designing the actual type language is still a challenge. For decidable typechecking, the type language should not depend on the computation language
and it must satisfy the usual meta-theoretical properties (e.g., strong normalization).
But the type language also has to fulfill its usual responsibilities. First, it
must provide a set of types (of kind Ω) to classify the computation terms. A
typical compiler intermediate language supports a large number of basic type
constructors (e.g., integer, array, record, tagged union, and function). Thesetypes may change their forms during compilation, so different intermediate
languages may have different definitions of Ω; for example, a computation
function at the source level may be turned into CPS-style, or later, to one whose
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

9

arguments are machine registers [Morrisett et al. 1998]. We also want to support intensional type analysis [Harper and Morrisett 1995] which is crucial for
typechecking runtime services [Monnier et al. 2001].
Our solution is to provide a general mechanism of inductive definitions in
our type language and to define each such Ω as an inductive kind. This wasmade possible only recently [Trifonov et al. 2000] and it relies on the use ofpolymorphic kinds. Taking the type language in Figure 1 as an example, we
add kind variables k and polymorphic kinds Πk : u. κ, and replace Ω and its
associated type constructors with inductive definitions (not shown):(kscm) u ::= Kind | . . .
(kind) κ ::= κ1 → κ2 | k | Πk : u. κ | . . .
(type) τ ::= t | λt : κ. τ | τ1 τ2 | λk : u. τ | τ [κ] | . . .
At the type level, we add kind abstraction λk : u. τ and kind application τ [κ].
The kind Ω is now inductively defined as follows (see Sections 3–4 for moredetails):
Inductive Ω : Kind := →→: Ω→Ω→Ω| ∀ : Πk : Kind. (k → Ω) → Ω..
.
Here →→ and ∀ are two of the constructors (of Ω). The polymorphic type ∀t : κ. τ
is now written as ∀ [κ] (λt : κ. τ ); the function type τ1 → τ2 is just →→ τ 1 τ2 .
Inductive definitions also greatly increase the programming power of ourtype language. We can introduce new data objects (e.g., integers, lists) anddefine primitive recursive functions, all at the type level; these in turn areused to help model the behaviors of the computation terms.
To have the type language double up as a proof language for higher-order
predicate logic, we add dependent product kind Πt : κ1 . κ2 , which subsumes thearrow kind κ1 → κ2 ; we also add kind-level functions to represent predicates.
Thus the type language naturally becomes the calculus of inductive constructions [Paulin-Mohring 1993].
2.6 Proof-preserving compilation
Even with a proof system integrated into our intermediate languages, we still
have to make sure that they can be CPS- and closure-converted down to lowlevel languages. These transformations should preserve proofs represented in
the type system; in fact, they should not traverse the proofs at all since doing
so is impractical with large proof libraries.
These challenges are nontrivial but the way we set up our type system makes
it easier to solve them. First, because our type language does not depend on
the computation language, we do not have the difficulties involved in CPSconverting dependently typed λ-calculi [Barthe et al. 1999]. Second, all our intermediate languages share the same type language, thus also the same proof
library; this is possible because the Ω kind (and the associated types) for eachintermediate language is just a regular inductive definition.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

10·

Z. Shao et al.

Finally, a type-preserving program transformation often requires translating the source types (of the source Ω kind) into the target types (of the target Ωkind). Existing CPS- and closure-conversion algorithms [Morrisett et al. 1998;
Harper and Lillibridge 1993; Minamide et al. 1996] all perform this translation
at the meta-level; they have to go through every type term (thus every proof
term in our setting) during the translation, because any type term may contain a sub-term which has the source Ω kind. In our framework, the fact thateach Ω kind is inductively defined means that we can internalize and write thetype-translation function inside our type language itself. This leads to elegant
algorithms that do not traverse any proof terms but still preserve typing andproofs (see Sections 5–6 for details).
2.7 Putting it all together
A certifying compiler in our framework will have a series of intermediate languages, each corresponding to a particular stage in the compilation process;all will share the same type language. An intermediate language is now justthe type language plus the corresponding computation terms, along with theinductive definition for the corresponding Ω kind. In the rest of this paper, wefirst give a formal definition of our type language (which will be named TLfrom now on) in Section 3; we then present a sample computation language λH
in Section 4; we show how λH can be CPS- and closure-converted into low-level
languages in Sections 5–6; finally, we discuss related work and then conclude.
3. THE TYPE LANGUAGE TL
Our type language TL resembles the calculus of inductive constructions (C IC)
implemented in the Coq proof assistant [Huet et al. 2000]. This is a great
advantage because Coq is a very mature system and it has a large set of proof
libraries which we can potentially reuse. For this paper, we decided not todirectly use C IC as our type language for three reasons. First, C IC contains
some features designed for program extraction [Paulin-Mohring 1989] which
are not required in our case (where proofs are only used as specifications forthe computation terms). Second, as far as we know, there are still no formal
studies covering the entire C IC language. Third, for theoretical purposes, wewant to understand what are the most essential features for modeling certified
binaries. In practice these differences are fairly minor. The main objectives ofthis section is to give a quick introduction to the essential features in the Coqlike dependent type theory.
3.1 Motivations
Following the discussion in Section 2.5, we organize TL into the following threelevels:(kscm) u ::= z | Πt : κ. u | Πk : u. u0 | Kind
(kind) κ ::= k | λt : κ. κ0 | κ[τ ] | λk : u. κ | κ κ0 | Πt : κ. κ0 | Πk : u. κ| Πz : Kscm. κ | Ind(k : Kind){~κ} | Elim[κ0 , u](τ ){~κ}(type) τ ::= t | λt : κ. τ | τ τ 0 | λk : u. τ | τ [κ] | λz : Kscm. τ | τ [u]| Ctor (i, κ) | Elim[κ0 , κ](τ 0 ){~τ }ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

11

Here kind schemas (kscm) classify kind terms while kinds classify type terms.
There are variables at all three levels: kind-schema variables z, kind variablesk, and type variables t. We have an external constant Kscm classifying all thekind schemas; essentially, TL has an additional level above kscm, of which
Kscm is the sole member.
A good way to comprehend TL is to look at its five Π constructs: there arethree at the kind level and two at the kind-schema level. We use a few examples to explain why each of them is necessary. Following the tradition, we use
arrow terms (e.g., κ1 → κ2 ) as a syntactic sugar for the non-dependent Π terms(e.g., Πt : κ1 . κ2 is non-dependent if t does not occur free in κ2 ).
—Kinds Πt : κ. κ0 and κ → κ0 are used to typecheck the type-level function
λt : κ. τ and the corresponding application form τ1 τ2 . Assuming Ω and Nat
are inductive kinds (defined later) and Prime is a predicate with kind schema
Nat → Kind, we can write a type term such as λt : Ω. t which has kind Ω → Ω, a
type-level arithmetic function such as plus which has kind Nat → Nat → Nat, orthe universally quantified proposition in Section 2.2 which is represented as
the kind Πt : Nat.Prime(t) → Prime(g(t)).
—Kinds Πk : u. κ and u → κ are used to typecheck the type-level kind abstraction λk : u. τ and its application form τ [κ]. As mentioned in Section 2.5, thisis needed to support intensional analysis of quantified types [Trifonov et al.
2000]. It can also be used to define logic connectives and constants, as inTrue : Kind
False : Kind==Πk : Kind. k → kΠk : Kind. k

True has the polymorphic identity as a proof:
id : True=

λk : Kind. λt : k. t

but False is not inhabited (this is essentially the consistency property of TL
which we will show later).
—Kind Πz : Kscm. κ is used to typecheck the type-level kind-schema abstraction
λz : Kscm. τ and the corresponding application τ [u]. This is not in the core calculus of constructions [Coquand and Huet 1988]. We use it in the inductive
definition of Ω (see Section 4) where both the ∀ Kscm and ∃∃Kscm constructors
have kind Πz : Kscm. (z → Ω) → Ω. These two constructors in turn allow us totypecheck predicate-polymorphic computation terms, which occur fairly often since the closure-conversion phase turns all functions with free predicate
variables (e.g., Prime) into predicate-polymorphic ones.
—Kind schemas Πt : κ. u and κ → u are used to typecheck the kind-level typeabstraction λt : κ. κ0 and the application form κ[τ ]. The predicate Prime has
kind schema Nat → Kind. A predicate with kind schema Πt : Nat. Prime(t) → Kind
is only applicable to prime numbers. We can also define for instance a binary
relation:
LT : Nat → Nat → Kind

so that LT t1 t2 is a proposition asserting that the natural number represented by t1 is less than that of t2 .
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

12·

Z. Shao et al.

Inductive Bool : Kind := true : Bool
| false : Bool

Inductive Nat : Kind := zero : Nat| succ : Nat → Natplus : Nat → Nat → Nat

le : Nat → Nat → Boolplus(zero)= λt : Nat. tplus(succ t) = λt0 : Nat. succ ((plus t) t0 )le(zero)= λt : Nat. truele(succ t) = λt0 : Nat. ifez t0 Bool false (le t)ifez : Nat → (Πk : Kind. k → (Nat → k) → k)lt : Nat → Nat → Boolifez(zero)= λk : Kind. λt1 : k. λt2 : Nat → k. t1ifez(succ t) = λk : Kind. λt1 : k. λt2 : Nat → k. t2 t

lt = λt : Nat. le (succ t)
Cond : Bool → Kind → Kind → Kind
Cond(true) = λk1 : Kind. λk2 : Kind. k1
Cond(false) = λk1 : Kind. λk2 : Kind. k2

Fig. 2.

Examples of inductive definitions and elimination—Kind schemas Πk : u. u0 and u → u0 are used to typecheck the kind-level
function λk : u. κ and the application form κ1 κ2 . We use it to write higherorder predicates and logic connectives. For example, the logical negation
operator can be written as follows:
Not : Kind → Kind=

λk : Kind. k → False

The consistency of TL implies that a proposition and its negation cannot beboth inhabited—otherwise applying the proof of the second to that of thefirst would yield a proof of False.
TL also provides a general mechanism for defining inductive types [PaulinMohring 1993]. The term Ind(k : Kind){~κ} introduces an inductive kind k withconstructors whose kinds are listed in ~κ. Here k must only occur “positively”
inside each κi (see Appendix A for the formal definition of positivity). The term
Ctor (i, κ) refers to the i-th constructor in an inductive kind κ. For presentation,
we will use a more friendly syntax in the rest of this paper. An inductive kind
I = Ind(k : Kind){~κ} will be written as:
Inductive I : Kind := c1 : [I/k]κ1| c2 : [I/k]κ2..
.
| cn : [I/k]κn

We give an explicit name ci to each constructor, so ci is just an abbreviation ofCtor (i, I). For simplicity, the current version of TL does not include parame-terized inductive kinds, but supporting them is quite straightforward [Werner
1994; Paulin-Mohring 1993].
TL provides two iterators to support primitive recursion on inductive kinds.
The small elimination Elim[κ0 , κ](τ 0 ){~τ } takes a type term τ 0 of inductive kind
κ0 , performs the iterative operation specified by ~τ (which contains a branchfor each constructor of κ0 ), and returns a type term of kind κ[τ 0 ] as the result.
The large elimination Elim[κ0 , u](τ ){~κ} takes a type term τ of inductive kind κ0 ,performs the iterative operation specified by ~κ, and returns a kind term of kind
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries(sort) s::= Kind | Kscm | Ext(var) X::= z | k | t·

13(ptm) A, B ::= s | X | λX : A. B | A B | ΠX : A. B
~ | Ctor (i, A) | Elim[A0 , B 0 ](A){B}~| Ind(X : Kind){A}
Fig. 3.

Syntax of the type language TL

schema u as the result. These iterators generalize the Typerec operator used inintensional type analysis [Harper and Morrisett 1995; Crary and Weirich 1999;
Trifonov et al. 2000].
Figure 2 gives a few examples of inductive definitions including the inductive kinds Bool and Nat and several type-level functions which we will use in
Section 4. The small elimination for Nat takes the form Elim[Nat, κ](τ 0 ){τ1 ; τ2 }.
Here, κ is a dependent kind with kind schema Nat → Kind; τ 0 is the argument
which has kind Nat. The term in the zero branch, τ1 , has kind κ[τ 0 ]. The termin the succ branch, τ2 , has kind Nat → κ[τ 0 ] → κ[τ 0 ]. TL uses the ι-reduction to
perform the iterator operation. For example, the two ι-reduction rules for Nat
work as follows:
Elim[Nat, κ](zero){τ1 ; τ2 } ;ι τ1
Elim[Nat, κ](succ τ ){τ1 ; τ2 } ;ι τ2 τ (Elim[Nat, κ](τ ){τ1 ; τ2 })The general ι-reduction rule is defined formally in Appendix A. In our examples, we take the liberty of using the pattern-matching syntax (as in ML) to
express the iterator operations, but they can be easily converted back to the
Elim form.
In Figure 2, plus is a function which calculates the sum of two natural numbers. The function ifez behaves like a switch statement: if its argument is zero,
it returns a function that selects the first branch; otherwise, the result takes
the second branch and applies it to the predecessor of the argument. The function le evaluates to true if its first argument is less than or equal to the second.
The function lt performs the less-than comparison.
The definition of function Cond, which implements a conditional with resultat the kind level, is expanded into TL using large elimination on Bool, of theform Elim[Bool, u](τ ){κ1 ; κ2 }, where τ is of kind Bool, and both the true and false
branches (κ1 and κ2 ) have kind schema u.
3.2 Formalization
We want to give a formal semantics to TL and then reason about its metatheoretic properties. But the five Π constructs have many similarities, so in
the rest of this paper, we will model TL as a pure type system (PTS) [Barendregt 1991] extended with inductive definitions. Intuitively, instead of having
a separate syntactic category for each level, we collapse all kind schemas u,kind terms κ, type terms τ , and the external constant Kscm into a single setof pseudoterms (ptm), denoted as A or B. Similar constructs can now sharetyping rules and reduction relations.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

14·

Z. Shao et al.

Figure 3 gives the syntax of TL, written in PTS style. There is now onlyone Π construct (ΠX : A. B), one λ-abstraction (λX : A. B), and one application
form (A B); two iterators for inductive definitions are also merged into one~(Elim[A0 , B 0 ](A){B}).
We use X and Y to represent generic variables, but wewill still use t, k, and z if the class of a variable is specific.
TL has the following PTS specification which we will use to derive its typing
rules:
S
A
R

=
=
=

{Kind, Kscm, Ext}
{Kind : Kscm, Kscm : Ext}{(Kind, Kind), (Kscm, Kind), (Ext, Kind),(Kind, Kscm), (Kscm, Kscm)}

Here S is the set of emphsorts used to denote universes. We have added theconstant Ext to support quantification over Kscm. The names we use for sortsreflect the fact that we have lifted the language one level up; they are related
to other systems via the following table:
SystemNotation

TL
Werner [1994]
Coq/C IC [Huet et al. 2000]
Barendregt [1991]

Kind

Kscm

Ext

Set

Type

Ext

Set, Prop

Type(0)Type(1)∗

2

4

The axioms in the set A denote the relationship between different sorts; anaxiom “s1 : s2 ” means that s2 classifies s1 . The pairs (rules) in the set R areused to define the well-formed Π constructs, from which we can deduce the setof well-formed λ-definitions and applications. For example, the five rules for
TL can be related to the five Π constructs through the following table:(Kind, Kind)(Kscm, Kind)(Ext, Kind)(Kind, Kscm)(Kscm, Kscm)

ΠX : A. B

λX : A. B

AB

Πt : κ1 . κ2
Πk : u. κΠz : Kscm. κ
Πt : κ. u
Πk : u1 . u2

λt : κ. τ
λk : u. τ
λz : Kscm. τ
λt : κ1 . κ2
λk : u. κτ 1 τ2
τ [κ]
τ [u]
κ[τ ]
κ κ0

We define a context ∆ as a list of bindings from variables to pseudoterms:(ctxt) ∆ ::= · | ∆, X : A
The typing judgment for TL in PTS style now takes the form ∆ ` A : A0 ,meaning that within context ∆, the pseudoterm A is well-formed and has A0
as its classifier. We can now write a single typing rule for all the Π constructs:∆ ` A : s1∆, X : A ` B : s2 (s1 , s2 ) ∈ R∆ ` ΠX : A. B : s2

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

( PROD )A Type System for Certified Binaries·

15

Taking rule (Kind, Kscm) as an example, to build a well-formed term ΠX : A. B,
which will be a kind schema (because s2 is Kscm), we need to show that A is awell-formed kind and B is a well-formed kind schema assuming X has kind A.
We can also share the typing rules for all λ-definitions and applications:∆, X : A ` B : B 0∆ ` ΠX : A. B 0 : s∆ ` λX : A. B : ΠX : A. B 0( FUN )∆ ` A : ΠX : B 0 . A0
∆ ` B : B0
∆ ` A B : [B/X]A0( APP )The reduction relations can also be shared. TL supports the standard β- and ηreductions (denoted by ;β and ;η ) plus the previously mentioned ι-reduction(denoted by ;ι ) on inductive objects (see Appendix A). The relations β , η ,and ι are the contextual closures of the relations ;β , ;η , and ;ι respectively.
We use ; and  for the unions of the above relations. We also write =βηι forthe reflexive, symmetric, and transitive closure of .
The complete typing rules for TL and the definitions of all the reduction relations are given in Appendix A. Following Werner [1994] and Geuvers [1993],
we have shown that TL satisfies all the key meta-theoretic properties, including subject reduction, strong normalization, Church-Rosser (and confluence),and consistency of the underlying logic. The detailed proofs for these properties are given in the companion technical report [Shao et al. 2001].
Theorem 3.1 (Subject reduction) If the judgment ∆ ` A : B is derivable,
and A  A0 , then ∆ ` A0 : B is derivable.
Proof sketch The detailed proof is given in the companion technical report [Shao et al. 2001]. We first define a calculus of unmarked terms. These
are TL terms with no annotations at lambda abstractions. We show that thislanguage is confluent. From this, we can prove that TL satisfies a weak formof confluence (also known as the Geuvers lemma [Geuvers 1993]); it says that aterm that is equal to one in head normal form can be reduced to an η-expanded
version of this head normal form. From the weak confluence, we then prove theinversion lemma which relates the structure of a term to its typing derivation.
We then prove the uniqueness of types and subject reduction for βι reductions.
Finally, we prove the strengthening lemma and then subject reduction for η
reduction.
Theorem 3.2 (Strong normalization) All well typed terms are strongly
normalizing.
Proof sketch The detailed proof is presented in our technical report [Shaoet al. 2001]. It is a straightforward extension of the proof given by Werner[1994]. First we introduce a calculus of pure terms; this is just the pure λcalculus extended with a recursive filtering operator; we do this so that we
can operate in a confluent calculus. We then define a notion of reducibility
candidates; every kind schema gives rise to a reducibility candidate; we also
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

16·

Z. Shao et al.

show how these candidates can be constructed inductively. We define a notion of well constructed kinds which is a weak form of typing. We associate aninterpretation to each well formed kind. We show that under adequate conditions, this interpretation is a candidate. We show that type level constructs
such as abstractions and constructors belong to the candidate associated with
their kind. We show that the interpretation of a kind remains the same under βη reduction. We then define a notion of kinds that are invariant on their
domain—these are kinds whose interpretation remains the same upon reduction. We show that kinds formed with large elimination are invariant on their
domain. From here we can show the strong normalization of the calculus ofpure terms; we show that if a type is well formed, then the pure term derived
from it is strongly normalizing. Finally, we reduce the strong normalization of
all well formed terms to the strong normalization of pure terms.
Theorem 3.3 (Church-Rosser) Let ∆ ` A : B and ∆ ` A0 : B be two
derivable judgments. If A =βηι A0 , and if A and A0 are in normal form, thenA = A0 .
Proof sketch The detailed proof is given in the companion technical report [Shao et al. 2001]. We first prove that a well typed term in βι normal form
has the same η reductions as its corresponding unmarked term. From here, weknow that if A and A0 are in normal form, then their corresponding unmarked
terms are equal. We then show that the annotations in the λ-abstractions areequal.
Theorem 3.4 (Consistency of the logic) There exists no term A for which· ` A : False.
Proof sketch Suppose A is a term for which · ` A : False. By Theorem 3.2,
there exists a normal form B for A. By Theorem 3.1 · ` B : False. We can show
now that this leads to a contradiction by case analysis of the possible normal
forms of types in the calculus.
4. THE COMPUTATION LANGUAGE λH
The language of computations λH for our high-level certified intermediate format uses proofs, constructed in the type language, to verify propositions which
ensure the runtime safety of the program. Furthermore, in comparison withother higher-order typed calculi, the types assigned to programs can be morerefined, since program invariants expressible in higher-order predicate logic
can be represented in our type language. These more precise types serve as
more complete specifications of the behavior of program components, and thus
allow the static verification of more programs.
One approach to presenting a language of computations is to encode its syntax and semantics in a proof system, with the benefit of obtaining machinecheckable proofs of its properties, for instance type safety. This appears tobe even more promising for a system with a type language like C IC, which is
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries

(exp)

e

·

17

::= x | n | tt | ff | f | fix x : A. f | e e0 | e[A] | hX = A, e : A0 i
| open e as hX, xi in e0 | he0 , . . . en−1 i | sel[A](e, e0 )| e aop e0 | e cop e0 | if [A, A0 ](e, X1 . e1 , X2 . e2 )where n ∈ N

(fun)

f

::= λx : A. e | ΛX : A. f(arith) aop ::= + | . . .
(cmp) cop ::= < | . . .
Fig. 4. Syntax of the computation language λH .

more expressive than higher-order predicate logic: The C IC proofs of some program properties, embedded as type terms in the program, may not be easily
representable in meta-logical terms, thus it may be simpler to perform all thereasoning in C IC. However our exposition of the language TL is focused onits use as a type language, and consequently it does not include all featuresof C IC. We therefore leave this possibility for future work, and give a standard meta-logical presentation instead; we address some of the issues related
to adequacy in our discussion of type safety.
In this section we use the unqualified “term” to refer to a computation term
(expression) e, with syntax defined in Figure 4. Most of the constructs areborrowed from standard higher-order typed calculi. To simplify the exposition we only consider constants representing natural numbers (n is the value
representing n ∈ N) and boolean values (tt and ff). The term-level abstraction
and application are standard; type abstractions and fixed points are restricted
to function values, with the call-by-value semantics in mind and to simplify
the CPS and closure conversions. The type variable bound by a type abstraction, as well as the one bound by the open construct for packages of existential
type, can have either a kind or a kind schema. Dually, the type argument ina type application, and the witness type term A in the package construction
hX = A, e : A0 i can be either a type term or a kind term.
The constructs implementing tuple operations, arithmetic, and comparisons
have nonstandard static semantics, on which we focus in section 4.2, but theirruntime behavior is standard. The branching construct is parameterized at
the type level with a proposition (which is dependent on the value of the testterm) and its proof; the proof is passed to the executed branch.
4.1 Dynamic semantics
We present a small step call-by-value operational semantics for λH in the styleof Wright and Felleisen [1994]. The values are defined inductively by
v ::= n | tt | ff | f | fix x : A. f | hX = A, v : A0 i | hv0 , . . . vn−1 i
The reduction relation ,→ is specified by the following rules.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

18·

Z. Shao et al.

(λx : A. e) v ,→ [v/x]e(R-β)(ΛX : B. f )[A] ,→ [A/X]f(R- TY-β)sel[A](hv0 , . . . vn−1 i, m) ,→ vm(m < n)open hX 0 = A, v : A0 i as hX, xi in e ,→ [v/x][A/X]e(R- SEL )(R- OPEN )(fix x : A. f ) v ,→ ([fix x : A. f /x]f ) v(R- FIX )(fix x : A. f )[A0 ] ,→ ([fix x : A. f /x]f )[A0 ](R- TYFIX )m + n ,→ m + n(R- ADD )m < n ,→ tt(m < n)(R- LT-T)m < n ,→ ff(m ≥ n)(R- LT-F)

if [B, A](tt, X1 . e1 , X2 . e2 ) ,→ [A/X1 ]e1(R- IF -T)

if [B, A](ff, X1 . e1 , X2 . e2 ) ,→ [A/X2 ]e2(R- IF -F)

An evaluation context E encodes the call-by-value discipline:
E ::= • | E e | v E | E[A] | hX = A, E : A0 i | open E as hX, xi in e
| hv0 , . . . vi−1 , E, ei+1 , . . . , en−1 i | sel[A](E, e) | sel[A](v, E)| if [A, A0 ](E, X1 . e1 , X2 . e2 ) | E aop e | v aop E | E cop e | v cop E
The notation E{e} stands for the term obtained by replacing the hole • in E bye. The single step computation 7→ relates E{e} to E{e0 } when e ,→ e0 , and 7→∗
is its reflexive transitive closure.
As shown the semantics is standard except for some additional passing oftype terms in R- SEL and R- IF -T/F. However an inspection of the rules showsthat types are irrelevant for the evaluation, hence a type-erasure semantics, inwhich all type-related operations and parameters are erased, would be entirely
standard.
4.2 Static semantics
The static semantics of λH shows the benefits of using a type language as expressive as TL. We can now define the type constructors of λH as constructorsof an inductive kind Ω, instead of having them built into λH . As we will showin Section 5, this property is crucial for the conversion to CPS, since it makes
possible transforming direct-style types to CPS types within the type language.
Inductive Ω : Kind := snat : Nat → Ω| sbool : Bool → Ω|→→ :Ω→Ω→Ω| tup : Nat → (Nat → Ω) → Ω| ∀ Kind : Πk : Kind. (k → Ω) → Ω| ∃∃Kind : Πk : Kind. (k → Ω) → Ω| ∀ Kscm : Πz : Kscm. (z → Ω) → Ω| ∃∃Kscm : Πz : Kscm. (z → Ω) → Ω
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

19

Informally, all well-formed computations have types of kind Ω, including singleton types of natural numbers snat A and boolean values sbool B, as well asfunction, tuple, polymorphic and existential types. To improve readability wealso define the syntactic sugar
A→B≡→
→ AB

∀s X : A. B ≡ ∀ s A (λX : A. B)
where s ∈ {Kind, Kscm}∃s X : A. B ≡ ∃∃s A (λX : A. B)
and often drop the sort s when s = Kind; for example the type void, containing
no values, is defined as ∀t : Ω. t ≡ ∀ Kind Ω (λt : Ω. t).
Using this syntactic sugar we can give a familiar look to many of the formation rules for λH expressions and functional values. Figure 5 contains theinference rules for deriving judgments of the form ∆; Γ ` e : A, which assign
type A to the expression e in a context ∆ and a type environment Γ defined by(type env) Γ ::= · | Γ, x : A
We introduce some of the notation used in these rules in the course of the
discussion.
Rules E- NAT, E- TRUE, and E- FALSE assign singleton types to numeric andboolean constants. For instance the constant 1 has type snat (succ zero) in any
valid environment. In rule E- NAT we use the meta-function b· to map natural
numbers n ∈ N to their representations as type terms. It is defined inductivelyd = succ n
by b
0 = zero and n+1
b, so ∆ ` nb : Nat holds for all valid ∆ and n ∈ N.
Singleton types play a central role in reflecting properties of values in thetype language, where we can reason about them constructively. For instancerules E- ADD and E- LT use respectively the type terms plus and lt (defined in
Section 3) to reflect the semantics of the term operations into the type level via
singleton types.
However, if we could assign only singleton types to computation terms, ina decidable type system we would only be able to typecheck terminating programs. We regain expressiveness of the computation language using existential types to hide some of the too detailed type information. Thus for example
one can define the usual types of all natural numbers and boolean values as
nat : Ω = ∃t : Nat. snat tbool : Ω = ∃t : Bool. sbool t

For any term e with singleton type snat A the package ht = A, e : snat ti has typenat. Since in a type-erasure semantics of λH all types and operations on them

are erased, there is no runtime overhead for the packaging. For each n ∈ Nb ≡ ht = n
there is a value of this type denoted by nb, n : snat ti. Operations on
terms of type nat are derived from operations on terms of singleton types of theform snat A; for example an addition function of type nat → nat → nat is definedas the expression
add = λx1 : nat. λx2 : nat.
open x1 as ht1 , x01 i inopen x2 as ht2 , x02 i in
ht = plus t1 t2 , x01 + x02 : snat ti
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

20·

Z. Shao et al.

∆ ` Kind : Kscm
∆ ` · ok(TE- MT )∆ ` Γ ok∆; Γ ` x : Γ(x)(E- VAR )∆; Γ ` e : snat A(E- NAT )∆; Γ ` e : snat A∆ ` Γ ok∆; Γ ` n : snat nb∆ ` Γ ok∆ ` A:Ω∆ ` Γ, x : A ok∆; Γ `∆; Γ `∆ ` Γ ok∆; Γ ` tt : sbool true

(E- TRUE )∆; Γ ` e1 : A → A0 ∆; Γ ` e2 : A

e : A0∆; Γ ` e1 e2 : A0

(E- FUN )∆ ` B:s∆, X : B; Γ ` f : A∆; Γ ` ΛX : B. f : ∀s X : B. A
where X ∈/ ∆, s 6= Ext∆; Γ ` e : ∀ s B A(E- TFUN )∆, X : B ` A0 : Ω∆; Γ ` e : [A/X]A0(E- PACK )∆; Γ ` hX = A, e : A0 i : ∃s X : B. A0
where s 6= Ext∆; Γ `

where s 6= Ext∆; Γ ` e : ∃∃s B A∆ ` A0 : Ω∆, X : B; Γ, x : A X ` e0 : A0∆; Γ ` open e as hX, xi in e0 : A0
where X ∈/ ∆, s 6= Ext∆; Γ ` e0 : snat A0∆; Γ `∆; Γ ` e : A∆ ` A : LT A0 A00

sel[A](e, e0 ) : B A0A =βηι A0∆; Γ `

Fig. 5.

(E- IF )(E- APP )∆ ` A0 : B

e[A0 ] : A A0

for all i < n∆; Γ ` ei : Ai∆; Γ ` he0 , . . . en−1 i : tup nb (nth (A0 :: . . . ::An−1 ::nil))∆; Γ ` e : tup A00 B(E- LT )(E- FIX )∆; Γ ` λx : A. e : A → A0

∆ ` A:B∆ ` B:s(E- ADD )∆; Γ ` if [B, A](e, X1 . e1 , X2 . e2 ) : A0

∆ ` A:Ω∆; Γ, x : A ` f : A∆; Γ ` fix x : A. f : A∆; Γ, x : A `∆; Γ ` e0 : snat A0e < e0 : sbool (lt A A0 )∆ ` B : Bool → Kind ∆; Γ ` e : sbool A00∆ ` A : B A00∆, X1 : B true; Γ ` e1 : A0
∆ ` A0 : Ω∆, X2 : B false; Γ ` e2 : A0

∆ ` Γ ok
(E- FALSE )∆; Γ ` ff : sbool false∆ ` A:Ω∆; Γ ` e0 : snat A0

e + e0 : snat (plus A A0 )(TE- EXT )∆ ` A0 : Ω

e : A0(E- TAPP )(E- OPEN )(E- TUP )(E- SEL )(E- CONV )Static semantics of the computation language λH .

Rule E- TUP assigns to a tuple a type of the form tup A B, in which the tup
constructor is applied to a type A representing the tuple size, and a function B
mapping offsets to the types of the tuple components. This function is definedin terms of operations on lists of types:
Inductive List : Kind := nil : List | cons : Ω → List → List
nth : List → Nat → Ω
nth nil= λt : Nat. voidnth (cons t1 t2 ) = λt : Nat. ifez t Ω t1 (nth t2 )ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

21

Thus nth L n
b reduces to the n-th element of the list L when n is less than thelength of L, and to void otherwise. We also use the infix form A::A0 ≡ cons A A0 .
The type of pairs is derived: A × A0 ≡ tup b
2 (nth (A::A0 ::nil)). Thus for instancecb·;· ` h42, 7i : snat 42 × snat 7 is a valid judgment.
The rules for selection and testing for the less-than relation (the only comparison we discuss for brevity) refer to the kind term LT with kind schema
Nat → Nat → Kind. Intuitively, LT represents a binary relation on kind Nat, soLT mb nb is the kind of type terms representing proofs of m < n. LT can be thoughtof as the parameterized inductive kind of proofs constructed from instances of
the axioms ∀n ∈ N. 0 < n+1 and ∀m, n ∈ N. m < n ⊃ m+1 < n+1:
Inductive LT : Nat → Nat → Kind:= ltzs : Πt : Nat. LT zero (succ t)| ltss : Πt : Nat. Πt0 : Nat. LT t t0 → LT (succ t) (succ t0 )To simplify the presentation of our type language, we allowed inductive kindsof kind scheme Kind only. Thus to stay within the scope of this paper we actually
use a Church encoding of LT (given in Section 4.3); this is sufficient since wenever analyze proof objects, so the full power of elimination is unnecessary for
our use of LT.
In the component selection construct sel[A](e, e0 ) the type A represents a
proof that the value of the subscript e0 is less than the size of the tuple e.
In rule E- SEL this condition is expressed as an application of the type term LT.
Due to the consistency of the logic represented in the type language, only theexistence and not the structure of the proof object A is important. Since its
existence is ensured statically in a well-formed expression, A would be eliminated in a type-erasure semantics.
The conditional if [B, A](e, X1 . e1 , X2 . e2 ) allows information obtained dynamically (e.g., through comparisons) to be made available for static reasoning in
the form of proof parameters to its branches. The type term A represents a
proof of the proposition encoded by either B true or B false, depending on thevalue of e. This proof is bound to the type variable (X1 or X2 ) of the appropriate
branch, which can use it in the construction of other proofs, or with a proofconsuming primitive like sel. The correspondence between the value of e andthe kind of A is again established through a singleton boolean type. Thus for
instance if the run-time value of e asserts the truthfulness of some proposition
P , since the type parameter A00 of the singleton type of e reflects the value ofe at the type level, we can define B so that B A00 represents P or ¬P , depending on whether A00 =βηι true or A00 =βηι false, and reason in each of the two
branches under the assumption that P or ¬P , respectively. Of course, for thisreasoning to be sound, we need a proof that A00 indeed reflects the truthfulnessof P , that is, we need a proof term A of kind B A00 .
In fact if is more flexible than that, because B false does not have to be thenegation of B true, one can have imprecise information flow into the branches.
In particular the encoding of the usual oblivious (in proof-passing sense) if ispossible using B = λt : Bool. True; section 4.3 gives another example, where theinformation is precise only in one branch of the conditional.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

22·

Z. Shao et al.

4.3 Example: Bound check elimination
A simple example of the generation, propagation, and use of proofs in λH is afunction which computes the sum of the components of any vector of naturals.
Let us first introduce some auxiliary types and functions. The type assigned
to a homogeneous tuple (vector) of n terms of type A is βηι-convertible to theform vec nb A for
vec : Nat → Ω → Ω

vec = λt : Nat. λt0 : Ω. tup t (nth (repeat t t0 ))whererepeat : Nat → Ω → List
repeat zero
= λt0 : Ω. nil
repeat (succ t) = λt0 : Ω. t0 ::(repeat t) t0

Then we can define a term which sums the elements of a vector with a given
length as follows:
sumVec : ∀t : Nat. snat t → vec t nat → nat≡ Λt : Nat. λn : snat t. λv : vec t nat.
(fix loop : nat → nat → nat.
λi : nat. λsum : nat. open i as ht0 , i0 i in
if [LTOrTrue t0 t, ltPrf t0 t](i0 < n,t1 . loop (add i b1) (add sum (sel[t1 ](v, i0 ))),
bb
t2 . sum)) 0 0

where

LTOrTrue : Nat → Nat → Bool → Kind
LTOrTrue = λt1 : Nat. λt2 : Nat. λt : Bool. Cond t (LT t1 t2 ) Trueand ltPrf of kind Πt0 : Nat. Πt : Nat. LTOrTrue t0 t (lt t0 t) is a type term defined below; as its kind suggests, ltPrf A A0 evaluates to a proof of LT A A0 , if A and A0
represent natural numbers n and n0 such that n < n0 .
The comparison i0 < n, used in this example as a loop termination test, checks
whether the index i0 is smaller than the vector size n. If it is, the adequacyof the type term lt with respect to the less-than relation ensures that the typeterm ltPrf t0 t represents a proof of the corresponding proposition at the typelevel, namely LT t0 t. This proof is then bound to t1 in the first branch of theif, and the sel construct uses it to verify that the i 0 -th element of v exists, thus
avoiding a second test. The type safety of λH (Theorem 4.6) guarantees that
implementations of sel need not check the subscript at runtime. Since the proof
t2 is ignored in the “else” branch, ltPrf t0 t is defined to reduce to the trivial proofof True when the value of i0 is not less than that of n.
The usual vector type, which keeps the length packaged with the content, is
vector : Ω → Ω
vector = λt : Ω. ∃t0 : Nat. snat t0 × vec t0 t
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

23

Now we can write a wrapper function for sumVec operating on packaged vectors.
sumVector : vector nat → nat≡ λv : vector nat.
open v as ht0 , v0 i in sumVec[t0 ] (sel[ltPrf b0b2](v0 , 0)) (sel[ltPrf b1b2](v0 , 1))

Next we show the type term ltPrf which generates the proof of the proposition
LTOrTrue t0 t (lt t0 t). We first present a Church encoding of the kind term LT and
its “constructors” ltzs and ltss.
LT : Nat → Nat → Kind
LT = λt : Nat. λt0 : Nat.
ΠR : Nat → Nat → Kind.
(Πt : Nat. R zero (succ t)) →(Πt : Nat. Πt0 : Nat. R t t0 → R (succ t) (succ t0 )) →R t t0ltzs : Πt : Nat. LT zero (succ t)
ltzs = λt : Nat. λR : Nat → Nat → Kind.
λz : (Πt : Nat. R zero (succ t)).
λs : (Πt : Nat. Πt0 : Nat. R t t0 → R (succ t) (succ t0 )).

zt
ltss : Πt : Nat. Πt0 : Nat. LT t t0 → LT (succ t) (succ t0 )ltss = λt : Nat. λt0 : Nat. λp : LT t t0 . λR : Nat → Nat → Kind.
λz : (Πt : Nat. R zero (succ t)).
λs : (Πt : Nat. Πt0 : Nat. R t t0 → R (succ t) (succ t0 )).

s t t0 (p R z s)
Next we define dependent conditionals on kinds Nat and Bool.
dep ifez : Πt : Nat. Πk : Nat → Kind. k zero → (Πt0 : Nat. k (succ t0 )) → k t
dep ifez zero= λk : Nat → Kind. λt1 : k zero. λt2 : (Πt0 : Nat. k (succ t0 )). t1
dep ifez (succ t) = λk : Nat → Kind. λt1 : k zero. λt2 : (Πt0 : Nat. k (succ t0 )). t2 t
dep if : Πt : Bool. Πk : Bool → Kind. k true → k false → k t
dep if true = λk : Bool → Kind. λt1 : k true. λt2 : k false. t1
dep if false = λk : Bool → Kind. λt1 : k true. λt2 : k false. t2

Note that, unlike the examples in Figure 2, the types of the branches in eachof these definitions are different: The type of the true branch of dep if isΠk : Bool → Kind. k true → k false → k true,
while that of its false branch isΠk : Bool → Kind. k true → k false → k false.
This is achieved by specifying the kind termλt : Bool. Πk : Bool → Kind. k true → k false → k t
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

24·

Z. Shao et al.

as the second parameter of the Elim construct for which the sugared definitionof dep if above stands. The resulting elimination term is type-correct because
the type of each branch is obtained by applying this kind term to the corresponding constructor of Bool.
Finally, we define some abbreviations, and then the proof generator itself.
LTcond : Nat → Nat → Kind
LTcond = λt0 : Nat. λt : Nat. LTOrTrue t0 t (lt t0 t)
LTsucc : Nat → Nat → Bool → Kind
LTsucc = λt0 : Nat. λt : Nat. λt00 : Bool.
LTOrTrue t0 t t00 → LTOrTrue (succ t0 ) (succ t) t00

ltPrf : Πt0 : Nat. Πt : Nat. LTcond t0 t
ltPrf = λt0 : Nat.
Elim[Nat, λt01 : Nat. Πt1 : Nat. LTcond t01 t1 ](t0 ){λt1 : Nat. dep ifez t1 (LTcond zero) id ltzs;
λt01 : Nat. λtP : (Πt1 : Nat. LTcond t01 t1 ). λt1 : Nat.
dep ifez

t1(LTcond (succ t01 ))id(λt1 : Nat. dep if (lt t01 t1 ) (LTsucc t01 t1 ) (ltss t01 t1 ) (id True) (tP t1 ))}4.4 Example: Type conversions
The language λH offers only the bare minimum of constructs for programmingwith TL types. However the reader may recall that λH is an intermediate language, and ease of programming in it is not necessarily of high importance.
Much more important is that it has the flexibility to express the more complex
relationships between terms and types in other languages, to do this in termsof simple constructs, which are relatively simple to reason about and transform, and do it at no run-time cost. To a large extent this flexibility comesfrom the use of type-level proof terms in λH .
One example of the power of programming with proof terms is the ability
to use λH in a way which allows more general type conversions than thosepermitted by rule E- CONV. This rule allows the conversion of a term’s type only
to other βηι-equivalent types, but not to types which are provably equivalent insome weaker sense. For instance it is impossible to convert a λH -term of typevec (plus t1 t2 ) nat to a term of type vec (plus t2 t1 ) nat in a context where thedistinct type variables t1 and t2 have kind Nat, because the type terms plus t1 t2
and plus t2 t1 , being different normal forms, are not βηι-equivalent.
A solution is to instead define and use types which represent equivalenceclasses with respect to a relation of interest, in this case raw datatypes of λ H
packaged together with proof terms of type equivalence. When a parameterof a type constructor must be subjected to conversions in our program, we
can replace it by a derived type constructor which hides the actual “value”
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

25of this parameter, and exposes only an equivalent value, with a proof of theirequivalence hidden in the package. Thus the singleton integer type snat(A) canbe replaced by the type snatp(A), defined as follows:
snatp : Nat → Ω
snatp = λt0 : Nat. ∃t : Nat. ∃ P : Eq Nat t0 t. snat(t)In a package of type snatp(A) the variable P is bound to a proof of the equality
between A and the witness type bound to t, which represents the actual valueof the term-level integer component. As we will show shortly, this allows toeasily convert a term of type snatp(A) to type snatp(A0 ) when A and A0 represent
natural numbers provably equal in the given context. The kind of equality
proofs Eq can be defined in C IC following Paulin-Mohring [1993] as
Eq : Πk : Kind. k → k → Kind
Eq = λk : Kind. λt : k. Ind(k 0 : k → Kind){k 0 t}
refl : Πk : Kind. Πt : k. Eq k t trefl = λk : Kind. λt : k. Ctor (1, Eq k t)

and its elimination allows us to define a type term showing this is actually
Leibniz equality:
Leibniz : Πk : Kind. Πt : k. Πt0 : k. Eq k t t0 → ΠP : k → Kind. P t → P t0

By this definition of equality, the normal form of a term representing a proofof equality between closed types A and A0 is an application of the constructor
refl, whose kind ensures that the types are βηι-equivalent. The expressivenesscomes from the possibility to construct proofs of equality using case analysis
with dependent elimination to relate different normal forms. Consider thefollowing example. Proving that zero is a left unit of plus is trivial:
leftUnit : Πt : Nat. Eq Nat t (plus zero t)
leftUnit = refl Nat

because according to our definition of plus we have plus zero t  t. Not so with
proving that zero is a right unit of plus: The type term plus t zero is in normal
form (assuming plus stands for the elimination term of TL defined in userfriendly form in Figure 2), not convertible to t. However it is possible to encode
an inductive proof, using dependent elimination on Nat:rightUnit : Πt : Nat. Eq Nat t (plus t zero)rightUnit zero= refl Nat zerorightUnit (succ t) = eqf Nat Nat succ t (plus t zero) (rightUnit t)

where
eqf : Πk : Kind. Πk 0 : Kind. Πf : k → k 0 . Πt : k. Πt0 : k. Eq k t t0 → Eq k 0 (f t) (f t0 )eqf = λk : Kind. λk 0 : Kind. λf : k → k 0 . λt : k. λt0 : k. λp : Eq k t t0 .
Leibniz k t t0 p (λt00 : k. Eq k 0 (f t) (f t00 )) (refl k 0 (f t))

The type term eqf constructs a proof of equality between the results of two applications of a function, given a proof of equality between the arguments. In
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

26·

Z. Shao et al.

rightUnit it is employed to obtain from the inductive hypothesis (with proof represented by rightUnit t) a proof of Eq Nat (succ t) (succ (plus t zero)), which by thedefinition of plus is βηι-equivalent to the goal Eq Nat (succ t) (plus (succ t) zero).
The dependency between the parameter of rightUnit and the types of the righthand side branches must be specified using λt : Nat. Eq Nat t (plus t zero) as thesecond parameter of the Elim term in the unsugared TL definition of rightUnit;
the type of the zero branch is βηι-equivalent to Eq Nat zero (plus zero zero), andthat of the succ branch with parameter t is Eq Nat (succ t) (plus (succ t) zero).

Returning to type conversions in λH , suppose now that we have a vector oflength plus t1 t2 , while a function we want to apply to it expects a vector oflength plus t2 t1 . Let us define the proof-augmented version of the vector typeas follows.
vecp : Nat → Ω → Ω
vecp = λt0 : Nat. λt1 : Ω. ∃t : Nat. ∃ P : Eq Nat t0 t. vec t t1

The “old” vectors can be trivially converted to the new type by giving them thesame size they had: If v1 has type vec A B, thenht = A, hP = refl Nat A, v1 : vec A Bi
: ∃ P : Eq Nat A t. vec t Bi
has type vecp A B. Selection from these vectors can be performed for the sameindex expressions as for the corresponding “old” vectors—constructing a proofof LT A0 t from proofs of LT A0 A and Eq Nat A t is straightforward. Conversionof the type of some term v from vecp (plus t1 t2 ) nat to vecp (plus t2 t1 ) nat is performed by the expression
open v as ht, v0 i in open v0 as hP, v00 i in

ht = t,hP = eqTrans Nat (plus t2 t1 ) (plus t1 t2 ) t (plusSym t2 t1 ) P,
v00 : vec t nati
: ∃ P : Eq Nat (plus t2 t1 ) t. vec t nati
where eqTrans is a proof of the transitivity of equality
eqTrans : Πk : Kind. Πt : k. Πt0 : k. Πt00 : k. Eq k t t0 → Eq k t0 t00 → Eq k t t00
eqTrans = λk : Kind. λt : k. λt0 : k. λt00 : k. λp : Eq k t t0 .
λp0 : Eq k t0 t00 . Leibniz k t0 t00 p0 (Eq k t) p

and plusSym is a proof of the symmetry of plus (using the lemma succPlus provingthat ∀n, m ∈ N. (n + m) + 1 = n + (m + 1)):
plusSym : Πt : Nat. Πt0 : Nat. Eq Nat (plus t t0 ) (plus t0 t)
plusSym zero
= rightUnit
plusSym (succ t) = λt0 : Nat. eqTrans Nat(plus (succ t) t0 )(succ (plus t0 t))(plus t0 (succ t))(eqf Nat Nat succ (plus t t0 ) (plus t0 t) (plusSym t t0 ))(succPlus t0 t)
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

27

succPlus : Πt : Nat. Πt0 : Nat. Eq Nat (succ (plus t t0 )) (plus t (succ t0 ))succPlus zero
= λt0 : Nat. refl Nat (succ t0 )succPlus (succ t) = λt0 : Nat. eqf Nat Nat succ
(succ (plus t t0 ))(plus t (succ t0 ))(succPlus t t0 )Similar proof terms can be found, among many other, in standard proof libraries (e.g., that of Coq [Huet et al. 2000]).
Due to the explicit use of proof terms, this technique for support of type conversions can also exploit equivalences which are valid only locally, for instancein a branch of a term-level conditional. To simplify the following example, let
us extend the computation language with a comparison for equality between
natural numbers with the obvious semantics.1 In the following example, two
vectors of unrelated (in general) sizes can be converted to the same type if they
are dynamically determined to have the same size.
Λt : Nat. λn : snat(t). λv : vecp t nat.
Λt0 : Nat. λn0 : snat(t0 ). λv0 : vecp t0 nat.
if [EqOrTrue t t0 , eqPrf t t0 ](n = n0 ,P. . . . open v0 as ht1 , xi in open x as hP1 , yi in
ht2 = t1 , hP2 = eqTrans Nat t t0 t1 P P1 , y : vec t1 nati, . . .
: ∃ P2 : Eq Nat t t2 . vec t2 nati
. ...)
where EqOrTrue and eqPrf are the analogues of LTOrTrue and ltPrf from Section 4.3.
The proof of Eq Nat t t2 , bound to P2 , is constructed by transitivity from theproof of Eq Nat t t0 , bound to P by the conditional, and the proof of Eq Nat t0 t2 ,extracted from the package v0 and bound to P1 . As a result the type of the open
term, which is a repackaged v0 , is vecp t nat—the type of v.
Notice that all terms involved in the type conversions have no computational
overhead and will be eliminated under type-erasure semantics; we emphasized
this fact in the examples by placing the conversions inline.
As with the kind term LT, strictly speaking TL does not allow the above definition of Eq, but its Church encoding has the same properties for our purposes,
since we do not need dependent or large elimination of equality proof terms forthe proof compositions shown here. The Church encoding of the equality kind,its “constructor,” and its elimination are as follows.
= λk : Kind. λt : k. λt0 : k. ΠP : k → Kind. P t → P t0refl
= λk : Kind. λt : k. λP : k → Kind. λp : P t. p
Leibniz = λk : Kind. λt : k. λt0 : k. λp : Eq k t t0 . p
Eq

1 Comparison for equality can be derived from the less-than comparison of λ ; we will also need aHstraightforward to define proof term for Πt : Nat. Πt0 : Nat. Not (LT t t0 ) → Not (LT t0 t) → Eq Nat t t0 orequivalent.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

28·

Z. Shao et al.

Clearly there are opportunities to generalize this style to weaker relations ofequivalence, which reveal partial information about the hidden type parameters. We will not explore this topic here.
4.5 Type safety
The type safety of λH is a corollary of its properties of progress and subject reduction. A pivoting element in proving progress (Lemma 4.3) is the connection
between the existence of a proof (type) term of kind LT mb nb, provided by rule
E- SEL, and the existence of a (metalogical) proof of the side condition m < n,required by rule R- SEL. Similarly, subject reduction (Lemma 4.5) in the casesof R- ADD and R- LT-T/F relies on the adequate representation of addition andcomparison by plus and lt.
Lemma 4.1 (Adequacy of the TL representation of arithmetic)\(1) For all m, n ∈ N, plus mb nb =βηι m+n.
(2) For all m, n ∈ N, lt mb nb =βηι true if and only if m < n.
(3) For all m, n ∈ N, m < n if and only if there exists a type A such that
· ` A : LT mb nb.
Proof sketch

1: By induction on m and inspection of the definition of plus.
2: By induction on m and the definition of le (Figure 2); for the forward direction the auxiliary inductive hypothesis is that for all n, if le mb nb, thenm ≤ n.
3: For the forward direction it suffices to observe that the structure of themetalogical proof of m < n (in terms of the above axioms of ordering) canbe directly reflected in a type term of kind LT mb nb. The inverse direction
is shown by examining the structure of closed type terms of this kind innormal form.
We also need a guarantee that the equivalence of constructor applications
implies the equivalence of the constructors and their arguments.
~ =βηι Ctor (i0 , I 0 ) A~ 0 , then i = i0 , I =βηι I 0 , andLemma 4.2 If Ctor (i, I) A
~ =βηι A~0.
A
Proof sketch A corollary of the confluence of TL (Theorem 3.3).
Lemma 4.3 (Progress) If ·;· ` e : A, then either e is a value, or there exists
e0 such that e 7→ e0 .
Proof sketch By standard techniques [Wright and Felleisen 1994] using induction on the typing derivation for e. Due to the transitivity of =βηι any
derivation of ∆; Γ ` e : A can be converted to a standard form in which there
is an application of rule E- CONV at its root, whose first premise ends with an
instance of a rule other than E- CONV, all of whose term derivation premises
are in standard form.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

29

The interesting case is that of the dependently typed sel construct.
If e = sel[A0 ](v, v 0 ), by inspection of the typing rules the derivation of ·;· ` e : A
in standard form must have an instance of rule E- SEL in the premise of its
root. Hence the subderivation for v must assign to it a tuple type, and thewhole derivation has the formE
D0·;· ` v : tup A2 A·;· ` v : snat A1 · ` A0 : LT A1 A2·;· ` sel[A0 ](v, v 0 ) : A00 A1·;· ` sel[A0 ](v, v 0 ) : A
D

00

0

where A =βηι A00 A1 . By inspection of the typing rules, rules other than ECONV assign to all values types which are applications of constructors of Ω.
Since the derivation D is in standard form, it ends with an E- CONV, in thepremise of which another rule assigns v a type βηι-equivalent to tup A2 A00 .
Then by Lemma 4.2 this type must be an application of tup, and again by inspection the only rule which applies is E- TUP, which implies v = hv0 , . . . vn−1 i,and the derivation D must have the form∀i < nDi·;· ` vi : A001 bi·;· ` hv0 , . . . vn−1 i : tup nb A001

Also by Lemma 4.2 A2 =βηι nb. Similarly the only rule assigning to a value
a type convertible to that in the conclusion of D 0 is E- NAT, hence A1 =βηι mbfor some m ∈ N, and v 0 = m. Then, by adequacy of LT (Lemma 4.1(3)), theconclusion of E implies that m < n. Hence by rule R- SEL e 7→ vm .
The other cases are straightforward; as a representative, consider e = e 1 e2 .
If e1 is not a value, then by inductive hypothesis e1 7→ e01 , therefore e1 = E1 {e11 }and e01 = E1 {e011 } for some evaluation context E1 and redex e11 such that e11 ,→e011 ; then e 7→ E{e011 }, where E = E1 e2 . The subcase when e1 is a value, but e2
is not, is similar. If both e1 and e2 are values, then the typing derivation for eends with an instance of rule E- CONV applied to a derivation with an instanceof E- APP at its root, where a derivation for e1 is in the premise for the subtermwith an arrow type. Reasoning as in the case for sel above, since e1 is a value
and only rules E- FUN and E- FIX (again excluding E- CONV due to the standard
form of the derivation) assign an arrow type to a value, we have that e1 mustbe either an abstraction or a fixpoint (of an arrow type). Then e reduces by rule
R-β or R- FIX, respectively, with the empty evaluation context.
A standard type substitution lemma is used in the proof of Subject Reduction
for the cases of redexes with type-level parameters.
Lemma 4.4 (Type substitution) If ∆, X : B; Γ ` e : A0 and ∆ ` A : B, then∆; [A/X]Γ ` [A/X]e : [A/X]A0 .
Proof sketch By induction on the typing derivation for e.
Lemma 4.5 (Subject Reduction) If ·;· ` e : A and e 7→ e0 , then ·;· ` e0 : A.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

30·

Z. Shao et al.

Proof sketch Since evaluation contexts bind no variables, it suffices to prove
subject reduction for ,→ and use a standard term substitution lemma. We show
only some cases of redexes involving sel and if.
—The derivation for e = sel[A0 ](hv0 , . . . vn−1 i, m) in standard form has theshape∀i < nDi·;· ` vi : A001 bi
D000·;· ` h~v i : tup nb A1·;· ` m : snat mb
E00·;· ` h~v i : tup A2 A·;· ` m : snat A1 · ` A0 : LT A1 A2·;· ` sel[A0 ](hv0 , . . . vn−1 i, m) : A00 A1·;· ` sel[A0 ](hv0 , . . . vn−1 i, m) : A

where A =βηι A00 A1 , A001 =βηι A00 , and A1 =βηι m.
b Since e 7→ e0 only by rule0
R- SEL, we have m < n and e = vm , so from Dm and A001 mb =βηι A00 m
b =βηι00
0
A A1 =βηι A we obtain a derivation of ·;· ` e : A.
—In the case of if the standard derivation D of·;· ` if [B, A0 ](tt, X1 . e1 , X2 . e2 ) : A
ends with an instance of E- CONV, preceded by an instance of E- IF. Using thenotation from Figure 5, from the premises of this rule it follows that we havea derivation E of · ` A0 : B A00 , and A00 =βηι true (since rule E- TRUE assigns
sbool true to tt), hence we have · ` A0 : B true by CONV. By Lemma 4.4 fromE and the derivation of X1 : B true; · ` e1 : A (provided as another premise),since X1 is not free in A (ensured by the premise · ` A : Ω) we obtain aderivation of ·;· ` [A0 /X1 ]e1 : A.
Theorem 4.6 (Safety of λH ) If ·;· ` e : A, then either e 7→∗ v and ·;· ` v : A,or e diverges (i.e., for each e0 , if e 7→∗ e0 , then there exists e00 such that e0 7→ e00 ).
Proof sketch Follows from Lemmas 4.3 and 4.5.
4.6 Discussion
The proof of Progress of λH relies critically on the adequacy of the representation of meta-proofs of natural numbers being in the less-than relation, thatis, that for closed A and B the kind LT A B is inhabited if and only if A and B
represent natural numbers related by less-than. In the case of the less-thanrelation and LT this fact was proved in Lemma 4.1. However, it must be kept inmind when considering extensions of λH that since C IC and TL are more expressive than higher-order predicate logic, adequacy of the representations ofmeta-proofs does not hold in general, hence the existence of a term of the kindof the proposition does not imply that there is a meta-proof of the proposition.
For instance the ability to eliminate inductive kinds in TL allows analysis of
proof derivations—a technique which allows the construction of proof terms
without counterpart in standard meta-reasoning. This issue does not arise forfirst-order proof representations (whose constructors have no parameters of afunction kind) such as LT, and we do not expect it to be a concern in practice.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

31

In cases when it does arise, it could be resolved by using the underlying consistent logic of C IC in place of the meta-logic; for instance in our presentation
the question of adequacy is raised because the operational semantics of λH isdefined in meta-logical terms, but this question would be moot if λH and its
semantics were defined as C IC terms. To eliminate the interaction with themeta-logic, this approach should be applied all the way down to the hardware
specification (as done in some PCC system [Appel and Felty 2000]); we plan topursue this in the future.
The language λH is intended only as an illustration of the expressivenessof type systems based on TL. As we showed in Section 4.4, type conversions
can be programmed in λH ; however, it is also easy to extend λH with a typeconversion construct cast, which allows conversion between any types which
the programmer can prove are in a given relation of equivalence. The strongest
such equivalence relation in TL is represented by Eq, and in this case thetyping rule for cast is∆; Γ ` e : A∆ ` B : Eq Ω A A0∆; Γ ` cast[A, A0 , B ]e : A0

(E- CAST )The dynamic semantics of cast is trivial:
cast[A, A0 , B ]e ,→ e

(R- CAST )The proof of the soundness of this extension is based on the observation(following from Theorem 3.3, the Church-Rosser property of TL) that if thejudgment · ` B : Eq Ω A A0 is derivable (which is what we have in the corresponding case of the proof of Subject Reduction), then the normal form B 0
of B is an application of refl to some kind equivalent to Ω and to some type
A1 . But the kind of this application is then Eq Ω A1 A1 , while the kind of B 0
is Eq Ω A A0 , so either A = A1 , or there is an application of rule CONV in thederivation for B 0 , with a proof of A =βηι A1 in the premise, and similarly forA0 vs. A1 . Thus we can obtain a proof that A =βηι A0 , and the rest of themeta-proof is the same as for E- CONV.2
In a language equipped with this construct, the programmer provides thecompiler with proofs of correctness of type conversions, which legalizes moreconversions than in any decidable type system with a built-in notion of conversion. Reusing definitions from Section 4.4, the cast from snat(plus t t0 ) tosnat(plus t0 t) is
cast[ snat (plus t t0 ),snat (plus t0 t),
eqf Nat Ω snat (plus t t0 ) (plus t0 t) (plusSym t t0 )]e

2 Again, this proof of soundness goes through with either an inductive definition of Eq, as in C IC ,or with its Church encoding, since no large or dependent elimination of proof terms is used.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

32·

Z. Shao et al.

5. CPS CONVERSIONIn this section we show how to perform CPS conversion on λH while still preserving proofs represented in the type system. This stage transforms all unconditional control transfers, including function invocation and return, to function
calls and gives explicit names to all intermediate computations. In this way,evaluation order is explicit and there is no need for a control stack.
There are two interesting points in our approach to CPS conversion. First,
as we discuss in detail later in this section, arbitrary terms of the type language that appear in computation terms are not transformed. Second, thetransformation of types is encoded as a function in our type language and, as
will become apparent later in this section, this fact is important for provingthat our CPS conversion is type-correct.
We start by defining a version of λH using type-annotated terms. By f¯ andē we denote the terms without annotations. Type annotations allow us topresent the CPS transformation based on syntactic instead of typing derivations.
(exp) e ::= ēAē ::= x | n | tt | ff | f | fix x : A. f | e e0 | e[A] | hX = A, e : A0 i
| open e as hX, xi in e0 | he0 , . . . en−1 i | sel[A](e, e0 )| e aop e0 | e cop e0 | if [A, A0 ](e, X1 . e1 , X2 . e2 )(fun) f ::= f¯Af¯ ::= λx : A. e | ΛX : A. f
We call the target calculus for this phase λK , with syntax:(val) v ::= x | n | tt | ff | hX = A, v : A0 i | hv0 , . . . vn−1 i| fix x0 [X1 : A1 , . . . Xn : An ](x : A). e(exp) e ::= v[A1 , . . . An ](v 0 ) | let x = v in e | let hX, xi = open v in e
| let x = sel[A](v, v 0 ) in e | let x = v aop v 0 in e | let x = v cop v 0 in e
| if [A, A0 ](v, X1 . e1 , X2 . e2 )Expressions in λK consist of a series of let bindings followed by a function application or a conditional branch. There is only one abstraction mechanism,
fix, which combines type and value abstraction. Multiple arguments may bepassed by packing them in a tuple. We use the following syntactic sugar to
denote non-recursive function definitions and value applications in λK (here x0
is a fresh variable):
λx : A. e ≡ fix x0 [](x : A). ev v 0 ≡ v[](v 0 )ΛX1 : A1 . . . . ΛXn : An . λx : A. e ≡ fix x0 [X1 : A1 , . . . Xn : An ](x : A). e
λK shares the TL type language with λH . The types for λK all have kind ΩK
which, as in λH , is an inductive kind defined in TL. The ΩK kind has all theconstructors of Ω plus one more (func). Since functions in CPS do not return
values, the function type constructor of ΩK has a different kind:→→:Ω K → ΩK

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

33

We use the more conventional syntax A →⊥ for →→ A (i.e., the type of functions
taking a parameter of type A). As will become apparent shortly in the static semantics of λK , no value of λK has type A →⊥. The latter is used in conjunction
with the new constructor func to form the types of function values:func:Ω K → ΩK

Every function value is implicitly associated with a closure environment (for all
the free variables), so the func constructor is useful in the closure-conversion
phase (see Section 6). In the case of function values, the type parameter offunc is an element of ΩK constructed by application of →→, ∀ Kind or ∀ Kscm . The
func constructor allows us to build one closure for each polymorphic function
definition (even though it contains both type abstraction and term abstraction).
In the static semantics of λK we use two forms of judgments. As in λH , thejudgment ∆; Γ `K v : A indicates that the value v is well formed and of type
A in the type and value contexts ∆ and Γ respectively. Moreover, ∆; Γ `K e
indicates that the expression e is well formed in ∆ and Γ. In both forms of
judgments, we omit the subscript from `K when it can be deduced from thecontext.
The static semantics of λK is specified by the formation rules in Figure 6. We
omit the rules for environment formation, variables, constants, tuples, packages, and type conversion on values, which are the same as in λH , and wegive only one example for arithmetic and comparison operators. Except for therules K- FIX and K- APP, which must take into account the presence of func, thestatic semantics for λK is a natural consequence of the static semantics for λH .
Typed CPS conversion involves the translation of both types and computation terms. Earlier algorithms [Harper and Lillibridge 1993; Morrisett et al.
1998] require traversing and transforming every term in the type language(which would include all the proofs in our setting). This is impractical because
proofs are large in size, and transforming them can alter their meanings andbreak the sharing among different intermediate languages.
To see the actual problem, let us convert the λH expression hX = A, e : Bi
to CPS, assuming that it has type ∃X : A0 . B. We use Ktyp to denote the metalevel translation function for the type language and Kexp for the computation
language. Under previous algorithms, the translation also transforms the witness A:
Kexp [[hX = A, e : Bi]] =λk : Ktyp [[∃X : A0 . B ]]. Kexp [[e]] (λx : Ktyp [[[A/X]B ]]. k hX = Ktyp [[A]], x : Ktyp [[B ]]i)
Here we CPS-convert e and apply it to a continuation, which puts the resultof its evaluation in a package and hands it to the return continuation k. With
proper definition of Ktyp and assuming that Ktyp [[X ]] = X on all variables X,
we can show that the two types Ktyp [[[A/X]B ]] and [Ktyp [[A]]/X](Ktyp [[B ]]) areequivalent (under =βηι ). Thus the translation preserves typing.
But we do not want to touch the witness A, so the translation function should
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

34·

Z. Shao et al.

for all i ∈ {1 . . . n}
∆ ` A i : si∆, X1 : A1 . . . , Xn : An ` A : Ω∆, X1 : A1 . . . , Xn : An ; Γ, x0 : A0 , x : A ` e∆; Γ ` fix x0 [X1 : A1 , . . . Xn : An ](x : A). e : A0
whereA0 = func (∀s1 X1 : A1 . . . . ∀sn Xn : An . A →⊥)for all i ∈ {1 . . . n}
∆ ` A i : Bi∆; Γ ` v 0 : func (∀s1 X1 : B1 . . . . ∀sn Xn : Bn . A →⊥)∆; Γ ` v : [A1/X1 ] . . . [An/Xn ]A(K- FIX )(K- APP )∆; Γ ` v 0 [A1 , . . . An ](v)∆; Γ ` v : A∆; Γ, x : A ` e∆; Γ ` let x = v in e∆; Γ ` v : tup A00 B∆; Γ ` v 0 : snat A0∆; Γ `∆; Γ ` v : ∃s Y : B. A

∆ ` A : LT A0 A00∆, X : B; Γ, x : [X/Y ]A ` e∆; Γ ` v 0 : snat A0∆; Γ `∆; Γ `

X∈/∆
s 6= Ext∆; Γ, x : snat (plus A A0 ) ` e

let x = v + v 0 in e∆; Γ ` v 0 : snat A0∆; Γ ` v : snat A∆; Γ, x : B A0 ` e

let x = sel[A](v, v 0 ) in e∆; Γ ` let hX, xi = open v in e∆; Γ ` v : snat A(K- VAL )∆; Γ, x : sbool (lt A A0 ) ` e

let x = v < v 0 in e

∆ ` B : Bool → Kind
∆ ` A : B A0∆; Γ ` v : sbool A0∆, X1 : B true; Γ ` e1∆, X2 : B false; Γ ` e2

(K- SEL )(K- OPEN )(K- ADD )(K- LT )(K- IF )∆; Γ ` if [B, A](v, X1 . e1 , X2 . e2 )Fig. 6. Static semantics of λK .

be defined as follows:
Kexp [[hX = A, e : Bi]] =λk : Ktyp [[∃X : A0 . B ]]. Kexp [[e]] (λx : Ktyp [[[A/X]B ]]. k hX = A, x : Ktyp [[B ]]i)
To preserve typing, we have to make sure that the two types Ktyp [[[A/X]B ]]and [A/X](Ktyp [[B ]]) are equivalent. This seems impossible to achieve if Ktyp isdefined at the meta level.
Our solution is to internalize the definition of Ktyp in our type language. We
replace Ktyp by a type function K of kind Ω → ΩK . For readability, we use thepattern-matching syntax, but it can be easily coded using the Elim construct.
K (snat t)= snat t
K (sbool t)= sbool t
K (t1 → t2 ) = func ((K(t1 ) × Kc (t2 )) →⊥)K (tup t1 t2 ) = tup t1 (λt : Nat. K(t2 t))
K (∀∀Kind k t) = func (∀∀Kind k (λt1 : k. Kc (t t1 ) →⊥))K (∃∃Kind k t) = ∃∃Kind k (λt1 : k. K(t t1 ))K (∀∀Kscm z t) = func (∀∀Kscm z (λk : z. Kc (t k) →⊥))K (∃∃Kscm z t) = ∃∃Kscm z (λk : z. K(t k))
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries

·

35

where
Kc ≡ λt : Ω. func (K(t) →⊥).

The definition of K is in the spirit of the interp function of Crary and Weirich[1999]. However interp cannot be used in defining a similar CPS conversion,
because its domain does not cover (nor is there an injection to it from) all types
appearing in type annotations. In λH these types are in the inductive kind Ωand can be analyzed by K. We can now prove K ([A/X]B) =βηι [A/X](K (B)) by
first reducing B to its normal form B 0 . Clearly, K ([A/X]B) =βηι K ([A/X]B 0 )and [A/X](K (B 0 )) =βηι [A/X](K (B)). Finally, we can show the equivalence
K ([A/X]B 0 ) =βηι [A/X](K (B 0 )) by induction over the structure of the normal
form B 0 .
The definition of the CPS transformation for computation terms of λH tocomputation terms of λK is given in Figure 7. As an example of how CPS
conversion works, let us consider the transformation of function abstraction(λx : A. e). The result is a function value that takes as a parameter a pair xarg ,consisting of the original abstraction’s parameter x and the current continuation k. After accessing the two elements of this pair, the function value applies
the CPS conversion of the abstraction’s body to k. On the other hand, the transformation of a function application (e1 e2 ) gives a function value that takes asa parameter the current continuation k. By applying the CPS conversions of e1and e2 to appropriate continuations, this function value ultimately applies thefunction corresponding to e1 to a pair consisting of the value corresponding to
e2 and the continuation k.
The following proposition states that our CPS conversion preserves typing.
As we discussed earlier, it is important for its proof that K has been encoded asa function in TL.
Proposition 5.1 (Type Correctness of CPS Conversion)
If ·;· `H e : A, then ·;· `K Kexp [[ ēA ]] : func (Kc (A) →⊥).
Proof sketch By induction on the typing derivation for e.
6. CLOSURE CONVERSIONIn this section we address the issue of how to make closures explicit for all
the CPS terms in λK . This stage rewrites all functions so that they containno free variables. Any variables that appear free in a function value are packaged in an environment, which together with the closed code of the function
form a closure. When a function is applied, the closed code and the environment are extracted from the closure and then the closed code is called with theenvironment as an additional parameter.
Our approach to closure conversion is based on Morrisett et al. [Morrisett
et al. 1998], who adopt a type-erasure interpretation of polymorphism. We use
the same idea for existential types. As in the case of CPS conversion, there
are again two interesting points in our approach. Arbitrary terms of the typelanguage that appear in computation terms are not transformed. Moreover,
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·36

Z. Shao et al.

Kfval [[ (λx : A. eB )A→B ]]= λxarg : K(A) × Kc (B).
let x = sel[ltPrf b0b2](xarg , 0) in let k = sel[ltPrf b1b2](xarg , 1) in Kexp [[ eB ]] k
Kfval [[ (ΛX : A. f B )∀s X:A. B ]] = ΛX : A. λk : Kc (B). k (Kfval [[ f B ]])b , ttsbool true , ffsbool false
for ēA one of xA , nsnat n

Kexp [[ ēA ]]= λk : Kc (A). k (ē)

Kexp [[ f A ]]= λk : Kc (A). k (Kfval [[ f A ) ]]Kexp[[ (fix x : A. fA )A ]]= λk : Kc (A). k (fix x[](k : Kc (A)). k (Kfval [[ f A ]]))

Kexp [[ (e1 A→B e2 A )B ]]= λk : Kc (B).
Kexp [[ e1 A→B ]] (λx1 : K(A → B). Kexp [[ e2 A ]] (λx2 : K(A). x1 hx2 , ki))00Kexp [[ (e∀ s A B [A])B A ]]= λk : Kc (B A). Kexp [[ e∀ s A B ]] (λx : K(∀∀s A0 B). x[A](k))

A

n−1 A
0
Kexp [[ heA
0 , . . . en−1 i ]]= λk : Kc (A).
0
Kexp [[ eA
0 ]] (λx0 : K(A0 ).
.
..
A

Kexp [[ sel[A](e1 tup A00

n−1
Kexp [[ en−1]] (λxn−1 : K(An−1 ). k hx0 , . . . xn−1 i) . . .)B , e snat A )B A ]] = λk : K (B A0 ). K
tup A00 B ]] (λx : K(tup A00 B).
c
exp [[ e1210Kexp [[ e2 snat A ]] (λx2 : K(snat A0 ).
let x0 = sel[A](x1 , x2 ) in k x0 ))000

Kexp [[ hX = A, e[A/X]B : BiA ]] = λk : Kc (A0 ). Kexp [[ e[A/X]B ]] (λx : K([A/X]B). k hX = A, x : K(B)i)
00Kexp [[ (open e1 ∃s Y:A . B as hX, xi in e2 A )A ]] = λk : Kc (A). Kexp [[ e1 ∃s Y:A . B ]] (λx1 : K(∃s Y : A0 . B).
let hX, xi = open x1 in Kexp [[ e2 A ]] k)00Kexp [[ (e1 snat A + e2 snat A )snat (plus A A ) ]] =λk : Kc (snat (plus A A0 )). Kexp [[ e1 snat A ]] (λx1 : K(snat A).
0
Kexp [[ e2 snat A ]] (λx2 : K(snat A0 ).
0
let x = x1 + x2 in k x0 ))00Kexp [[ (e1 snat A < e2 snat A )sbool (lt A A ) ]] =λk : Kc (sbool (lt A A0 )). Kexp [[ e1 snat A ]] (λx1 : K(snat A).
0
Kexp [[ e2 snat A ]] (λx2 : K(snat A0 ).
0
let x = x1 < x2 in k x0 ))
00

0

0

0

Kexp [[ (if [B, A](esbool A , X1 . e1 A , X2 . e2 A ))A ]] =00
λk : Kc (A0 ). Kexp [[ esbool A ]] (λx : K(sbool A00 ).
00
if [B, A](x, X1 . Kexp [[ e1 A ]] k, X2 . Kexp [[ e2 A ]] k))
Fig. 7.

CPS conversion: from λH to λK .

the transformation of types is again encoded as a function in our type language
and this is crucial for proving that closure conversion is type-correct.
We call the language we use for this phase λC ; its syntax is:(val) v ::= x | n | tt | ff | fix x0 [X1 : A1 , . . . Xn : An ](x : A). e | v[A]| hv0 , . . . vn−1 i | hX = A, v : A0 i(exp) e ::= v v 0 | let x = v in e | let x = sel[A](v, v 0 ) in e | let hX, xi = open v in e
| let x = v aop v 0 in e | let x = v cop v 0 in e | if [B, A](v, X1 . e1 , X2 . e2 )λC is similar to λK , the main difference being that type application and value
application are again separate. Type applications are values in λC reflecting
the fact that they have no runtime effect in a type-erasure interpretation. We
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

37

use the same kind of types ΩK as in λK .
The main difference in the static semantics between λK and λC is that in
the latter the body of a function must not contain free type or term variables.
This is formalized in the rule C- FIX below. The rules C- TAPP and C- APP corresponding to the separate type and value application in λC are standard.
for all i < n· ` A i : si·, X1 : A1 . . . , Xn : An ` A : Ω ·, X1 : A1 . . . , Xn : An ; ·, x0 : B, x : A ` e∆; Γ ` fix x0 [X1 : A1 , . . . Xn : An ](x : A). e : B
where B = ∀s1 X1 : A1 . . . . ∀sn Xn : An . A →⊥(C- FIX )∆; Γ ` v : ∀s X : A0 . B∆ ` A : A0∆; Γ ` v[A] : [A/X]B(C- TAPP )∆; Γ ` v1 : A →⊥∆; Γ ` v2 : A∆; Γ ` v1 v2(C- APP )We define the transformation of types as a function Cl : ΩK → ΩK → ΩK , thesecond argument of which represents the type of the closure environment. As
in CPS conversion, we write Cl as a TL function so that the closure-conversion
algorithm does not have to traverse proofs represented in the type system.
Cl (snat t)= λt0 : ΩK . snat t
Cl (sbool t) = λt0 : ΩK . sbool t
Cl (t →⊥)
= λt0 : ΩK . (t0 × Cl (t) ⊥) →⊥Cl (func t)= λt0 : ΩK . ∃t1 : ΩK . (Cl (t) t1 × t1 )Cl (tup t1 t2 ) = λt0 : ΩK . tup t1 (λt00 : Nat. Cl (t2 t00 ) t0 )Cl (∀∀Kind k t) = λt0 : ΩK . ∀ Kind k (λt1 : k. Cl (t t1 ) t0 )Cl (∃∃Kind k t) = λt0 : ΩK . ∃∃Kind k (λt1 : k. Cl (t t1 ) t0 )Cl (∀∀Kscm z t) = λt0 : ΩK . ∀ Kind z (λk : z. Cl (t k) t0 )Cl (∃∃Kscm z t) = λt0 : ΩK . ∃∃Kscm z (λk : z. Cl (t k) t0 )The definition of the closure transformation for the computation terms of λ K
is given in Figure 8. To understand how closure conversion works, let us again
consider the transformations of function abstraction and function application.
The former is the heart of closure conversion and clearly the most involvedcase. A λK term of the form fix x0 [X1 : A1 , . . . Xn : An ](x : A). e is transformed to a
package hX = Aenv , hvcode [Y1 ] . . . [Ym ], venv i : AX i. The first part of this package
is the type of the closure environment Aenv . The second part is a pair consistingof the transformed function body vcode [Y1 ] . . . [Ym ] and the closure environment
venv . The closure environment is a tuple containing the values of all term
variables x0 , . . . xk−1 that are free in e. On the other hand, the transformed
function body takes as parameters: (i) all type variables Y1 , . . . Ym that are
free in e, (ii) the type parameters X1 , . . . Xn of the original function, and (iii) apair xarg containing the closure environment xenv and the term parameter xof the original function. From the transformation of function abstractions, one
immediately notices that quantification over kind schemas is required: thedefinition of A0 X uses ∀ Kscm if Ai : Kscm.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

38·

Z. Shao et al.
for v one of x, n, tt, ff

Cval [[ v ]]= v,

Cval [[ hv0 , . . . vn−1 i ]]= hCval [[ v0 ]], . . . Cval [[ vn−1 ]]i

Cval [[ hX = A, v : Bi ]]= hX = A, Cval [[ v ]] : Cl (B) ⊥i

Cval [[ fix x0 [X1 : A1 , . . . Xn : An ](x : A). e ]] = hX = Aenv , hvcode [Y1 ] . . . [Ym ], venv i : AX i
where
AX = A0 X × X
A0 X = ∀s1 X1 : A1 . . . . ∀sn Xn : An . (X × Cl (A) ⊥) →⊥
0

A0

0
B1

B0

k−1
0
{xA
, . . . xk−1
} = FV (e) − {x, x0 }0

, . . . Ym m } =FTV (fix x0 [X1 : A1 , . . . Xn : An ](x : A). e)
Aenv = Cl (tup bk (nth (A0 0 :: . . . A0 k−1 ::nil))) ⊥venv = hx0 . . . xk−1 i
0 , X :A , . . . X :A ]vcode = fix vfix [Y1 : B10 , . . . Ym : Bmnn11(xarg : Aenv × Cl (A) ⊥).
let xenv = sel[ltPrf b0b2](xarg , 0) in
let x = sel[ltPrf b1b2](xarg , 1) in
let x0 = hX = Aenv ,hvfix [Y1 ] . . . [Ym ], xenv i : AX i inlet x0 = sel[ltPrf b0bk ](xenv , 0) in . . .
let xk−1 = sel[ltPrf k[−1bk](xenv , k − 1) in
Cexp [[ e ]]{Y1

Cexp [[ v1 [A1 , . . . An ](v2 ) ]]= let hXenv , xarg i = open Cval [[ v1 ]] in
let xcode = sel[ltPrf b0b2](xarg , 0) in
let xenv = sel[ltPrf b1b2](xarg , 1) in
xcode [A1 ] . . . [An ] hxenv , Cval [[ v2 ]]i

Cexp [[ let x = v in e ]]= let x = Cval [[ v ]] in Cexp [[ e ]]Cexp[[ let x = sel[A](v, v 0 ) in e ]]= let x = sel[A](Cval [[ v ]], Cval [[ v 0 ]]) in Cexp [[ e ]]Cexp [[ let hX, xi = open v in e ]]= let hX, xi = open Cval [[ v ]] in Cexp [[ e ]]Cexp [[ let x = v1 + v2 in e ]]= let x = Cval [[ v1 ]] + Cval [[ v2 ]] in Cexp [[ e ]]Cexp [[ let x = v1 < v2 in e ]]= let x = Cval [[ v1 ]] < Cval [[ v2 ]] in Cexp [[ e ]]Cexp [[ if [B, A](v, X1 . e1 , X2 . e2 ) ]] = if [B, A](Cval [[ v ]], X1 . Cexp [[ e1 ]], X2 . Cexp [[ e2 ]])Fig. 8.

Closure conversion: from λK to λC .

Inversely, the transformation of function application opens the package andreveals the type Xenv and value xenv of the closure environment, as well as thefunction’s body xcode . It then applies the body to the actual parameters and to
xenv .
The following proposition states that our closure conversion preserves typing. As in the case of CPS conversion, the fact that Cl has been encoded as afunction in TL is important for its proof.
Proposition 6.1 (Type Correctness of Closure Conversion)
If ·;· `K v : A, then ·;· `C Cval [[v ]] : Cl (A) ⊥.
Proof sketch By induction on the typing derivation for v.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

39

7. RELATED WORK
Our type language is a variant of the calculus of constructions [Coquand andHuet 1988] extended with inductive definitions (with both small and large
elimination) [Paulin-Mohring 1993; Werner 1994]. We omitted parameterized
inductive kinds and dependent large elimination to simplify our presentation,
however, all our meta-theoretic proofs carry over to a language that includes
them. We support η-reduction in our language while the official Coq systemdoes not. The proofs for the properties of TL are adapted from Geuvers [1993]
and Werner [1994] (which in turn borrows ideas from Altenkirch [1993]); themain difference is that our language has kind-schema variables and a new
product formation rule (Ext, Kind) which are not in Werner’s system.
The Coq proof assistant provides support for extracting programs from proofs[Paulin-Mohring 1993]. It separates propositions and sets into two distinct
universes Prop and Set. We do not distinguish between them because we are
not aiming to extract programs from our proofs, instead, we are using proofs
as specifications for our computation terms.
Burstall and McKinna [1991] proposed the notion of deliverables, which isessentially the same as our notion of certified binaries. They use dependent
strong sums to model each deliverable and give its categorical semantics. Theirwork does not support programs with effects and has all the problems mentioned in Section 2.3.
Xi and Pfenning’s DML [Xi and Pfenning 1999] is the first language thatnicely combines dependent types with programs that may involve effects. Our
ideas of using singleton types and lifting the level of the proof language are directly inspired by their work. DML does not support explicit proofs in its typelanguage; any assertions (or constraints) must be resolved fully automaticallyin order to ensure decidable typechecking. As a result, DML’s assertion language only allows integer linear inequalities. Our system, on the other hand,allows arbitrary propositions and proofs. An assertion in our system can use
any integer constraints but a certified program must explicitly provide proofs
on how these constraints are satisfied. Our system is best suited for use incompiler typed intermediate languages while the DML type system is moresuitable for use in a source programming language. Another difference is thatDML does not define the Ω kind as an inductive definition so it does not support intensional type analysis [Trifonov et al. 2000] and it is unclear how it canpreserve proofs during compilation.
We have discussed the relationship between our work and those on PCC,
typed assembly languages, and intensional type analysis in Section 1. Inductive definitions subsume and generalize earlier systems on intensional typeanalysis [Harper and Morrisett 1995; Crary and Weirich 1999; Trifonov et al.
2000]; the type-analysis construct in the computation language can be eliminated using the technique proposed by Crary et al. [1998].
The work presented in this paper showed one way of having types and proofs
coexist in an intermediate language for certified binaries, that is, by embedding predicates and proofs directly into types. Another possibility, which we
did not address, is to embed types into the logic which proofs are carried out—
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

40·

Z. Shao et al.

essentially using pre- and post-conditions as in Hoare logic to express typeinvariants. Unfortunately, Hoare logic does not work well with higher-orderfunctions, for example, it is unclear how to describe an assertion that a formal parameter (of another function) has a function type (as simple as int→int).
Foundational PCC [Appel and Felty 2000] requires explicit construction of
the fixed point (using index-based semantic model) to support higher-orderfunctions—which is probably too complex for compiler intermediate languages.
Concurrently with our work, Crary and Vanderwaart [2001] recently proposed a system called LTT, which also aims at adding explicit proofs to typed
intermediate languages. LTT uses Linear LF [Cervesato and Pfenning 1996]
as its proof language. It shares some similarities with our system in that bothare using singleton types [Xi and Pfenning 1999] to circumvent the problemsof dependent types. However, since LF does not have inductive definitions andthe Elim construct, it is unclear how LTT can support intensional type analysis and type-level primitive recursive functions [Crary and Weirich 2000]. In
fact, to define Ω as an inductive kind [Trifonov et al. 2000], LTT would haveto add proof-kind variables and proof-kind polymorphism, which could significantly complicate the meta-theory of its proof language. LTT requires different
type languages for different intermediate languages; it is unclear whether it
can preserve proofs during CPS and closure conversion. The power of linear
reasoning in LTT is desirable for tracking ephemeral properties that hold only
for certain program states; we are working on adding such support into ourframework.
8. CONCLUSIONSWe presented a general framework for explicitly representing propositions andproofs in typed intermediate or assembly languages. We showed how to integrate an entire proof system into our type language and how to perform CPS
and closure conversion while still preserving proofs represented in the typesystem. Our work is a first step toward the goal of building realistic infrastructure for certified programming and certifying compilation.
Our type system is fairly concise and simple with respect to the number ofsyntactic constructs, yet it is powerful enough to express all the propositions
and proofs in the higher-order predicate logic (extended with induction principles). In the future, we would like to use our type system to express advanced
program invariants such as those involved in low-level mutable recursive data
structures.
Our type language is not designed around any particular programming language. We can use it to typecheck as many different computation languages
as we like; all we need is to define the corresponding Ω kind as an inductive
definition. We hope to evolve our framework into a realistic typed common
intermediate format.
APPENDIX
In this appendix we supply the rest of the details involved in the formalizationof our type language TL.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

41

A. FORMALIZATION OF TL
Most of our notation and definitions are directly borrowed from Werner [1994].
In addition to the symbols defined in the syntax, we will also use C to denote
general terms, Y and Z for variables, and I for inductive definitions.
To ensure that the interpretation of inductive definitions remains consistentand they can be interpreted as terms closed under their introduction rules,
we impose positivity constraints on the constructors of an inductive definition.
The positivity constraints are defined in Definitions A.1 and A.2.
Definition A.1 A term A is strictly positive in X if A is either X or ΠY : B. A0 ,where A0 is strictly positive in X, X does not occur free in B, and X 6= Y .
Definition A.2 A term C is a well-formed constructor kind for X (written
wfc X (C)) if it has one of the following forms:(1) X;(2) ΠY : B. C 0 , where Y 6= X, X is not free in B, and C 0 is a well-formed
constructor kind for X; or(3) B 0 → C 0 , where B 0 is strictly positive in X and C 0 is a well-formed
constructor kind for X.
Note that in the definition of wfc X (C) the second clause covers the case when
C is of the form B → C 0 and X does not occur free in B. Therefore, we only
allow the occurrence of X in the non-dependent case.
In the rest of this paper we often write well-formed constructor kinds for X~ : B.
~ X. We also denote terms that are strictly positive in X by ΠY~ : B.
~ X,
as ΠY~
where X is not free in B.
Definition A.3 Let C be a well-formed constructor kind for X. Then C is of~ : B.
~ X. If all the Y ’s are t’s, that is, C is of the form Π~t: B.
~ X, thenthe form ΠY
we say that C is a small constructor kind (or just a small constructor when
there is no ambiguity) and denote it as small (C).
Our inductive definitions reside in Kind, whereas a small constructor does notmake universal quantification over objects of type Kind. Therefore, an inductive
definition with small constructors is a predicative definition. While dealing
with impredicative inductive definitions, we must forbid projections on universes equal to or bigger than the one inhabited by the definition. In particular, we restrict large elimination to inductive definitions with only small
constructors.
Next, we define the set of reductions on our terms. The definition of β- andη-reduction is standard. The ι-reduction defines primitive recursion over inductive objects.
Definition A.4 Let C be a well-formed constructor kind for X and let A, B 0 ,and I be terms. We define ΦX,I,B 0 (C, A) inductively on the structure of C:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

42·

Z. Shao et al.

ΦX,I,B 0 (X, A)
0ΦX,I,B 0 (ΠY : B. C , A)

def

=

A

def

λY : B. ΦX,I,B 0 (C 0 , A Y )=~ : B.
~ X) → C 0 , A) def=
ΦX,I,B 0 ((ΠY~ : B.
~ B 0 (Z Y
~ )))~ : B.
~ I). ΦX,I,B 0 (C 0 , A Z (λYλZ : (ΠY
Definition A.5 The reduction relations on our terms are defined as:(λX : A. B) A0 ;β [A0 /X]BλX : A. (B X) ;η B, if X ∈/ FV (B)~ B}~~
Elim[I, A00 ](Ctor (i, I) A){;ι (ΦX,I,B 0 (Ci , Bi )) A~
where I = Ind(X : Kind){C}~B 0 = λY : I. (Elim[I, A00 ](Y ){B})
Recall that in Section 3.2 we introduced the relations β , η , and ι as thecontextual closures of the relations ;β , ;η , and ;ι respectively; we write ;and  for the unions of the above relations, and =βηι for the reflexive, symmetric, and transitive closure of .
~ the term A of
Let us examine the ι-reduction in detail. In Elim[I, A00 ](A){B},~ contains the set of branches of Elim,type I is being analyzed. The sequence B
one for each constructor of I. In the case when Ci = X, which implies that A isof the form Ctor (i, I), the Elim just selects the Bi branch:~ ; ι Bi
Elim[I, A00 ](Ctor (i, I)){B}~ : B.
~ X, where X does not occur free in B,~ A must be
In the case when Ci = ΠY~of the form Ctor (i, I) A, with Ai of type Bi . The Elim selects the Bi branch andpasses the constructor arguments to it. Accordingly, the reduction yields (byapplication of the meta-level function Φ):~~ B}~ ; ι Bi A
Elim[I, A00 ](Ctor (i, I) A){
The recursive case is the most interesting. For simplicity assume that the ith~ :B~ 0 . X) → ΠY~ 0 : B~00 . X. Therefore, A is of theconstructor has the form (ΠY~~ :B~ 0 . I, andform Ctor (i, I) A with A1 being the recursive component of type ΠYA2 . . . An being non-recursive. The reduction rule then yields:~ B}~ ;ι Bi A1 (λY~ :B~ 0 . Elim[I, A00 ](A1 Y~ ){B})~ A 2 . . . An
Elim[I, A00 ](Ctor (i, I) A){
The Elim construct selects the Bi branch and passes the arguments A1 ,. . ., An ,and the result of recursively processing A1 . In the general case, it would process each recursive argument.
For example, suppose the kind Nat of natural numbers is defined as
Ind(Nat : Kind){Nat; Nat → Nat},with the constructor zero defined as Ctor (1, Nat) and the constructor succ definedas Ctor (2, Nat). Consider Elim[Nat, A00 ](A){B0 ; BS }, where B0 and BS are thebranches for the zero and succ constructors. Then we have:
Elim[Nat, A00 ](Ctor (1, Nat)){B0 ; BS } ;ι B0
Elim[Nat, A00 ](Ctor (2, Nat) N ){B0 ; BS } ;ι BS N (Elim[Nat, A00 ](N ){B0 ; BS })ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries∆ ` C : Kind

· ` Kind : Kscm

( AX 1)· ` Kscm : Ext( AX 2)∆ ` A:Bt∈/ Dom(∆)( WEAK 1)k∈/ Dom(∆)( WEAK 2)∆ ` A:Bz∈/ Dom(∆)∆, z : C ` A : B( WEAK 3)∆, t : C ` A : B∆ ` C : Kscm

∆ ` A:B∆, k : C ` A : B∆ ` C : Ext∆ ` Kind : Kscm

X ∈ Dom(∆)∆, X : A ` B : B 0∆ ` ΠX : A. B 0 : s∆ ` λX : A. B : ΠX : A. B 0∆ ` A : ΠX : B 0 . A0 ∆ ` B : B 0∆ ` A B : [B/X]A0∆, X : A ` B : s2

(s1 , s2 ) ∈ R∆, X : Kind ` Ci : Kind

wfc X (Ci )~ : Kind∆ ` Ind(X : Kind){C}∆ ` I : Kind
∆ ` Ctor (i, I) : [I/X]Ci~
where I = Ind(X : Kind){C}~ : A0 A∆ ` Elim[I, A0 ](A){B}~
where I = Ind(X : Kind){C}

for all i∆ ` B0 : s( IND )

( ELIM )∆ ` A0 : Kscm
∆ ` Bi : ΨX,I (Ci , A0 )~ : A0∆ ` Elim[I, A0 ](A){B}~
where I = Ind(X : Kind){C}∆ binds no kind-schema variables∆ ` A:B( PROD )( CON )∆ ` A:I∆ ` A0 : I → Kind
for all i∆ ` Bi : ζX,I (Ci , A0 , Ctor (i, I))∆ ` A:I
small (Ci )( FUN )( APP )∆ ` ΠX : A. B : s2
for all i

43( VAR )

∆ ` X : ∆(X)

∆ ` A : s1·

∆ ` B:sB =βηι B 0∆ ` A : B0

( L - ELIM )( CONV )Fig. 9. Formation rules of TL.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

44·

Z. Shao et al.

The following two definitions introduce the meta-level functions ζ and Ψ,
which compute the types of the branches of the small and large elimination
constructs, respectively. The cases follow from the ι-reduction rule in Definition A.5.
Definition A.6 Let C be a well-formed constructor kind for X and let A, B 0 ,and I be terms. We define ζX,I (C, A, B 0 ) inductively on the structure of C:
def

ζX,I (X, A, B 0 )= A B0defζX,I (ΠY : B. C 0 , A, B 0 )= ΠY : B. ζX,I (C 0 , A, B 0 Y )def~ : B.
~ X) → C 0 , A, B 0 ) =ζX,I ((ΠY~~ I). (ΠY
~ : B.
~ (A (Z Y~ ))) → ζX,I (C 0 , A, B 0 Z)
ΠZ : (ΠY : B.
~
where X is not free in B and B.
Definition A.7 Let C be a well-formed constructor kind for X and let A andI be two terms. We define ΨX,I (C, A) inductively on the structure of C:
ΨX,I (X, A)

def

= A

def

ΨX,I (ΠY : B. C 0 , A) = ΠY : B. ΨX,I (C 0 , A)
ΨX,I (B 0 → C 0 , A)def

= [I/X]B 0 → [A/X]B 0 → ΨX,I (C 0 , A)

where X is not free in B and B 0 is strictly positive in X.
The complete typing rules for TL are listed in Figure 9. The three weakening
rules make sure that all variables are bound to the correct classes of terms in
the context. There are no separate context-formation rules; a context ∆ is wellformed if we can derive the judgment ∆ ` Kind : Kscm (notice we can only add
new variables to the context via the weakening rules).
ACKNOWLEDGMENTS

We would like to thank Thorsten Altenkirch, Gilles Barthe, Thierry Coquand,
Antony Courtney, Karl Crary, Xinyu Feng, Christopher League, Zhaohui Luo,
Christine Paulin-Mohring, Stefan Monnier, Henrik Nilsson, Walid Taha, andanonymous referees for discussions and comments on this and an earlier version of this paper. Benjamin Werner helped us understand the intricacies inthe strong-normalization proof for the core calculus of inductive constructions.
REFERENCES
A LTENKIRCH , T. 1993. Constructions, inductive types and strong normalization. Ph.D. thesis,
University of Edinburgh, UK.
A PPEL , A. W. AND F ELTEN, E. W. 2001. Models for security policies in proof-carrying code. Tech.
Rep. CS-TR-636-01, Princeton Univ., Dept. of Computer Science. March.
A PPEL , A. W. AND F ELTY, A. P. 2000. A semantic model of types and machine instructions for
proof-carrying code. In Proc. 27th ACM Symp. on Principles of Prog. Lang. ACM Press, 243–253.
B ARENDREGT, H. P. 1991. Lambda calculi with types. In Handbook of Logic in Computer Science(volume 2), S. Abramsky, D. Gabbay, and T. Maibaum, Eds. Oxford Univ. Press.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

A Type System for Certified Binaries·

45

B ARENDREGT, H. P. AND G EUVERS , H. 1999. Proof-assistants using dependent type systems. In
Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier Sci. Pub. B.V.
B ARTHE , G., H ATCLIFF , J., AND S ORENSEN, M. 1999. CPS translations and applications: thecube and beyond. Higher Order and Symbolic Computation 12, 2 (September), 125–170.
B URSTALL , R. AND M C K INNA , J. 1991. Deliverables: an approach to program development inconstructions. Tech. Rep. ECS-LFCS-91-133, Univ. of Edinburgh, UK.
C ERVESATO , I. AND P FENNING , F. 1996. A linear logical framework. In Proc. 11th IEEE Symp.
on Logic in Computer Science. 264–275.
C OLBY, C., L EE , P., N ECULA , G. C., B LAU, F., P LESKO , M., AND C LINE , K. 2000. A certifying
compiler for Java. In Proc. 2000 ACM Conf. on Prog. Lang. Design and Impl. ACM Press, New
York, 95–107.
C ONSTABLE , R. 1985. Constructive mathematics as a programming logic I: Some principles oftheory. Ann. of Discrete Mathematics 24.
C OQUAND , T. AND H UET, G. 1988. The calculus of constructions. Information and Computation 76, 95–120.
C RARY, K. AND VANDERWAART, J. 2001. An expressive, scalable type theory for certified code.
Tech. Rep. CMU-CS-01-113, School of Computer Science, Carnegie Mellon Univ., Pittsburgh,
PA. May.
C RARY, K., WALKER , D., AND M ORRISETT, G. 1999. Typed memory management in a calculus of
capabilities. In Proc. 26th ACM Symp. on Principles of Prog. Lang. ACM Press, 262–275.
C RARY, K. AND W EIRICH , S. 1999. Flexible type analysis. In Proc. 1999 ACM SIGPLAN Int’l
Conf. on Functional Prog. ACM Press, 233–248.
C RARY, K. AND W EIRICH , S. 2000. Resource bound certification. In Proc. 27th ACM Symp. on
Principles of Prog. Lang. ACM Press, 184–198.
C RARY, K., W EIRICH , S., AND M ORRISETT, G. 1998. Intensional polymorphism in type-erasuresemantics. In Proc. 1998 ACM SIGPLAN Int’l Conf. on Functional Prog. ACM Press, 301–312.
G EUVERS , H. 1993. Logics and type systems. Ph.D. thesis, Catholic University of Nijmegen, The
Netherlands.
G IRARD , J.-Y. 1972. Interprétation fonctionnelle et élimination des coupures dans l’arithmétiqued’ordre supérieur. Ph.D. thesis, University of Paris VII.
H ARPER , R. April 2000. The practice of type theory. Talk presented at 2000 Alan J. Perlis Symposium, Yale University, New Haven, CT.
H ARPER , R. AND L ILLIBRIDGE , M. 1993. Explicit polymorphism and CPS conversion. In Proc.
20th ACM Symp. on Principles of Prog. Lang. ACM Press, 206–219.
H ARPER , R. AND M ORRISETT, G. 1995. Compiling polymorphism using intensional type analysis.
In Proc. 22nd ACM Symp. on Principles of Prog. Lang. ACM Press, 130–141.
H AYASHI , S. 1991. Singleton, union and intersection types for program extraction. In Proc. International Conference on Theoretical Aspects of Computer Software, A. R. Meyer, Ed. 701–730.
H OWARD , W. A. 1980. The formulae-as-types notion of constructions. In To H.B.Curry: Essays on
Computational Logic, Lambda Calculus and Formalism. Academic Press.
H UET, G., PAULIN -M OHRING, C., ET AL . 2000. The Coq proof assistant reference manual. Part of
the Coq system version 6.3.1.
M INAMIDE , Y., M ORRISETT, G., AND H ARPER , R. 1996. Typed closure conversion. In Proc. 23rd
ACM Symp. on Principles of Prog. Lang. ACM Press, 271–283.
M ONNIER , S., S AHA , B., AND S HAO , Z. 2001. Principled scavenging. In Proc. 2001 ACM Conf. on
Prog. Lang. Design and Impl. ACM Press, New York, 81–91.
M ORRISETT, G., WALKER , D., C RARY, K., AND G LEW, N. 1998. From System F to typed assembly
language. In Proc. 25th ACM Symp. on Principles of Prog. Lang. ACM Press, 85–97.
N ECULA , G. 1997. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Prog. Lang.
ACM Press, New York, 106–119.
N ECULA , G. 1998. Compiling with proofs. Ph.D. thesis, School of Computer Science, Carnegie
Mellon Univ.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

46·

Z. Shao et al.

N ECULA , G. AND L EE , P. 1996. Safe kernel extensions without run-time checking. In Proc. 2nd
USENIX Symp. on Operating System Design and Impl. USENIX Assoc., 229–243.
N ECULA , G. AND L EE , P. 1998. The design and implementation of a certifying compiler. In Proc.
1998 ACM Conf. on Prog. Lang. Design and Impl. ACM Press, New York, 333–344.
N ORDSTROM , B., P ETERSSON, K., AND S MITH , J. 1990. Programming in Martin-Löf’s type theory.
Oxford University Press.
PAULIN -M OHRING , C. 1989. Extracting Fω ’s programs from proofs in the Calculus of Constructions. In Proc. 16th ACM Symp. on Principles of Prog. Lang. ACM Press, New York, 89–104.
PAULIN -M OHRING , C. 1993. Inductive definitions in the system Coq—rules and properties. In
Proc. TLCA, M. Bezem and J. Groote, Eds. LNCS 664, Springer-Verlag.
S HAO , Z. 1997. An overview of the FLINT/ML compiler. In Proc. 1997 ACM SIGPLAN Workshop
on Types in Compilation.
S HAO , Z., L EAGUE , C., AND M ONNIER , S. 1998. Implementing typed intermediate languages. In
Proc. 1998 ACM SIGPLAN Int’l Conf. on Functional Prog. ACM Press, 313–323.
S HAO , Z., S AHA , B., T RIFONOV, V., AND PAPASPYROU, N. 2001. A type system for certified binaries. Tech. Rep. YALEU/DCS/TR-1211, Dept. of Computer Science, Yale University, New Haven,
CT. March.
S HELDON, M. A. AND G IFFORD , D. K. 1990. Static dependent types for first class modules. In
1990 ACM Conference on Lisp and Functional Programming. ACM Press, New York, 20–29.
T RIFONOV, V., S AHA , B., AND S HAO , Z. 2000. Fully reflexive intensional type analysis. In Proc.
2000 ACM SIGPLAN Int’l Conf. on Functional Prog. ACM Press, 82–93.
WALKER , D. 2000. A type system for expressive security policies. In Proc. 27th ACM Symp. on
Principles of Prog. Lang. 254–267.
W ERNER , B. 1994. Une théorie des constructions inductives. Ph.D. thesis, A L’Université Paris 7,
Paris, France.
W RIGHT, A. K. AND F ELLEISEN, M. 1994. A syntactic approach to type soundness. Information
and Computation 115, 1, 38–94.
X I , H. AND P FENNING , F. 1999. Dependent types in practical programming. In Proc. 26th ACM
Symp. on Principles of Prog. Lang. ACM Press, 214–227.
Received January 2002; revised March 2003 and November 2003; accepted May 2004.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.