Awesome Open Source
Awesome Open Source

This repository was originally intended as a log of my learning of the Coq proof assistant. My interests have since grown enormously in breadth and so the document has surpassed its original scope. At this moment, I'd like this place to collect and categorise interesting and useful resources on the theory and applications of various methods of formal verification. This includes topics such as theorem proving, higher-order logic, lambda calculus, type theory, model checking, automated reasoning and so on.

During my adventures in the software verification land, I too often grieved that there was no single book or website that would concisely and eloquently describe some of the methods of the field, the software packages it employed, the jargon or connections to other fields of research. To the best of my knowledge, there is still no such book, survey article, podcast or any other resource. My vision is to fill this gap and provide a sort of signpost or handbook for readers who are new to this area and are eager to learn all of it.

I do not yet claim completeness, correctness, consistency or usefulness of any of information contained herein.


Useful resources on Coq

Coq-related blogs

Libraries and plug-ins for Coq

Applications of Coq

Papers and articles using Coq

Related languages, tools and stuff

For tools, see also page on the Coq website.

Related ACM Special Interest Groups: SIGPLAN, SIGLOG and SIGACT.

Journals and book series

( denotes open-access journals)

Meta

Conferences and workshops

See the standalone file.

Proof assistants, provers and languages

  • Lean a new theorem prover developed by Microsoft and CMU with automation support; based on CIC, supports HoTT as well
  • Matita based on (a variant of) CoC
  • Agda a (relatively) new, hip dependently-typed functional language and interactive theorem prover
  • Idris another new and hip "general purpose" language with dependent types, support for theorem proving and tactics; kind of like Coq-flavoured Haskell
  • Dedukti proof checker based on the -calculus; tools for translation from other proof assistants available
  • the PRL Project a.k.a. Nuprl
    • MetaPRL
    • JonPRL (GitHub) a reimplementation of Nuprl by Jon Sterling, Danny Gratzer and Vincent Rahli
    • Red JonPRL yet another reincarnation by Jon Sterling
  • MetaPRL
  • miniprl a minimal implementation of PRL in Standard ML
    • cha an implementation in Haskell
  • Isabelle great Archive of Formal Proofs; small trusted meta-logical core, usually used along with HOL
  • HOL by Michael Gordon et al. the original system for interactive theorem proving in higher-order logic
  • MINLOG interactive proof assistant based on first-order natural deduction calculus
  • ProofPower based on higher-order logic
  • Mizar
  • ACL2 (A Computational Logic for Applicative Common Lisp) logic for modelling systems and a complementary prover; based on first-order logic
  • Milawa theorem prover for ACL2-like logic
  • ATS (Applied Type System) dependently typed functional languge
  • E theorem prover for first-order logic
  • LEGO proof assistant
  • F7 extension of F#'s type system with refinement types, dependent types and -calculus-style concurrency
  • F* "a new higher order, effectful programming language designed with program verification in mind"
  • Eff functional language with first-class effects and native handling of all kinds of computational effects without touching monads
  • Twelf
  • Celf
  • Abella
  • Beluga
  • Delphin
  • Andromeda type theory with equality reflection
  • Prover9 and Mace4 and automated theorem prover for FOL and searcher for counterexamples, respectively
  • leanCOP tiny automated theorem prover for classical first-order logic implemented in Prolog
  • PVS
  • Guru
  • MMT language and system

See also: Every proof assistant series of lectures.

Coq
Coq is an interactive theorem prover and proof assistant based on an intensional intuitionistic type theory -- the Calculus of Inductive Constructions (CIC). It is a dependently-typed -calculus and (by the Curry-Howard isomorphism) an intuitionistic higher-order logic. It is written in OCaml.

Model checkers

SAT & SMT solvers

Other tools

Formal methods in practice

Learning resources

Courses, textbooks, papers, theses, competitions, influential figures in the field.

Type theory

Danny Gratzer's learn-tt is a fantastic resource for those interested in type and category theory. He presents all the terrific tools, textbooks, and papers that deal with both of these in a sensible and logical way, which is a quality that my repository will never have.

I'll only list here resources which he doesn't mention and which I personally find interesting.

Check out the TYPES mailing list as well.

Dependent types

Observational Type Theory

Univalent Foundations and Homotopy Type Theory

Cubical Type Theory

Copyright

Written in 20152020 by Matj Grabovsk

This work is licensed under a Creative Commons Attribution 4.0 International License.


Get A Weekly Email With Trending Projects For These Topics
No Spam. Unsubscribe easily at any time.
Coq (1,310
Handbook (1,239
Lecture Notes (577
Category Theory (276
Dependent Types (235
Formal Methods (199
Formal Verification (196
Theorem Proving (111
Scribble (17