Skip to content

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

License

Notifications You must be signed in to change notification settings

mgrabovsky/fm-notes

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

  • SPIN
  • DIVINE – parallel, distributed-memory explicit-state LTL checker
  • UPPAAL
  • TLA+
  • NuSMV – symbolic model checker
  • Ultimate Automizer – model checker based on an automata approach
  • LTSmin – language-agnostic
  • PRISM – probabilistic model checker
  • MMC – explicit-state model checker for π-calculus
  • CBMC – bounded model checking
  • ESBMC – context-bounded model checking
  • Nidhugg

SAT & SMT solvers

Other tools

  • Why3 – platform for deductive reasoning on programs with support for many external provers
  • Alloy – "a language and tool for relational models"
  • Boogie – intermediate verification language
  • Q Program Verifier – collection of tools for a source–IR–IVL translation and subsequent verification
    • SMACK – bounded verification via LLVM to Boogie translation
  • Dafny – "a language and program verifier for functional correctness"
  • Vienna Verification Toolkit
  • CSeq
  • IKOS – "library designed to facilitate the development of sound static analyzers based on Abstract Interpretation"
  • Crab – "language agnostic engine to perform static analysis based on abstract interpretation"
  • Seahorn – "fully automated verification framework for LLVM-based languages"
  • rise4fun – a collection of numerous tools, i.a. for program and algorithm analysis and verification, by Microsoft Research, CMU and others that you can try right on the web page
  • Profound – "an experiment in subformula linking as an interaction method"
  • S²E – "A Platform for In-Vivo Analysis of Software Systems"
  • KLEE – symbolic execution VM
  • CPAchecker
  • Ultimate
  • K Framework
  • Lem

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 2015–2020 by Matěj Grabovský

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

Releases

No releases published

Packages

No packages published