Mathematical logic

Proofs and types

The full text of this book by Jean-Yves Girard, Yves Lafont and Paul Taylor, is now available online. Alternatively copies of the original book are available in the library.

Toposes, triples and theories

The full text of the new out of print book by Michael Barr and Charles Wells, the authors of Category theory for computing science (see below).

Category theory for computing science

Regretably the full text of this book is not available, but there is, nevertheless some useful material in the supplement available via this link, and also the solutions to the exercises.

Book of proof

An introduction to the standard methods of proving mathematical theorems. This book is now one of the recommended texts for the part 1A discrete mathematics course, and is freely avalable online.

Theorem proving in Lean

Covers the theorem proving aspect of the Lean language for the M.Phil Proof assistants module.

Mathematics in Lean

Covers using the Lean language for mathematics, as recommended for the M.Phil Proof assistants course.

Introduction to homotopy type theory

The pre-publication draft of Egbert Rijke's book which is being recommended for the M.Phil module Homotopy type theory and univalent foundations. Until the book is published in print this is the only means of accessing it.

Introduction to univalent foundations of mathematics

The full text of Martin Escardo's book which is recommended for the M.Phil module Homotopy type theory and univalent foundations. The book is not currently available in print so this is the only means of accessing the full text.