AbelA proof of Abel-Ruffini theorem.
Stars: ✭ 26 (+85.71%)
autosubstAutomation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
Stars: ✭ 41 (+192.86%)
FrapFormal Reasoning About Programs
Stars: ✭ 465 (+3221.43%)
topologyGeneral topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Stars: ✭ 36 (+157.14%)
mcoqMutation analysis tool for Coq verification projects
Stars: ✭ 22 (+57.14%)
Category TheoryAn axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+3914.29%)
AutosubstAutomation for de Bruijn syntax and substitution in Coq
Stars: ✭ 22 (+57.14%)
Math CompMathematical Components
Stars: ✭ 344 (+2357.14%)
Practical FmA gently curated list of companies using verification formal methods in industry
Stars: ✭ 272 (+1842.86%)
fcsl-pcmPartial Commutative Monoids
Stars: ✭ 20 (+42.86%)
PuddingKCoFI Pudding: The formal proofs for the KCoFI system
Stars: ✭ 5 (-64.29%)
Set-TheoryCoq encoding of ZFC and formalization of the textbook Elements of Set Theory
Stars: ✭ 55 (+292.86%)
CoqpieCoqPIE (an IDE for the Coq theorem prover + PEDANTIC)
Stars: ✭ 8 (-42.86%)
chaparA framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Stars: ✭ 29 (+107.14%)
CosetteCosette is an automated SQL solver.
Stars: ✭ 533 (+3707.14%)
gaiaImplementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Stars: ✭ 15 (+7.14%)
Software FoundationsSolutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
Stars: ✭ 9 (-35.71%)
coq-artCoq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Stars: ✭ 57 (+307.14%)
PgThis repo is the new home of Proof General
Stars: ✭ 367 (+2521.43%)
RiscvSpecFormalThe RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.
Stars: ✭ 69 (+392.86%)
rupicolaGallina to Bedrock2 compilation toolkit
Stars: ✭ 41 (+192.86%)
Coq TricksTricks you wish the Coq manual told you
Stars: ✭ 302 (+2057.14%)
Hs To CoqConvert Haskell source code to Coq source code
Stars: ✭ 273 (+1850%)
vericertA formally verified high-level synthesis tool based on CompCert and written in Coq.
Stars: ✭ 63 (+350%)
VstVerified Software Toolchain
Stars: ✭ 264 (+1785.71%)
Cufp 2015 TutorialAn introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (-35.71%)
UnimathThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+4757.14%)
InfSeqExtA Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators
Stars: ✭ 12 (-14.29%)
Dblib LinearFormalisation of the linear lambda calculus in Coq
Stars: ✭ 10 (-28.57%)
coq-of-ocamlFormal verification of OCaml programs
Stars: ✭ 161 (+1050%)
Sf Zh《软件基础》中译版 Software Foundations Chinese Translation
Stars: ✭ 554 (+3857.14%)
finmapFinite sets, finite maps, multisets and generic sets
Stars: ✭ 45 (+221.43%)
Cpp2vFormalization of C++ for verification purposes.
Stars: ✭ 24 (+71.43%)
MtacARMtac in Agda
Stars: ✭ 29 (+107.14%)
VerdiA framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+3442.86%)
multinomialsMultinomials for the Mathematical Components library.
Stars: ✭ 12 (-14.29%)
Stalin SortAdd a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+6100%)
LibHypsA Coq library providing tactics to deal with hypothesis
Stars: ✭ 14 (+0%)
JscoqA port of Coq to Javascript -- Run Coq in your Browser
Stars: ✭ 380 (+2614.29%)
FreeSpecA framework for implementing and certifying impure computations in Coq
Stars: ✭ 48 (+242.86%)
Micro Policies CoqCoq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Stars: ✭ 18 (+28.57%)
Fiat CryptoCryptographic Primitive Code Generation by Fiat
Stars: ✭ 359 (+2464.29%)
odd-orderThe formal proof of the Odd Order Theorem
Stars: ✭ 20 (+42.86%)
MonadsCoq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-35.71%)
fm-notesUnassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (+35.71%)
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 (+25371.43%)
aleaCoq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
Stars: ✭ 20 (+42.86%)
FinsetA Coq library for extensional finite sets and comprehension
Stars: ✭ 6 (-57.14%)
Company CoqA Coq IDE build on top of Proof General's Coq mode
Stars: ✭ 297 (+2021.43%)
CoqjvmCoq executable semantics and resource verifier
Stars: ✭ 10 (-28.57%)
Hott SpeciesCombinatorial species in HoTT
Stars: ✭ 9 (-35.71%)
CrimpCertified Relational to Imperative
Stars: ✭ 5 (-64.29%)
Hott IntroAn introductory course to Homotopy Type Theory
Stars: ✭ 277 (+1878.57%)