Proof Theory and Logic Programming:
Computation as Proof Search

Book Cover

Proof Theory and Logic Programming: Computation as Proof Search
by Dale Miller.

I gave the final draft of this book to Cambridge University Press in Spring 2025. They should publish it in December 2025. Pre-ordering is possible via Cambridge University Press and Amazon.

The most recent version of this book is available as a PDF: ptlp-2025-08-18.pdf (317 pages, 3.3 MB). Comments are welcome.

Summary

This book develops a modern perspective on logic programming by viewing computation as proof search, whereby program execution is seen as the search for proof. It reveals how programs can be naturally and declaratively expressed as logical formulas and their execution as a systematic search for proofs within classical, intuitionistic, and linear logics. It employs sequent calculus as the essential tool for analyzing the operational reading of logic programs. It introduces and applies advanced techniques such as focused proofs to expose the underlying mechanisms of goal-directed search and backchaining. A key feature is its in-depth coverage of higher-order quantification and its implications for logic programming. Beyond theory, the book explores practical applications, including encoding security protocols, specifying operational semantics, and static analysis of Horn clauses, demonstrating the versatility and power of this proof-theoretic approach.

Some key features of this book

Endorsements

The book cover contains endorsements from Gopalan Nadathur, Alwen Tiu, and Elaine Pimentel.

Table of Contents

Cover artwork

The cover artwork is by Nadia Miller (LinkedIn, ArtStation and WiX).


Last updated: 18 August 2025