Message from Prof. Dale Miller (Inria Saclay, FR) **** 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://doi.org/10.1017/9781009561280 <https://urldefense.com/v3/__https://doi.org/10.1017/9781009561280__;!!IBzWLUs!SHPU6ikQuwNLTj_DsZfyFNACJbz6ZA2GjtMfkZuc0uvjEEW9g1P1XYN4Ni5qr9GPcJC72i9aLKjBt9UIbOlo7haWG2IPMaXDHXrZ$> - Author’s Webpage: View table of contents, endorsements, and preprint https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/ <https://urldefense.com/v3/__https://www.lix.polytechnique.fr/Labo/Dale.Miller/ptlp/__;!!IBzWLUs!SHPU6ikQuwNLTj_DsZfyFNACJbz6ZA2GjtMfkZuc0uvjEEW9g1P1XYN4Ni5qr9GPcJC72i9aLKjBt9UIbOlo7haWG2IPMQhGLJuK$> Best regards, Dale Miller **** -- Elaine. ----------------------------------- Elaine Pimentel Schools Outreach Lead Professor of Logic and Computation Deputy Director of the Computer Science and Philosophy programme Programming Principles, Logic, and Verification Department of Computer Science, Office: Room 3.11, 66-72 Gower Street University College London URL: https://sites.google.com/site/elainepimentel/ UCL Computer Science is an *Athena Swan Gold award winner for gender equality <https://www.ucl.ac.uk/computer-science/about/equity-diversity-and-inclusion/gender-equality-athena-swan>* UCL is ranked among the *top ten in the QS World University Rankings 2024 <https://www.ucl.ac.uk/news/2023/jun/ucl-ranked-top-10-universities-world-12-years-running>* and is winner of *The Times and Sunday Times University of the Year 2024 <https://www.ucl.ac.uk/news/2023/sep/ucl-named-university-year>* ----------------------------------- -- LOGICA-L Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <[email protected]> --- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta conversa, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAHQVs%2BUPxD9iYZ6hiuFf5r%3DErbHV3V%3D%3DJEGQZdqfBGwVL5QUPg%40mail.gmail.com.
