Scalable Certification for Typed Assembly Language

13 years 11 months ago
Scalable Certification for Typed Assembly Language
Abstract. A type-based certifying compiler maps source code to machine 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 higher-level 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. Using these techniques, which include common-subexpression elimination of type...
Dan Grossman, J. Gregory Morrisett
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 2000
Where TIC
Authors Dan Grossman, J. Gregory Morrisett
Comments (0)