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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Aug 30, 2015
- Source ID
- 10.1145/2887747.2804318
Entities
People
- Eric Seidel
- James Bielman
- Jamey Sharp
- John Launchbury
- Lee Pike
- Pat Hickey
- Simon Winwood
- Trevor Elliott
Organizations
- Defense Advanced Research Projects Agency
- University of California, San Diego
- Willamette University