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: Copilot is a language embedded in Haskell. So you'll need Haskell to use it. Copilot is best installed using Cabal, which automatically downloads and installs Copilot from Hackage. This is done by executing
```
> cabal install copilot
```
Tutorial: Copilot tutorial.
Examples: A lot of examples can be found in the Examples directory, included when you install Copilot.
Source code:
The "old" Copilot: for posterity, the previous version of Copilot is available here.

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
Blogging about Copilot: http://leepike.wordpress.com/ (forthcoming)
Other things I do: http://www.cs.indiana.edu/~lepike/

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