Home

Welcome to the ROSCoq wiki! It assumes that you have have read the accompanying paper. Questions are very welcome. Please create an issue.

• Installation
  • Dependencies
  • Installing ROSCoq
• Tutorial
  • Specification of a robot
  • Specification of a cyber-physical system
  • Proving properties
  • Running the software agents
    • Generating Coq types for message types of the Robot Operating System
    • Providing implementation details, and extracting to Haskell
    • Compiling and running the Haskell program
• Extending ROSCoq
  • Exporting effectful Haskell functions to Coq