PgThis repo is the new home of Proof General
Stars: ✭ 367 (+680.85%)
Practical FmA gently curated list of companies using verification formal methods in industry
Stars: ✭ 272 (+478.72%)
CoqpieCoqPIE (an IDE for the Coq theorem prover + PEDANTIC)
Stars: ✭ 8 (-82.98%)
CosetteCosette is an automated SQL solver.
Stars: ✭ 533 (+1034.04%)
chaparA framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Stars: ✭ 29 (-38.3%)
Software FoundationsSolutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
Stars: ✭ 9 (-80.85%)
Coq TricksTricks you wish the Coq manual told you
Stars: ✭ 302 (+542.55%)
Coq PrintfImplementation of sprintf for Coq
Stars: ✭ 15 (-68.09%)
Set-TheoryCoq encoding of ZFC and formalization of the textbook Elements of Set Theory
Stars: ✭ 55 (+17.02%)
Category TheoryAn axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+1095.74%)
gaiaImplementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (-68.09%)
CoqjvmCoq executable semantics and resource verifier
Stars: ✭ 10 (-78.72%)
FrapFormal Reasoning About Programs
Stars: ✭ 465 (+889.36%)
Profunctor MonadBidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-36.17%)
Math CompMathematical Components
Stars: ✭ 344 (+631.91%)
Hott SpeciesCombinatorial species in HoTT
Stars: ✭ 9 (-80.85%)
Hott IntroAn introductory course to Homotopy Type Theory
Stars: ✭ 277 (+489.36%)
ParsequeTotal Parser Combinators in Coq
Stars: ✭ 37 (-21.28%)
topologyGeneral topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Stars: ✭ 36 (-23.4%)
AutosubstAutomation for de Bruijn syntax and substitution in Coq
Stars: ✭ 22 (-53.19%)
AbelA proof of Abel-Ruffini theorem.
Stars: ✭ 26 (-44.68%)
Hello WorldA Hello World program in Coq.
Stars: ✭ 14 (-70.21%)
CrimpCertified Relational to Imperative
Stars: ✭ 5 (-89.36%)
UnimathThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+1346.81%)
multinomialsMultinomials for the Mathematical Components library.
Stars: ✭ 12 (-74.47%)
Stalin SortAdd a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+1746.81%)
Sf Zh《软件基础》中译版 Software Foundations Chinese Translation
Stars: ✭ 554 (+1078.72%)
NuprlincoqImplementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-34.04%)
VerdiA framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+955.32%)
Dblib LinearFormalisation of the linear lambda calculus in Coq
Stars: ✭ 10 (-78.72%)
JscoqA port of Coq to Javascript -- Run Coq in your Browser
Stars: ✭ 380 (+708.51%)
CertintA Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-17.02%)
Fiat CryptoCryptographic Primitive Code Generation by Fiat
Stars: ✭ 359 (+663.83%)
MonadsCoq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-80.85%)
CoqCoq 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.
Stars: ✭ 3,566 (+7487.23%)
HottHomotopy type theory
Stars: ✭ 946 (+1912.77%)
Company CoqA Coq IDE build on top of Proof General's Coq mode
Stars: ✭ 297 (+531.91%)
Cufp 2015 TutorialAn introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (-80.85%)
Hs To CoqConvert Haskell source code to Coq source code
Stars: ✭ 273 (+480.85%)
PornviewPorn browser formally-verified in Coq
Stars: ✭ 42 (-10.64%)
VstVerified Software Toolchain
Stars: ✭ 264 (+461.7%)
Cpp2vFormalization of C++ for verification purposes.
Stars: ✭ 24 (-48.94%)
VvclocksVerified vector clocks, with Coq!
Stars: ✭ 14 (-70.21%)
InfSeqExtA Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Stars: ✭ 12 (-74.47%)
Micro Policies CoqCoq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Stars: ✭ 18 (-61.7%)
coq-of-ocamlFormal verification of OCaml programs
Stars: ✭ 161 (+242.55%)
CompcertThe CompCert formally-verified C compiler
Stars: ✭ 984 (+1993.62%)
finmapFinite sets, finite maps, multisets and generic sets
Stars: ✭ 45 (-4.26%)
FinsetA Coq library for extensional finite sets and comprehension
Stars: ✭ 6 (-87.23%)
MtacARMtac in Agda
Stars: ✭ 29 (-38.3%)
Jt89sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-70.21%)
PoleiroA blog about Coq
Stars: ✭ 42 (-10.64%)
FreespecA framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-12.77%)
ParamcoqCoq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-31.91%)
PuddingKCoFI Pudding: The formal proofs for the KCoFI system
Stars: ✭ 5 (-89.36%)