Coq
215 items from coq-community/awesome-coq ★396
-
Tree Sitter Rocq github.com
Partial Rocq tree-sitter grammar useful for syntax highlighting in text editors like Helix, but not recommended for full parsing of Rocq code.
-
Puiseuxth github.com
Proof of Puiseux's theorem and computation of roots of polynomials of Puiseux's series.
-
Rocqnavi github.com
Fork of coq2html that adds indexes, clickable notations, Markdown and LaTeX formatting in comments, and more.
-
Coq keyword on Zenodo zenodo.org
-
Official Coq X/Twitter x.com
-
VST vst.cs.princeton.edu
Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler.
-
Vélus velus.inria.fr
Verified compiler for a Lustre/Scade-like dataflow synchronous language.
-
Proofs and Reliable Programming using Coq team.inria.fr
Introduction to developing and verifying programs with Coq.
-
Official Coq-Club mailing list sympa.inria.fr
-
An Introduction to MathComp-Analysis staff.aist.go.jp
Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.
-
Coq tag on Stack Overflow stackoverflow.com
-
Volume 3: Verified Functional Algorithms softwarefoundations.cis.upenn.edu
Demonstration of how a variety of fundamental data structures can be specified and verified.
-
Volume 5: Verifiable C softwarefoundations.cis.upenn.edu
An extended tutorial on specifying and verifying C programs using the Verified Software Toolchain.
-
Volume 6: Separation Logic Foundations softwarefoundations.cis.upenn.edu
An introduction to separation logic and how to build program verification tools on top of it.
-
Volume 4: QuickChick softwarefoundations.cis.upenn.edu
Introduction to tools for combining randomized property-based testing with formal specification and proof.
-
Volume 2: Programming Language Foundations softwarefoundations.cis.upenn.edu
Introduction to the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
-
Volume 1: Logical Foundations softwarefoundations.cis.upenn.edu
Introduction to functional programming, basic concepts of logic, and computer-assisted theorem proving.
-
Thomas Letan's blog posts on Coq soap.coffee
-
Hybrid site.uottawa.ca
System for reasoning using higher-order abstract syntax representations of object logics.
-
PLClub Blog seas.upenn.edu
-
Nix Coq packages search.nixos.org
Collection of Coq-related packages for Nix.
-
Computer Arithmetic and Formal Proofs sciencedirect.com
Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
-
Coq subreddit reddit.com
-
Ralf Jung's blog posts on Coq ralfj.de
-
Proof General proofgeneral.github.io
Generic interface for proof assistants based on the extensible, customizable text editor Emacs.
-
Coq tag on Proof Assistants Stack Exchange proofassistants.stackexchange.com
-
Coq Exchange: ideas and experiment reports about Coq project.inria.fr
-
Poleiro: a Coq blog by Arthur Azevedo de Amorim poleiro.info
-
Paco plv.mpi-sws.org
Library for parameterized coinduction.
-
MIT PLV blog posts on Coq plv.csail.mit.edu
-
Debian Coq packages people.debian.org
Coq-related packages available in the testing distribution of Debian.
-
opam opam.ocaml.org
Flexible and Git-friendly package manager for OCaml and Coq with multiple compiler support.
-
Mike Nahas's Coq Tutorial mdnahas.github.io
Basics of using Coq to write formal proofs.
-
The Mathematical Components book math-comp.github.io
Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.
-
Learn X in Y minutes where X=Coq learnxinyminutes.com
Whirlwind tour of Coq as a language.
-
Coq'Art labri.fr
The first book dedicated to Coq.
-
Joachim Breitner's blog posts on Coq joachim-breitner.de
-
Iris iris-project.org
Higher-order concurrent separation logic framework.
-
Coq requirements in Common Criteria evaluations inria.hal.science
Guide on how to write readable and reviewable Coq code in high assurance applications.
-
Programs and Proofs ilyasergey.net
Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
-
Gregory Malecha's blog gmalecha.github.io
-
Program verification with types and logic gitlab.science.ru.nl
Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
-
Coq-std++ gitlab.mpi-sws.org
Extended alternative standard library for Coq.
-
lambda-rust gitlab.mpi-sws.org
Formal model of a Rust core language and type system, a logical relation for the type system, and safety proofs for some Rust libraries.
-
Prosa gitlab.mpi-sws.org
Definitions and proofs for real-time system schedulability analysis.
-
Gappa gitlab.inria.fr
Tactic for discharging goals about floating-point arithmetic and round-off errors.
-
Flocq gitlab.inria.fr
Formalization of floating-point numbers and computations.
-
Itauto gitlab.inria.fr
SMT-like tactics for combined propositional reasoning about function symbols, constructors, and arithmetic.
-
Coquelicot gitlab.inria.fr
Formalization of classical real analysis compatible with the standard library and focusing on usability.
-
CoqInterval gitlab.inria.fr
Tactics for performing proofs of inequalities on expressions of real numbers.
- next page of items loading…
