I will discuss some ongoing work on using types based on intuitionistic modal logic and its natural deduction proof systems for specifying, controlling, and verifying how programs use their resources. I will begin by first recalling some of the main challenges that designing natural deduction proof systems for (intuitionistic) modal logic poses, and the different ways these challenges have been addressed in the literature. From a programming languages perspective, a natural deduction proof system is desirable, as opposed to a purely axiomatic account, because the interaction of introduction and elimination rules immediately gives us natural rules of computation. Then, in the second part of the talk, I will discuss how a particular approach to natural deduction for intuitionistic modal logic, often called a Fitch-style presentation, when viewed through the Curry-Howard (propositions as types) correspondence, provides us a convenient type-based means for controlling how programs use their resources.
(The second part of the talk is based on past and ongoing joint work with Andres Alumets, Mariana Milicich, Gašper Žajdela, and Joosep Tavits.)
The Curry-Howard correspondence is a celebrated result connecting logic and computation: propositions are types, proofs are programs, and proof normalization is computation. Lambek extended this correspondence to category theory, revealing that proofs of intuitionistic propositional logic and terms of the simply typed lambda calculus share a common categorical structure---Cartesian closed categories. Building on this extension and on recent developments in string diagrams for closed symmetric monoidal categories, we position diagrammatic methods at the same level as proofs and programs, establishing diagrams as a third, equivalent pillar of this fundamental correspondence.
In the first part of the talk, I will discuss new logical characterizations of the circuit complexity class TC0 via extensions of first-order logic with simple cardinality quantifiers over ordered structures. In the second part, I will consider first-order logic and its extensions under the so-called semiring semantics, and their connections to complexity classes defined by Blum-Schub-Smale (BSS) machines and arithmetic circuits.
The early development of mathematical logic was the result of efforts by logicians in several countries. Important contributions were made in Britain by a line of logicians from George Boole to Bertrand Russell. Charles Sanders Peirce opened the way to modern logic in the United States. Gottlob Frege and Ernest Schröder worked in Germany. In Italy, Giuseppe Peano founded an influential school of logic. However, it is rather rare to meet with French logicians in histories of early mathematical logic. Did they not exist?
Combinatory logic was introduced more than a century ago in pursuit of logical syntax without bound variables. Its power and simplicity have made it a subject of enduring interest, and it has played a foundational role in logic and computer science. A combinatory algebra is an algebraic model of combinatory logic. Concretely, such an algebra consists of a set equipped with a binary operation satisfying a condition called combinatory completeness. This condition is rather complex, but is equivalent to the existence of elements of the carrier set satisfying certain simple equations.
This talk concerns a more general notion of combinatory completeness relative to a certain well-behaved collections of functions between finite sets, called faithful Cartesian clubs. The classical notion of combinatory completeness corresponds to the club consisting of all such functions. Moreover, the equivalence of combinatory completeness with the existence of elements satisfying simple equations holds in some form for a number instances of the more general notion.
These results hold in settings beyond the usual category of sets and functions, and their technical development takes place in a multicategory equipped with an action of the faithful Cartesian club in question. These structured multicategories are a natural setting in which to study (variations of) combinatory algebras. Although the categorical perspective is in some ways the central idea, the talk will aim to be accessible to those not versed in category theory.
This talk is based on joint work with Ivan Kuzmin, Ülo Reimaa, and Sam Speight. A preprint is available as arXiv eprint 2511.17152 (2025).
Making formal guarantees based on other people's claims is difficult, especially since not everyone is inclined to share all they know, and verifying facts based on partial information is sometimes impossible. Do you simply accept their claims as true, and risk building on lies and mistakes? Or is there a way to keep such claims in their proper context, as statements based on certain sources? Intuitionistic multimodal logic gives a good framework for combining formal constructive reasoning principles, given by the intuitionistic logic, with subjective beliefs and claims, formulated using modalities. In this talk, we go over how to reason about such modalities expressing knowledge and communication. Which modal axioms strike the right balance between correctness, usefulness, simplicity and decidability? We moreover look at the emergent concept of trust in claims, in order to analyse and express which claims need to be trusted in order to make a formal guarantee.
This talk is based on past and ongoing work with Peeter Laud.
The fibrational perspective on logic considers formulas and proofs as living in a space D that maps down to some smaller and simpler space C. Different questions about logical deduction may then be formulated as "lifting problems" along the mapping p : D → C. One benefit of this perspective is that it may be formulated precisely in the language of category theory and clarifies some aspects of the syntax and semantics of substructural and modal logics. Another benefit is that it provides a uniform mathematical framework in which deductive systems may be considered on a par with other kinds of logical structures, including finite-state automata and context-free grammars.
The talk will provide a high-level overview and introduction to this perspective, focusing on long-running work with Paul-André Melliès as well as recent work with Bryce Clarke and Gabriel Scherer.
References: