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:	11/30/2025
Pages:	400
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.