Copilot

A (Haskell DSL) stream language for generating hard real-time C code.

---

---

Can you write a list in Haskell? Then you can write embedded C code using Copilot. Copilot is a stream language that mimics Haskell's lazy lists and generates real-time C code.

Copilot contains an interpreter, two compiler back-ends, a QuickCheck engine, and uses a model-checker to check the correctness of your programs. The compiler generates constant time and constant space C code via Tom Hawkin's Atom Language (thanks Tom!) as well as Levent Erkök's SBV language.

Diving In

• Installing: please see the project README.md.
• Tutorial: Copilot tutorial.
• Examples: A lot of examples can be found in the Examples directory, included when you install Copilot.
• Source code:
  • Main Copilot repo
  • Copilot language
  • Copilot libraries
  • Core language
  • Atom back-end
  • SBV back-end
  • CBMC interface
  • Discussion and todos

Other Resources

• Pics/videos from Copilot's maiden voyage monitoring a fault-tolerant pitot tube sensor (partly written in Atom): http://picasaweb.google.com/105722675808588603973
• Copilot on Hackage: http://hackage.haskell.org/package/copilot

Acknowledgements

We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially supported this work.

License

BSD3

The Copilot Team

• Maintainer: Lee Pike (leepike@gmail.com), Galois, Inc. Email with any questions, bugs, or cool uses!
• Alwyn Goodloe, National Institute of Aerospace
• Robin Morisset, École Normale Supérieure
• Sebastian Niller, Technische Universität Ilmenau
• Nis Wegmann, University of Cophenhagen