My research in Computational Logic includes the following topics.
Proof theory: Classical, intuitionistic, and linear logics; focused proof systems; fixed points; higher-order quantification
Automated reasoning: foundational proof certificates (ProofCert), unification, interactive theorem proving, Abella, Bedwyr
Logic programming: proof theory foundations, λProlog, λ-tree syntax, linear logic programming
Formalized meta-theory: two-level logic specifications, structured operational semantics
publications |
edited volumes |
tech reports & short articles
talks |
editorial & professional duties |
teaching & advising
cv (pdf) |
research themes |
bio |
personal |
photos
- My book Proof Theory and Logic Programming: Computation as Proof Search will be published by Cambridge University Press in December 2025. A pre-publication draft is available.
- In Memoriam: Peter B. Andrews (November 1, 1937 – April 21, 2025). Also: Personal Comments about Peter Andrews.
- Check out the Proof Theory Blog.
- The Abella proof assistant is based on relational specifications that use the notions of λ-tree syntax and two-level logic specifications. Abella is designed for meta-level reasoning about structures with bindings: see, for example, the specifications of the λ-calculus and the π-calculus.
- Cambridge University Press published in 2012 the book Programming with Higher-Order Logic by Gopalan Nadathur and me (doi, available via CUP and Amazon). This book covers the design and applications of the λProlog programming language.