This is the Coq formalization of Sterling and Harper's "Guarded Computational Type Theory".

Hacking

To build this Coq development, ensure that you have Coq 8.7 installed. I recommend that you install Coq in the standard way through OPAM, and my instructions are not guaranteed to work otherwise (they may work, but I have no way to double check).

opam install coq.8.7.1+1

Now, you are ready to build this development. Simply run make. To build the coqdoc (HTML rendering of the proofs), run make html.