-
Updated
Jun 8, 2014 - CSS
Coq
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
Here are 622 public repositories matching this topic...
Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq
-
Updated
May 26, 2016 - Coq
4th Year Honours Thesis on Programming Language Semantics
-
Updated
Jun 13, 2016 - TeX
Un ejemplo de uso de Coq y Agda para lemas triviales sobre árboles binarios.
-
Updated
Dec 4, 2016 - TeX
Certified implementation of a parametrized framework for concurrent garbage collectors
-
Updated
Dec 4, 2016 - Coq
a system that helps formally verify the correctness of concurrent programs, integrated into a toy programming language called Imp.
-
Updated
Dec 14, 2016 - Coq
The Ur/Web programming language
-
Updated
Feb 3, 2017 - Standard ML
A full-featured hierarchy of typeclasses for functional programming in Coq
-
Updated
Feb 6, 2017 - Coq
Software Foundations book and exercises taken from https://www.cis.upenn.edu/~bcpierce/sf/current/index.html
-
Updated
Feb 24, 2017 - HTML
Fun plugin to play with the Gallina AST.
-
Updated
Feb 27, 2017 - OCaml
Hoare Type Theory
-
Updated
Mar 28, 2017 - Coq
Calvin Talks Types
-
Updated
Apr 10, 2017 - TeX
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 2 months ago
- Followers
- 56 followers
- Repository
- coq/coq
- Website
- coq.inria.fr
- Wikipedia
- Wikipedia