Coq
215 items from coq-community/awesome-coq ★396
-
Software Foundations softwarefoundations.cis.upenn.edu
Series of Coq-based textbooks on logic, functional programming, and foundations of programming languages, aimed at being accessible to beginners.
-
Nix nixos.org
Package manager for Linux and other Unix systems, supporting atomic upgrades and rollbacks.
-
Mathematical Components math-comp.github.io
Formalization of mathematical theories, focusing in particular on group theory.
-
Formal Reasoning About Programs adam.chlipala.net
Book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
-
Menhir gallium.inria.fr
Parser generator that can output Coq code for verified parsers.
-
Gagallium gallium.inria.fr
-
Coq coq.inria.fr
-
Compcert C Compiler compcert.inria.fr
High-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors.
-
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.
- next page of items loading…
