Our systems are now restored following recent technical disruption, and we’re working hard to catch up on publishing. We apologise for the inconvenience caused. Find out more

Item added to bagSorry, there was a problem getting your bag informationItem cannot be purchased with the existing contents of your bagItem unavailable online
✕

was added to your bag.

Please try again.

Sorry, this item cannot be purchased in the same transaction as the existing items in your bag.

Please complete the purchase of the items currently in your bag and then add this item in a separate transaction or visit Shopping Help.

Sorry, this product is not currently available to buy online. Please visit Shopping Help.

View bag and checkout
Remove item
✕

Are you sure you want to remove from your bag?

Recommended product

Popular links

Popular links

Proof Theory and Logic Programming

All titles
Proof Theory and Logic Programming

Proof Theory and Logic Programming

Computation as Proof Search
Dale Miller , INRIA Saclay-ÃŽle-de-France
December 2025
Not yet published - available from December 2025
Hardback
9781009561297

Looking for an examination copy?

This title is not currently available for examination. However, if you are interested in the title for your course we can consider offering an examination copy. To register your interest please contact [email protected] providing details of the course you are teaching.

c.
$79.99
USD
Hardback
    Description

    Product details

    December 2025
    Hardback
    9781009561297
    400 pages
    229 × 152 mm
    Not yet published - available from December 2025

    Often bought together

    Logic Programming
    Logic Programming

    : Paperback

    Operational Semantics and Proof Theory

    Foundations of Parallel Programming
    Foundations of Parallel Programming

    : Paperback

    Logic and Computation
    Logic and Computation

    : Paperback

    Interactive Proof with Cambridge LCF

    Semantics and Logics of Computation
    Semantics and Logics of Computation

    : Hardback

    Often bought together

    cambridge core banner

    Related Journals

    The Review of Symbolic Logic
    The Review of Symbolic Logic

    : Journal

    The Review of Symbolic Logic is designed to cultivate research on theborders of logic, philosophy, and the sciences, and to supportsubstantive interactions between these disciplines. The journalwelcomes submissions in any of the following areas, broadly construed: - The general study of logical systems and their semantics,including non-classical logics and algebraic logic; - Philosophical logic and formal epistemology, including interactions with decision theory and game theory; - The history, philosophy, and methodology of logic and mathematics, including the history of philosophy of logic and mathematics; - Applications of logic to the sciences, such as computer science, cognitive science, and linguistics; and logical results addressing foundational issues in the sciences. The Review welcomes submissions in all these areas. (For informationon how to submit papers, see Guidelines below.) The Review beganpublication in June 2008.

    Related Journals

    Also by this Author

    Contents

    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.
      • Show more
    Courses
    Resources
    Additional Information
    About the authors
      Author
    • Dale Miller , INRIA Saclay-ÃŽle-de-France

      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.

    Accessibility

    Browse by related subject

     
    ✕

    Sorry, this item cannot be purchased in the same transaction as the existing items in your cart.

    Please complete the purchase of the items currently in your cart and then add this item in a separate transaction or contact

    Customer Services