Books
- Mathematical Logic and Computation
In copyediting. To be published by Cambridge University Press.
Table of contents and preface: pdf.
Online texts:
- Theorem Proving in Lean
with Leonardo de Moura and Soonho Kong. Online: html, text: pdf.
- Theorem Proving in Lean 4
with Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. Online: html.
- Logic and Proof
with Floris van Doorn and Robert Lewis. Online: html, text: pdf.
- Mathematics in Lean
with Kevin Buzzard, Robert Lewis, and Patrick Massot (in progress). Online: html, text: pdf.
- Logic and Mechanized Reasoning
with Marijn Heule and Wojciech Nawrocki (in progress). Online: html, text: pdf.
- The Lean Reference Manual
with Leonardo de Moura, Gabriel Ebner, and Sebastian Ullrich. Online: html, text: pdf.
Edited:
- Proceedings of Interactive Theorem Proving (ITP) 2018
with Assia Mahboubi. SpringerLink.
- Proceedings of Certified Programs and Proofs (CPP) 2016
with Adam Chlipala. doi.