Fork me on GitHub


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

Other Resources


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



The Copilot Team