ROSCoq

Robots powered by Constructive Reals

This is a framework for writing and reasoning about Robotic programs in Coq. Our Coq programs are designed to actually run on robots using the Robot Operating System. https://www.youtube.com/watch?v=3cV4Qr1-I0E&feature=youtu.be
For conceptual details, please read the paper http://www.cs.cornell.edu/~aa755/ROSCoq/ROSCOQ.pdf

Also, there are slides from a talk at ITP 2015:
http://www.cs.cornell.edu/~aa755/ROSCoq/ITP.pdf
, and a shorter and more recent (11/23/2015) talk at IBM Research:
http://researcher.ibm.com/researcher/files/us-pietroferrara/anand.pdf

For instructions on installing and using ROSCoq, please visit the wiki:
https://github.com/aa755/ROSCoq/wiki
Questions are welcome; please create an issue, or ask me directly.

Updates since the ITP15 submission:

I have written a more general shim in Haskell using (my fork of) roshask:
https://github.com/aa755/roshask
One can now extract Coq programs to Haskell and then link it with the haskell shim. It should be now possible to use ROSCoq to program any robot supported by ROS.