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.

• BIBTEX:
  

  @inproceedings{ivory-15,
    author    = {Trevor Elliott and
                 Lee Pike and
                 Simon Winwood and
                 Pat Hickey and
                 James Bielman and
                 Jamey Sharp and
                 Eric Seidel and
                 John Launchbury},
    title     = {Guilt Free Ivory},
    booktitle = {Haskell Symposium},
    publisher = {ACM},
    year      = {2015},
    note      = {Available at \url{https://leepike.github.io/pub_pages/ivory.html}}}

• PAPER DOWNLOAD: ivory.pdf