Proof Theory and Logic Programming - Computation as Proof Search

List 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.

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.

Product details

• Authors: Miller Dale
• Publisher: Cambridge Academic
• Languages: English
• Product format: Hardback
• Release: 31.12.2025
• EAN: 9781009561297
• ISBN: 978-1-009-56129-7
• Illustrations: Worked examples or Exercises
• Subjects: Natural sciences, medicine, IT, technology > IT, data processing > Programming languages; Programming Techniques, Computer architecture & logic design, Programming & scripting languages: general, Computer architecture and logic design, Program concepts / learning to program, Programming and scripting languages: general, COMPUTERS / Languages / General