Proof Theory and Logic Programming:
Computation as Proof Search

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-06-27.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 (where 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 like 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

• Computation as Proof Search

  This book develops the idea that computation can be based on the search for proofs in various logical systems. This perspective offers a declarative understanding of programming, where the logic formulas themselves are the programs, and their execution is the process of finding proofs. This approach provides a principled and logical foundation for understanding how logic programs work. It moves away from purely operational descriptions and allows for reasoning about programs based on the properties of the underlying logic.

• A Spectrum of Logics for Programming

  The book explores how different logics—namely, classical, intuitionistic, and linear logic, as well as first-order and higher-order versions—can be the foundation for designing logic programming languages. Many examples are provided that show how the choice of logic influences the expressiveness and operational behavior of the resulting programming language.

• Emphasis on Sequent Calculus and Focused Proofs

  The book uses sequent calculus as the primary proof system for formalizing logic programming. In particular, it developed the notion of focused proof systems, which provide a structured approach to proof search by organizing inference rule applications into distinct phases. This use of sequent calculus and its focused variants provides concrete tools for analyzing the operational semantics of logic programs.

• Over 90 exercises are proposed and many have full or partial solutions

  The exercises are designed to help the reader explore definitions and proof techniques.

Table of Contents

• Preface
• Chapter 1. Introduction
• Chapter 2. Terms, formulas, and sequents
• Chapter 3. Sequent calculus proof rules
• Chapter 4. Classical and intuitionistic logics
• Chapter 5. Two abstract logic programming languages
• Chapter 6. Linear logic
• Chapter 7. Formal properties of linear logic focused proofs
• Chapter 8. Linear logic programming
• Chapter 9. Higher-order quantification
• Chapter 10. Specifying computations using multisets
• Chapter 11. Collection analysis for Horn clauses
• Chapter 12. Encoding security protocols
• Chapter 13. Formalizing operational semantics
• Solutions to Selected Exercises
• Bibliography
• Index

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

Last updated: 27 June 2025