Scalable Certication for Typed Assembly Language

A type-based certifying compiler maps source code to ma-chine code and target-level type annotations. The target-level annotations make it possible to prove easily that the machine code is type-safe, independent of the source code or compiler. To be useful across a range of source languages and compilers, the target-language type system should provide powerful type constructors for encoding source-language and compiler invariants. Unfortunately, it is diÆcult to engineer such type systems so that annotation sizes are small and verication times are fast. In this paper, we describe our experience writing a cer-tifying compiler that targets Typed Assembly Language (TALx86) and discuss some general techniques we have used to keep annotation sizes small and verication times fast. We quantify the eectiveness of these techniques by mea-suring their eects on a sizeable application | the certify-ing compiler itself. The selective use of these techniques, which include common-subexpression elimination of types, higher-order type abbreviations, and selective reverication, can change certicate size and verication time by well over an order of magnitude.