coq-http

HTTP specification in Coq, testable and verifiable

Meta

• Author(s):
  • Yishuai Li
  • Li-yao Xia
  • Yao Li
  • Azzam Althagafi
  • Benjamin C. Pierce
• License: Mozilla Public License 2.0
• Compatible Rocq/Coq versions: 8.14 or later
• Additional dependencies:
  • OCamlbuild
  • QuickChick
  • AsyncTest
• Rocq/Coq namespace: HTTP
• Related publication(s):
  • From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server doi:10.1145/3293880.3294106
  • Model-Based Testing of Networked Applications doi:10.1145/3460319.3464798
  • Verifying an HTTP Key-Value Server with Interaction Trees and VST doi:10.4230/LIPIcs.ITP.2021.32
  • Testing by Dualization doi:20.500.14332/32046

Building and installation instructions

The easiest way to install the latest released version of coq-http is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-http

To instead build and install manually, you need to make sure that all the libraries this development depends on are installed. The easiest way to do that is still to rely on opam:

git clone https://github.com/liyishuai/coq-http.git
cd coq-http
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .
make   # or make -j <number-of-cores-on-your-machine> 
make install