Guilt free ivory

Abstract

Ivory is a language that enforces memory safety and avoids most undefined behaviors while providing low-level control of memory- manipulation. Ivory is embedded in a modern variant of Haskell, as implemented by the GHC compiler. The main contributions of the paper are two-fold. First, we demonstrate how to embed the type-system of a safe-C language into the type extensions of GHC. Second, Ivory is of interest in its own right, as a powerful language for writing high-assurance embedded programs. Beyond invariants enforced by its type-system, Ivory has direct support for model-checking, theorem-proving, and property-based testing. Ivory’s semantics have been formalized and proved to guarantee memory safety.