Proof Theory and Logic Programming: Computation as Proof Search

by Dale Miller

Overview

Shows how computation can be understood as proof search across classical, intuitionistic, and linear logics via sequent calculus.

Product Details

ISBN-13:	9781009561297
Publisher:	Cambridge University Press
Publication date:	12/18/2025
Pages:	334
Product dimensions:	6.50(w) x 1.50(h) x 9.50(d)

About the Author

Dale Miller is Director of Research at INRIA Saclay-Île-de-France. He has been a professor at the University of Pennsylvania, Pennsylvania State University, and the École Polytechnique in France. He served as Editor-in-Chief of the 'ACM Transactions on Computational Logic' and has received an ERC Advanced Investigators Grant, the LICS Test-of-Time Award (twice), and the Dov Gabbay Prize for Logic and Foundations. He is an ACM Fellow.

Table of Contents

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

Editorial Reviews

‘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

From the Publisher