A (Haskell DSL) stream language for generating hard real-time C
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
- 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
> cabal install copilot
- Tutorial: Copilot tutorial.
- Examples: A lot of examples can be found in
directory, included when you install Copilot.
- Source code:
- The "old" Copilot: for posterity, the previous version of Copilot is
We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National Institute of Aerospace, which partially
supported this work.
The Copilot Team
- Maintainer: Lee Pike (email@example.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