|
Proof Theory and Logic Programming: Computation as Proof Search 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. |
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.
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.
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.
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.
The exercises are designed to help the reader explore definitions and proof techniques.
An excellent exposition of proof search as a vehicle for realizing computations that, in the process, provides a novel view of structural proof theory through the prism of logic programming. Another strength is the presentation of linear logic and its use in modelling computational systems. Ideal for a graduate-level course on logic and its role in specification and programming.
Gopalan Nadathur, University of Minnesota
Proof Theory and Logic Programming: Computation as Proof Search by Dale Miller is a refreshing look at the role that logic, specifically proof theory, plays in the foundation of computation. The book takes the perspective of a less-traveled route of applications of proof theory to computation - through the lens of proof search, a systematic and disciplined approach for searching for proofs of logical propositions. The book assumes minimal prerequisites, which makes it accessible to novices and experts alike. Its comprehensive coverage of decades of work in the field should make this an excellent reference textbook.
Alwen Tiu, The Australian National University
This book is a clear and elegant journey through the connections between proof theory and programming. With a rigorous treatment of logic programming via sequent calculus and focused proof systems, Miller shows how logic can shape the way we think about computation without losing sight of practical relevance. Proof Theory and Logic Programming is a great resource for students, researchers, and anyone interested in exploring the theoretical foundations of logic-based programming languages.
Elaine Pimentel, University College London
This book takes the reader on a rigorous, yet accessible journey starting from fundamental proof theoretic principles to understanding proof search as the computational foundation of logic programming. It is a joy to read and a valuable resource for anyone interested in the intersection of logic, computation, and language design.
Brigitte Pientka, McGill University
Miller's book represents a long-awaited authoritative source on the proof-theoretic account of logic programming. It is ideal for students, educators, and researchers seeking to understand logic programming from a principled standpoint. Miller develops this account via the theoretical lens of sequent calculus, carefully illustrating how the choice of logic and search strategy affects operational properties of computation and structural properties of proofs. The material is interleaved with examples and exercises, providing a first-of-its-kind resource for learners on subjects such as focused proof systems, linear logic programming, and higher-order logic programming. The book concludes with two case studies, showcasing how a logic programming language incorporating the book's earlier developments can be used for modeling communication protocols and operational semantics.
Chris Martens, Northeastern University
The book cover is based on artwork by Nadia Miller (LinkedIn, ArtStation and WiX).
Last updated: 28 August 2025
