Experience Report: a Do-It-Yourself High-Assurance Compiler

• ABSTRACT:
  
  Embedded domain-specific languages (EDSLs) are an approach for quickly building new languages while maintaining the advantages of a rich metalanguage. We argue in this experience report that the "EDSL approach" can surprisingly ease the task of building a high-assurance compiler. We do not strive to build a fully formally- verified tool-chain, but take a "do-it-yourself" approach to increase our confidence in compiler-correctness without too much effort. Copilot is an EDSL developed by Galois, Inc. and the National Institute of Aerospace under contract to NASA for the purpose of runtime monitoring of flight-critical avionics. We report our experience in using type-checking, QuickCheck, and model-checking "off-the-shelf" to quickly increase confidence in our EDSL tool-chain.

• BIBTEX:
  

  @InProceedings{pike-icfp-12,
    author =    {Lee Pike and Nis Wegmann and Sebastian Niller and Alwyn Goodloe},
    title =     {Experience Report: a Do-It-Yourself High-Assurance Compiler},
    booktitle = {Proceedings of the Intl. Conference on Functional Programming (ICFP)},
    publisher = {ACM},
    year =      {2012},
    month =     {September},
    note =      {Preprint available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/icfp2012.html}},
  }
  

• PAPER DOWNLOAD: pike-icfp12.pdf

• TALK DOWNLOAD: pike-icfp12.pdf
  There is also a video of the presentation on Youtube.

• Copilot Compiler and Language: http://leepike.github.com/Copilot/.

• Erratum: Pg. 4, col. 2: In the sentence, "We also check at compile-time that streams are productive; for example, the stream definition x = x fails type-checking.", the equation 'x = x' should read 'x = local x (\_ -> x)', i.e., a let expression in the Copilot language.