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 on more advanced properties. In this paper, we present a general framework for explicitly representing complex predicates and proofs in typed intermediate and assembly languages. We show how to reason about certified programs that involve effects while still maintaining decidable type checking. Our work provides a foundation for the process of automatically generating certified binaries in a type-theoretic framework.

Proof-carrying code and typed assembly languages aim to minimize the trusted computing base by directly certifying the actual machine code. Unfortunately, these systems cannot get rid of the dependency on a trusted garbage collector. Indeed, constructing a provably type-safe garbage collector is one of the major open problems in the area of certifying compilation.
Building on an idea by Wang and Appel, we present a series of new techniques for writing type-safe stop-and-copy garbage collectors. We show how to use intensional type analysis to capture the contract between the mutator and the collector, and how the same method can be applied to support forwarding pointers and generations. Unlike Wang and Appel, our framework directly supports higher-order functions and is compatible with separate compilation; our collectors are written in provably type-safe languages with rigorous semantics and fully formalized soundness proofs.

Compilers for polymorphic languages can use runtime type inspection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data structures. Intensional type analysis is a type-theoretic framework for expressing and certifying such type-analyzing computations. Unfortunately, existing approaches to intensional analysis do not work on polymorphic, existential, or recursive types. This makes it impossible to code applications such as garbage collection, persistency, or marshalling which must be able to examine the type of any runtime value.
We present a typed intermediate language that supports fully reflexive intensional type analysis. By fully reflexive, we mean that type-analyzing operations are applicable to the type of any runtime value. In particular, we provide both type-level and term-level constructs for analyzing quantified types. Our system supports structural induction on quantified types, yet type-checking remains decidable. We show how to use reflexive type analysis to support type-safe marshalling.