Connectives of linear logic are sometimes classified as canonical or not. This refers to the possibility (or not) to characterise a connective (up to logical equivalence) by means of its introduction rules. The standard claim is that all linear-logic connectives, but the exponential ones, are canonical. We want to stress that this claim strongly depends, not only on linear logic itself, but on the way rules are constructed. This means in particular that canonicity is not an intrinsic property of connectives but depends on how they are presented: canonicity is not canonical…
Book Announcement: “Proof Theory and Logic Programming: Computation as Proof Search”
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…
Diamond-free parts of intuitionistic modal logics
A post by Anupam and Sonia in 2022 ignited a surge of interest from the modal logic and proof theory communities: until then, it was commonly believed that different inuitionistic versions of modal logic agreed on their -free parts, but this turns out to be false. After 23 comments, 3 papers, 1 further blog post,…
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…