jonsterling / Coq Guarded Computational Type Theory
Stars: ✭ 18
Labels
Projects that are alternatives of or similar to Coq Guarded Computational Type Theory
Jscoq
A port of Coq to Javascript -- Run Coq in your Browser
Stars: ✭ 380 (+2011.11%)
Mutual labels: coq
Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+3677.78%)
Mutual labels: coq
Company Coq
A Coq IDE build on top of Proof General's Coq mode
Stars: ✭ 297 (+1550%)
Mutual labels: coq
Fiat Crypto
Cryptographic Primitive Code Generation by Fiat
Stars: ✭ 359 (+1894.44%)
Mutual labels: coq
Verdi
A framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+2655.56%)
Mutual labels: coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+3022.22%)
Mutual labels: coq
Practical Fm
A gently curated list of companies using verification formal methods in industry
Stars: ✭ 272 (+1411.11%)
Mutual labels: coq
Finset
A Coq library for extensional finite sets and comprehension
Stars: ✭ 6 (-66.67%)
Mutual labels: coq
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.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].