Cambridge University Press has recently published my book, “Proof Theory and Logic Programming: Computation as Proof Search” (December 2025). A preprint of the full text is available for download [1]. While the proof-as-program approach — where computation is driven by proof normalization — is well-documented in the literature, this book explores an alternative formalization: the…
Dale Miller
I received my Ph.D. in Mathematics in 1983 from Carnegie Mellon University. I have been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and Department Head in Computer Science and Engineering at Pennsylvania State University. I am currently a Director of Research at Inria Saclay. My research interests include various topics in computational logic including proof theory, automated reasoning, logic programming, unification theory, operational semantics, and proof certificates.
Personal Comments about Peter Andrews
I want to add more personal observations about Peter and his work than what appears in the In Memoriam. Being a Ph.D. Student with Peter Andrews An important research project for Peter was constructing a theorem-proving environment for the version of higher-order logic that his Ph.D. advisor, Alonzo Church, designed and named the Simple Theory…
In Memoriam: Peter B. Andrews (November 1, 1937 – April 21, 2025)
Peter B. Andrews, an American mathematician and Professor Emeritus at Carnegie Mellon University, passed away on April 21, 2025, at the age of 87. Andrews was a leading figure in the theory and applications of higher-order logic and automated reasoning. Peter Andrews received his Ph.D. in Mathematics from Princeton University in 1964, where he was…
Notation for focused proof systems
Standardized notation can be helpful, especially after a topic has matured. For example, Gentzen used as an infix symbol to build sequents from lists of formulas. While one also sees used, it seems that in recent years, has become the standard, especially when proof theory is applied to type theory (where is invariably used) and…