[TYPES/announce] Book Announcement--Proof Theory and Logic Programming: Computation as Proof Search

[Dale Miller]

Dear colleagues,

I am pleased to announce the publication of my new book,
``Proof Theory and Logic Programming: Computation as Proof Search''
(Cambridge University Press, December 2025).

While the proof-as-program paradigm is widely used to explain
functional programming, this book explores the alternative paradigm:
computation as the search for proofs. By shifting the foundation of
logic programming from resolution and Horn clauses to structural proof
theory and the sequent calculus, we can extend the reach of logic
programming into intuitionistic and linear logics, incorporating both
first-order and higher-order quantification.

Key Features of the Book

 * Theoretical Foundations: Detailed coverage of the sequent calculus,
   focused proofs, and cut-elimination.
 * Logic Expressiveness: Exploration of classical, intuitionistic, and
   linear logics within a programming context.
 * Practical Applications: Case studies in security protocols,
   operational semantics, and static analysis.

The book is designed for advanced undergraduate and graduate students,
researchers, and educators. No prior background in the sequent
calculus is assumed, making it accessible to anyone with a general
interest in logic and computer science.

More Information & Resources
- Order from the Publisher: Cambridge University Press:
  https://urldefense.com/v3/__https://doi.org/10.1017/9781009561280__;!!IBzWLUs!SHPU6ikQuwNLTj_DsZfyFNACJbz6ZA2GjtMfkZuc0uvjEEW9g1P1XYN4Ni5qr9GPcJC72i9aLKjBt9UIbOlo7haWG2IPMaXDHXrZ$ 
- Author’s Webpage: View table of contents, endorsements, and preprint
  https://urldefense.com/v3/__https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/__;!!IBzWLUs!SHPU6ikQuwNLTj_DsZfyFNACJbz6ZA2GjtMfkZuc0uvjEEW9g1P1XYN4Ni5qr9GPcJC72i9aLKjBt9UIbOlo7haWG2IPMQhGLJuK$ 

Best regards,
Dale Miller
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20260105/f316964f/attachment-0001.htm>