Topic: coq Goto Github

👇 Here are 601 public repositories matching this topic...

absint / compcert
coq,The CompCert formally-verified C compiler
Organization: absint
Home Page: https://compcert.org
compcert coq c compiler

aeneasverif / aeneas
coq,A verification toolchain for Rust programs
Organization: aeneasverif
compiler coq deductive-reasoning formal-methods formal-verification fstar hol4 lean ocaml proofs

awesomo4000 / awesome-provable
coq,A curated set of links to formal methods involving provable code.
User: awesomo4000
formal-verification certified-programming sel4 coq isabelle isabelle-hol idris agda

certicoq / certicoq
coq,A Verified Compiler for Gallina, Written in Gallina
Organization: certicoq
coq gallina compiler formal-verification

coq-community / awesome-coq
coq,A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
Organization: coq-community
Home Page: https://coq-community.org/awesome-coq
awesome awesome-list coq resources

coq-community / coq-ext-lib
coq,A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Organization: coq-community
Home Page: https://coq-community.org/coq-ext-lib/
coq library programming coq-platform coq-ci

coq-community / fourcolor
coq,Formal proof of the Four Color Theorem [maintainer=@ybertot]
Organization: coq-community
coq ssreflect mathcomp four-color-theorem coq-ci

coq-community / math-classes
coq,A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
Organization: coq-community
Home Page: https://math-classes.github.io/
coq-library typeclasses mathematics coq coq-ci coq-platform

coq-community / vscoq
coq,A Visual Studio Code extension for Coq [maintainers=@rtetley,@maximedenes,@huynhtrankhanh,@thery,@Blaisorblade]
Organization: coq-community
coq vscode vscode-extension editor vscodium

coq-zh / sf-zh
coq,《软件基础》中译版 Software Foundations Chinese Translation
Organization: coq-zh
Home Page: https://Coq-zh.github.io/SF-zh/
coq translation chinese-translation

coq / coq
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.
Organization: coq
Home Page: https://coq.inria.fr/
proof-assistant coq theorem-proving dependent-types

coq / opam
coq,Archive for all Coq related OPAM packages organized in various repositories
Organization: coq
Home Page: https://coq.inria.fr/opam/www/
coq opam opam-repository

cpitclaudel / company-coq
coq,A Coq IDE build on top of Proof General's Coq mode
User: cpitclaudel
proof-general coq integrated-development-environment company-mode emacs proof-assistant

discus-lang / iron
coq,Coq formalizations of functional languages.
Organization: discus-lang
Home Page: iron.ouroborus.net
coq lambda-calculus theory proof coq-formalizations

egbertrijke / hott-intro
coq,An introductory course to Homotopy Type Theory
User: egbertrijke
agda hott univalence book coq formalization mathematics

ejgallego / coq-lsp
coq,Visual Studio Code Extension and Language Server Protocol for Coq
User: ejgallego
coq ide user-interface vscode-extension interactive-theorem-proving language-server-protocol

ejgallego / coq-serapi
coq,Coq Protocol Playground with Se(xp)rialization of Internal Structures.
User: ejgallego
coq serialization json sexp proof-assistant protocol machine-learning-api

formal-land / coq-of-ocaml
coq,Formal verification for OCaml
Organization: formal-land
Home Page: https://formal.land/docs/coq-of-ocaml/introduction
coq ocaml compiler

formal-land / coq-of-rust
coq,Check 100% of execution cases of Rust programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦 Formal verification
Organization: formal-land
coq formal-verification rust proof

geocoq / geocoq
coq,A formalization of geometry in Coq based on Tarski's axiom system
Organization: geocoq
formalization coq geometry tarski-axiom hilbert-axioms desargues pappus parallel-postulate euclid elements

ilya-klyuchnikov / ttlite
coq,A SuperCompiler for Martin-Löf's Type Theory
User: ilya-klyuchnikov
supercompilation programming-language dependent-types type-theory agda idris coq

ilyasergey / pnp
coq,Lecture notes for a short course on proving/programming in Coq via SSReflect.
User: ilyasergey
Home Page: https://ilyasergey.net/pnp
coq hoare-logic dependent-types tutorial ssreflect mathcomp

jasmin-lang / jasmin
coq,Language for high-assurance and high-speed cryptography
Organization: jasmin-lang
compiler language coq

jscoq / jscoq
coq,A port of Coq to Javascript -- Run Coq in your Browser
Organization: jscoq
Home Page: https://jscoq.github.io
coq proof-assistant javascript integrated-development-environment

jwiegley / category-theory
coq,An axiom-free formalization of category theory in Coq for personal study and practical work
User: jwiegley
category-theory coq monad profunctor comonads monoid profunctor-composition construction category categories

ligurio / practical-fm
coq,A gently curated list of companies using verification formal methods in industry
User: ligurio
formal-verification formal-methods tlaplus tla-specification coq software-engineering formal-verification-methods practice

logicalatomist / principia
coq,The Principia Rewrite
User: logicalatomist
Home Page: https://www.principiarewrite.com/
logic history-of-philosophy coq coq-ecosystem formal-logic formal-mathematics formal-proofs latex latex-packages

lpcic / coq-elpi
coq,Coq plugin embedding elpi
Organization: lpcic
coq metaprogramming extension-language lambda-prolog scripting

lukaszcz / coqhammer
coq,CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
User: lukaszcz
coq hammer automation proof-search theorem-prover verification dependent-types

magmide / magmide
coq,A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Organization: magmide
formal-verification formal-methods type-safety systems-programming dependent-types verification logic coq

math-comp / analysis
coq,Mathematical Components compliant Analysis Library
Organization: math-comp
coq mathcomp ssreflect analysis

math-comp / math-comp
coq,Mathematical Components
Organization: math-comp
Home Page: https://math-comp.github.io
coq ssreflect mathcomp

mattam82 / coq-equations
coq,A function definition package for Coq
User: mattam82
Home Page: http://mattam82.github.io/Coq-Equations
coq programming-language dependent-types

metacoq / metacoq
coq,Metaprogramming, verified meta-theory and implementation of Coq in Coq
Organization: metacoq
Home Page: https://metacoq.github.io
coq metaprogramming coq-formalization

mit-pdos / perennial
coq,Verifying concurrent crash-safe systems
Organization: mit-pdos
coq concurrency verification

mit-plv / kami
coq,A Platform for High-Level Parametric Hardware Specification and its Modular Verification
Organization: mit-plv
Home Page: https://plv.csail.mit.edu/kami/
coq hardware-verification bluespec proof-assistant hardware-description-language

mit-plv / koika
coq,A core language for rule-based hardware design 🦑
Organization: mit-plv
coq programming-languages formal-methods semantics hardware-description-language compilation

namin / dot
coq,formalization of the Dependent Object Types (DOT) calculus
User: namin
Home Page: http://lamp.epfl.ch/~amin/dot/
meta-theory twelf plt-redex coq dafny oop

namin / llm-verified-with-monte-carlo-tree-search
coq,LLM verified with Monte Carlo Tree Search
User: namin
Home Page: https://arxiv.org/abs/2402.08147
ai dafny llm monte-carlo-tree-search coq lean synthesis

princetonuniversity / vst
coq,Verified Software Toolchain
Organization: princetonuniversity
Home Page: https://vst.cs.princeton.edu
coq coq-vst compcert c coq-library verification proof proof-assistant formal-methods formal-verification

proofgeneral / pg
coq,This repo is the new home of Proof General
Organization: proofgeneral
Home Page: https://proofgeneral.github.io
proof-general emacs integrated-development-environment proof-assistant coq docker-coq-action

quickchick / quickchick
coq,Randomized Property-Based Testing Plugin for Coq
Organization: quickchick
testing coq

stepchowfun / proofs
coq,My personal repository of formally verified mathematics.
User: stepchowfun
coq proof-assistant formal-verification type-theory interactive-theorem-proving

tchajed / coq-tricks
coq,Tricks you wish the Coq manual told you
User: tchajed
coq

unimath / unimath
coq,This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Organization: unimath
Home Page: http://unimath.org/
coq coq-library foundations mathematics unimath

uwdb / cosette
coq,Cosette is an automated SQL solver.
Organization: uwdb
rosette coq sql database verification

uwplse / verdi
coq,A framework for formally verifying distributed systems implementations in Coq
Organization: uwplse
verdi coq coq-library proof distributed-systems

uwplse / verdi-raft
coq,An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Organization: uwplse
raft verdi coq proof distributed-systems consensus key-value

verse-lab / ceramist
coq,Verified hash-based AMQ structures in Coq
Organization: verse-lab
bloom-filter probability coq-formalization coq counting-bloom-filter quotient-filter amq

whonore / coqtail
coq,Interactive Coq Proofs in Vim
User: whonore
coq vim proof-assistant