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