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.
For tools, see also page on the Coq website.
Related ACM Special Interest Groups: SIGPLAN, SIGLOG and SIGACT.
( denotes open-access journals)
Meta
See the standalone file.
See also: Every proof assistant series of lectures.
Courses, textbooks, papers, theses, competitions, influential figures in the field.
The QED Manifesto, some more details here
VerifyThis a competition and collection of problems in formal verification of algorithms and software
Competition on Software Verification (SV-COMP)
Oregon Programming Languages Summer School video recordings of awesome lectures on type theory, provers, logic, etc.; earlier editions only have lecture notes and slides published
2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005
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
Written in 20152020 by Matj Grabovsk
This work is licensed under a Creative Commons Attribution 4.0 International License.