A type-based, certifying compiler maps source code to machine code and
target-level typing 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 difficult to
engineer such type systems so that annotation sizes are small and
verification times are fast.
In this paper, we describe our experience writing a certifying
compiler that targets Typed Assembly Language (TALx86) and discuss some
general techniques we have used to keep annotation sizes small and
verification times fast. We quantify the effectiveness of these
techniques by measuring their effects on a sizeable application --
the certifying compiler itself. The selective use of these
techniques, which include common-subexpression elimination of types,
higher-order type abbreviations, and selective reverification, can
change certificate size and verification time by well over an order of
magnitude.
