ABSTRACT. The Functional Machine Calculus (FMC) is a new foundational model of computation that seamlessly integrates higher-order functions (the lambda-calculus) with effectful imperative computation. Previous approaches to this problem have made use of heavy mathematical machinery, such as monads, monad transformers, Lawvere theories, and premonoidal categories. However, even in the monadic approach, standard effects such as store, input/output, and exceptions are all constructed from simple primitives: products, coproducts, and function spaces; or in other words, standard intuitionistic logic. This opens up a fundamental question: are effects inherently complex, or is there a simple underlying model waiting to be exposed? The FMC is an attempt at the latter, via the approach of structural proof theory, essentially asking the question: what is a good syntax for the phenomena we observe? The answer is a minimal extension of the lambda-calculus, preserving confluent reduction and a type system within intuitionistic logic, that nevertheless allows the embedding of various calculi, effects, and other constructions: the call-by-value lambda-calculus and call-by-push-value; higher-order store, input/output, and probabilistic choice; and sequencing, constants, conditionals, exceptions, and loops. In this tutorial, after a brief overview of the problem and some past solutions, I will introduce the FMC in stages, along with its main features: a small-step operational semantics in a simple stack machine; a natural big-step operational semantics; a confluent reduction relation; and a system of simple types.

ABSTRACT. In a Curry-Howard-Lambek correspondence perspective, proofs are considered up to computational equivalence: βη-equivalence, cut-elimination and axiom-expansion, categorical equality, etc. In intuitionistic logic, η-long β-normal forms of the λ-calculus provide canonical representatives of the equivalence classes. In constructive classical logic, normal forms of the λµ-calculus are not canonical anymore but proof nets provide canonical representatives. By navigating through various (non-polarized) fragments of linear logic, we show that proof nets often reach their limits with respect to canonicity. This forces us to reconsider the equivalence of proofs up to rule permutations as a more robust and more versatile tool for the study of the computational identity of proofs in large fragments.

ABSTRACT. Constructing reasonable proof systems in the presence of generalized quantifiers is challenging, in part due to the general lack of sound introduction/elimination rules for such quantifiers. We propose an alternative approach to the proof theory of generalized quantifiers, using deep inference methods to circumvent this problem. We show that the quantifiers suitable for a deep inference treatment are specifically the class of monotone quantifiers, and subsequently present a generic methodology for designing deep inference proof systems for logics with monotone quantifiers.

ABSTRACT. Proving non-trivial lower bounds on proof size in the classical sequent calculus remains a longstanding open problem in proof complexity. In this work, we revisit this problem through the lens of substructural and linear logics. By considering calculi that restrict contraction or weakening, we obtain systems in which derivations are subject to resource-sensitive constraints. Within these frameworks, we exhibit formulas that, while admitting short classical proofs, require substantially larger derivations. These results provide a proof-theoretic explanation of why classical systems are difficult to analyze: their efficiency stems from the interaction of structural rules, a feature that becomes visible only when examined against substructural baselines.

ABSTRACT. This work investigates proof-theoretic methods for handling Henkin quantifiers within first-order logic. While such quantifiers extend expressiveness beyond standard first-order logic and are naturally representable in second-order logic, their direct treatment poses challenges for analytic proof systems and unification-based reasoning. Building on sequent calculi that incorporate Henkin quantifiers while preserving desirable properties such as cut-elimination and completeness relative to corresponding second-order systems, we introduce tableau systems with unification, enabling effective proof search while maintaining soundness and completeness.

ABSTRACT. The falsifier calculus [1] has recently been introduced as a new deep-inference proof system for first-order predicate logic in the language of Hilbert’s epsilon-calculus. It uses a new inference rule, the falsifier rule, to introduce epsilon-terms into proofs that is distinct from the critical axioms of the traditional epsilon-calculus. The falsifier rule is a generalisation of one of the quantifier-shifts, inference rules for shifting quantifiers inside and outside of formulae. Like the epsilon-calculus and proof systems which include quantifier-shifts, the falsifier calculus admits non-elementarily smaller cut-free proofs of certain first-order theorems than Gentzen’s sequent calculus. Analogous to the way in which Herbrand’s Theorem decomposes a proof into a first-order and a propositional part, connected by a Herbrand disjunction as an intermediate formula, the falsifier calculus provides a new decomposition theorem for first-order proofs which gives rise to a new notion of intermediate formula in the epsilon-calculus, falsifier disjunctions. Certain first-order theorems admit non-elementarily smaller falsifier disjunctions than Herbrand disjunctions, providing a new perspective on the structure and complexity of Herbrand disjunctions. This talk will overview the established work on the falsifier calculus and explore the ongoing research into using the falsifier calculus as a means of extracting Herbrand disjunctions from first-order proofs. [1] Cameron Allett, Non-Elementary Compression of First-Order Proofs in Deep Inference Using Epsilon-Terms, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024), Tallinn, Estonia, Association for Computing Machinery, 2024.