Hitchhiker's Guide to Logical Verification (2023 Edition)

Hitchhiker's Guide to Logical Verification (2023 Edition)

by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg

lean

lean.forward

The Hitchhiker's Guide to Logical Verification is a textbook that<br>introduces the reader to interactive theorem proving using the Lean 4<br>proof assistant as its vehicle. The textbook is accompanied by Lean<br>demonstration and exercise files.

If you are an instructor and want to use the materials in your course,<br>we would be grateful if you could contact Jasmin Blanchette.

Materials

The Hitchhiker's Guide to Logical Verification (standard edition)

The Hitchhiker's Guide to Logical Verification (tablet edition)

git repository with Lean and PDF files

Further_References

Lean community (web page)

Visual Studio Code (web page)

Lean's mathematical library (git repository)

Concrete Semantics: With Isabelle/HOL (book)