Proof Theory and Logic Programming - Computation As Proof Search

This book offers a principled view of programming, showing how computation arises from logic. It explores different logical and proof-theoretic systems as foundations for programming, providing a deeper understanding for readers interested in the theoretical underpinnings of computation and the logic programming paradigm.

Inhaltsverzeichnis

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.

Über den Autor / die Autorin

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.

Produktdetails

• Autoren: Dale (Inria Saclay-Ile-De-France) Miller, Miller Dale
• Verlag: Cambridge University Press ELT
• Sprache: Englisch
• Produktform: Fester Einband
• Erschienen: 31.12.2025
• EAN: 9781009561297
• ISBN: 978-1-0-0956129-7
• Seiten: 334
• Themen: Naturwissenschaften, Medizin, Informatik, Technik > Informatik, EDV > Programmiersprachen; 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