This page is no longer being maintained. It has not been updated since March 2020. See, instead, the Formal Methods Teaching Committee web pages.

This page collects resources for anyone considering the use of formal methods and formal tools in a classroom. The effort grew out of a discussion that was held during the Big Proof program at the Isaac Newton Institute in Cambridge, UK. A recording of the discussion is available.

There are many axes along which one can organize such a list, such as the level of expertise of the intended audience (from experts to the public at large) or disciplinary orientation (computer science, mathematics, mathematical logic, etc.). Here I have chosen to classify the material by subject matter:

• computer science: material for teaching students to use formal methods for computational purposes, e.g. courses on software design and verification.

• mathematics: material for teaching mathematics, e.g. courses on discrete mathematics or introductions to mathematical proof.

• logic and formal methods: materials for teaching logic and formal methods themselves, e.g. courses on dependent type theory and automated reasoning.

If you would like add something, just send the text as you would like it to appear to avigad@cmu.edu, preferrably already formatted in markdown. Entries should provide a link to the relevant resources, which in turn should make use of formal tools (theorem provers, SAT solvers, model checkers, etc.) in some way.

The source for this page is here, based on a template by Karl Broman.

Computer Science

• Benjamin Pierce at al., Software Foundations.

  A book on designing reliable software, using Coq.

• Adam Chlipala, Certified Programming with Dependent Types

  A book about software engineering, using Coq.

• Adam Chlipala, Formal Reasoning About Programs

  The early stages of a book on formal reasoning about program correctness, using Coq.

• Tobias Nipkow and Gerwin Klein, Concrete Semantics

  A book on the semantics of programming languages, using Isabelle.

• Peter Dybjer, Types for Programs and Proofs

  A course on types systems in programming language design, using Agda.

• J. Strother Moore, A Formal Model of the Java Virtual Machine

  A course based on ACL2.

• Aaron Stump, Verified Functional Programming in Agda

  A book on writing verified programs with Agda.

• Jacques Fleuriot, Formal Verification

  A course on formal verification, using model checking, SAT, and SMT.

• Mauricio Ayala-Rincón and Flávio L. C. de Moura, Applied Logic for Computer Scientists

  A book on hardware and software verification, using PVS.

• The Summer School on Formal Techniques

  An annual summer school emphasizing hands-on use.

• Philip Wadler, Types and Semantics for Programming Languages

  A course based on Coq.

• Tobias Nipkow and Peter Lammich, Verified Functional Data Structures

  A course on the design and analysis of data structures for functional programming languages, using Isabelle. The resources are available here.

• Yves Bertot, Software Verification and Computer Proof

  An introductory course on functional programming and program verification using Coq.

• Yves Bertot, Cyril Cohen, Laurence Rideau, and Enrico Tassi, Advanced Software Verification and Computer Proof

  A course on describing mathematical concepts and algorithms using Coq and the mathematlcal Components library.

• Dafny Tutorial

  An online tutorial for the Dafny program verification system.

• Rustan Leino and colleagues, Verification Corner

  Videos on topics in verification, based on Dafny.

• Jasmin Blanchette and Alexander Bentkamp, Logical Verification

  An introduction to Lean, with applications to both computer science and mathematics.

• Jasmin Blanchette and Robert Lewis, Logic and Modelling

  A course based on Lean.

• Maria Knobelsdorf, Christiane Frede, Sebastian Böhne, and Christoph Kreitz, Theorem Provers as a Learning Tool in Theory of Computation

  A paper on using Coq to teach proof in CS.

Mathematics

• Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn, Logic and Proof

  An introduction to mathematical proof and symbolic logic, with exercises in Lean.

• Daniel Velleman, Proof Designer

  A Java applet designed to help students write proofs.

• The STACK Project

  A system for designing sophisticated computer-aided assessments in mathematics.

• Chris Sangwin, Computer Aided Assessment of Mathematics

  A book on the use of computer aided assessment.

• Patrick Massot, Introduction aux mathématiques formalisées

  An introduction to formalized mathematics, using Lean.

• Benjamin C. Pierce et al, Discrete Math in Coq

  A textbook.

• Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, and Patrick Massot, Mathematics in Lean

  An interactive textbook.

Logic and Formal Methods

• Jon Barwise and John Etchemendy, Hyperproof

  An introduction to logic, proof, and diagrammatic reasoning.

• Femke van Raamsdonk, Hermann Guevers, et al., Type Theory and Coq

  An introduction to logic, type theory, and metatheory, using Coq.

• Jacques Fleuriot, Automated Reasoning

  A course on automated reasoning, using Isabelle.

• N. Shankar, L. de Moura, H. Ruess, and A. Tiwari, Little Engines of Proof

  A course on automated deduction and decision procedures.

• Josef Urban, Chad E. Brown, and Ondřej Kunčar, Formal Mathematics and Proof Assistants

  A course using Mizar, Isabelle, and Coq.

• The AProS project

  Includes a web-based introductory course on Logic and Proof.

• Jeremy Avigad, Soonho Kong, and Leonardo de Moura, Theorem Proving in Lean.

  An introduction to dependent type theory and Lean.