[Haskell-cafe] ANN: Copilot 0.22 -- A stream DSL for writing embedded C.

[Lee Pike]

Announcing Copilot 0.22:

Can you write a list in Haskell? Then you can write embedded C code using Copilot. 

Here's a Copilot program that computes the Fibonacci sequence (over Word 64s) and tests for even numbers:

fib :: Streams
fib = do
 "fib" .= [0,1] ++ var "fib" + (drop 1 $ varW64 "fib")
 "t" .= even (var "fib")
   where even :: Spec Word64 -> Spec Bool
         even w = w `mod` const 2 == const 0

Copilot contains an interpreter, a compiler, and uses a model-checker to check the correctness of your program. The compiler generates constant time and constant space C code via Tom Hawkin's Atom[1] (thanks Tom!). Copilot was originally developed to write embedded monitors for more complex systems, but it can be used to develop a variety of embedded code.

HACKAGE: http://hackage.haskell.org/package/copilot

WEBPAGE: http://leepike.github.com/Copilot/ (with more info).

PICS/VIDEO of Copilot's maiden flight: http://picasaweb.google.com/105722675808588603973

A PAPER (PDF): http://www.cs.indiana.edu/~lepike/pub_pages/rv2010.html

The Copilot Team
* Maintainer: Lee Pike (leepike at galois.com), Galois, Inc. 
* Alwyn Goodloe, National Institute of Aerospace
* Robin Morisset, École Normale Supérieure
* Sebastian Niller, Technische Universität Ilmenau

[1] http://hackage.haskell.org/package/atom