-
analysis Public
Forked from math-comp/analysisMathematical Components compliant Analysis Library
Coq Other UpdatedOct 12, 2021 -
-
voronoi-fortune Public
Forked from ak-fr/voronoi-fortuneFortune's algorithm described in coq
Coq UpdatedJun 1, 2021 -
cbench Public
Forked from cverified/cbenchA benchmark for C program verification
C UpdatedMar 25, 2021 -
www Public
Forked from rocq-prover/coq.github.ioSources files of the coq.inria.fr website (static part)
HTML UpdatedMar 25, 2021 -
perennial Public
Forked from mit-pdos/perennialVerifying concurrent crash-safe systems
Coq MIT License UpdatedFeb 5, 2021 -
-
-
hydra-battles Public
Forked from rocq-community/hydra-battlesVariations on Kirby & Paris' hydra battles and other funny maths (collaborative, documented, include exercises) [maintainer=@Casteran]
Coq MIT License UpdatedNov 26, 2020 -
-
HighSchoolGeometry Public
Forked from rocq-community/HighSchoolGeometryGeometry in Coq for French high school [maintainer=@thery]
Coq GNU Lesser General Public License v2.1 UpdatedSep 11, 2020 -
practical-fm Public
Forked from ligurio/practical-fmA gently curated list of companies using verification formal methods in industry
UpdatedJul 8, 2020 -
coq-function-equations Public
A case study on using Function and Equations to avoid case explosion in proofs about pattern-matching
Coq MIT License UpdatedJul 3, 2020 -
-
fsets Public
Forked from rocq-archive/fsetsFinite Sets overs Ordered Types
Coq GNU Lesser General Public License v2.1 UpdatedMay 14, 2020 -
cbench-vst Public
Forked from cverified/cbench-vstVST verification of programs from the cbench benchmark
Coq UpdatedApr 25, 2020 -
exact-real-arithmetic Public
Forked from rocq-community/exact-real-arithmeticExact Real Arithmetic [maintainers=@ybertot,@magaud]
Coq GNU Lesser General Public License v2.1 UpdatedJan 8, 2020 -
master-info Public
Forked from arnaud-m/master-infoThe website of the MSc Computer Science at UCA built upon »Feeling Responsive«, a free flexible theme for Jekyll built on Foundation framework.
JavaScript MIT License UpdatedSep 20, 2019 -
plugin_tutorials Public archive
A collection of small projects to illustrate how to write plugins for Coq
-
coind_filters Public
Coq code associated to an article published at TLCA'05 "Filters on Co-inductive Streams..."
-
improper_integrals Public
Extensions to the coquelicot library for improper integrals
Coq MIT License UpdatedApr 18, 2018 -
norm_union_example Public
A experience to describe the termination of difficult function, question from stackexchange
-
cad Public
Forked from math-comp/cadFormalizing Cylindrical Algebraic Decomposition related theories in mathcomp
Coq UpdatedAug 23, 2017 -
UniMath Public
Forked from cathlelay/UniMathThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Coq Other UpdatedJul 18, 2017 -
-
Lindemann Public
Forked from Sobernard/LindemannTheory and Lindemann theorem
Coq UpdatedJun 26, 2017 -
-
-
-
checker Public
Forked from DanGrayson/checkeran attempt at making a toy proof checker for experimental purposes
OCaml UpdatedJan 31, 2013
{{ message }}