Schedule for: 25w5406 - Proof Representations: From Theory to Applications

A buffet dinner is served daily between 5:30pm and 7:30pm in Vistas Dining Room, top floor of the Sally Borden Building.

Informal Meet and Greet at BIRS Lounge (PDC building, 2nd floor). You are also welcome to use JPL 313 space and deck 6-9pm (should you wish to have an alternative location).

Breakfast is served daily between 7 and 9am in the Vistas Dining Room, the top floor of the Sally Borden Building.

A brief introduction to BIRS with important logistical information, technology instruction, and opportunity for participants to ask questions.

In this tutorial I will present a family of modal logics that include operators that can modify the model in which they are being evaluated.  Some examples of this family are Public Announcement Logic and Sabotage Logic.  We will discuss when and how the addition of this kind of modal operators leads to expressivity gains, and the impact they have for reasoning systems for the resulting logics. 

KC #301

In this tutorial I will present a family of modal logics that include operators that can modify the model in which they are being evaluated.  Some examples of this family are Public Announcement Logic and Sabotage Logic.  We will discuss when and how the addition of this kind of modal operators leads to expressivity gains, and the impact they have for reasoning systems for the resulting logics. 

Lunch is served daily between 11:30am and 1:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

The question of whether Propositional Dynamic Logic (PDL) has the Craig Interpolation Property (CIP) has remained open for many years, with at least three attempted proofs later found to be flawed or incomplete. In this talk, I will present the main ideas behind our tableau-based argument that PDL does indeed satisfy the CIP, with a focus on the novel aspects of our approach. arXiv preprint: arxiv.org/abs/2503.13276 Our proof builds on foundational ideas introduced in Manfred Borzechowski’s 1988 diploma thesis. This is joint work with Malvin Gattinger, Helle Hvid Hansen, Valentina Trucco Dalmas, and Yde Venema.

Breakout Rooms available for BIRS participant use: Kinnear Centre #301 Jeane and Peter Lougheed (JPL) #213, #214,#215 TCPL #107

KC#301

Breakout Rooms available for BIRS participant use: Kinnear Centre #301 Jeane and Peter Lougheed (JPL) #213, #214,#215 TCPL #107

A buffet dinner is served daily between 5:30pm and 7:30pm in Vistas Dining Room, top floor of the Sally Borden Building.

Breakfast is served daily between 7 and 9am in the Vistas Dining Room, the top floor of the Sally Borden Building.

In this tutorial I intend to show that it is easy to do better, i.e. formalised, basic proof theory. More precisely, we will interactively go through the formalisation of a few types of proof systems for intuitionistic logic. On the menu: an axiomatic system with sets as contexts ; a sequent calculus based on multisets ; a sequent calculus based on lists. We will introduce basic Rocq* tools as we go, prove a few fundamental results for each calculus, and discuss design decisions. The Rocq code for this course will be readily available for you to modify and formalise a proof system for your favourite logic. *The Coq proof assistand was recently renamed to Rocq.

KC#301

Meet outside the Kinnear Centre to participate in the BIRS group photo. The photograph will be taken outdoors, so dress appropriately for the weather. Please don't be late, or you might not be in the official group photo!

Lunch is served daily between 11:30am and 1:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

Type theory is central to the design of several prominent proof assistants, such as Automath, Rocq, and Lean. In contrast, proof assistants directly inspired by proof theory are less prevalent, with Abella serving as a significant example. This talk will analyze key design differences between proof assistants rooted in type theory and those drawing from proof theory. Despite the current dominance of type-theoretic approaches, we will explore the potential of proof-theoretic principles to inspire novel features and advancements in proof assistants, particularly as demonstrated by systems like Abella. Furthermore, we will discuss how leveraging proof-theoretic insights could unlock new functionalities and directions for the evolution of proof assistants like Abella.

Breakout Rooms available for BIRS participant use: Kinnear Centre #301 Jeane and Peter Lougheed (JPL) #213, #214,#215 TCPL #107

KC#301

Breakout Rooms available for BIRS participant use: Kinnear Centre #301 Jeane and Peter Lougheed (JPL) #213, #214,#215 TCPL #107

A buffet dinner is served daily between 5:30pm and 7:30pm in Vistas Dining Room, top floor of the Sally Borden Building.

Breakfast is served daily between 7 and 9am in the Vistas Dining Room, the top floor of the Sally Borden Building.

Deep inference is a methodology for the design of proof formalisms, which generalises the composition mechanisms seen in Gentzen-style proof systems. Proofs can be composed not only by inference rules but also sequentially and horizontally by connective; equivalently, rules can be applied at any depth inside a formula. I will discuss how this disrupts some established results in Gentzen-style structural proof theory, but by counting more objects as proofs, we see benefits from the perspectives of normalisation, complexity and semantics. I will also present some ongoing research in subatomic logic, a recent area of development in deep inference in which the atoms also become connectives by which proofs can be composed.

KC#301

Proof-theoretic semantics aims to explain the meaning of logical constants through the structure of inference rather than truth-conditions. This talk surveys the development of the field from its roots in Gentzen’s account of proof and Prawitz’s normalization-based account of validity, through to the contemporary framework of base-extension semantics. I’ll describe how this approach resolves key limitations and yields soundness and completeness proofs for a wide range of logics, including intuitionistic, classical, modal, and linear systems. The goal is not only to chart a line of continuity in the theory, but to show how questions of meaning, inference, and structure are converging into a more unified proof-theoretic foundation.

Lunch is served daily between 11:30am and 1:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

A buffet dinner is served daily between 5:30pm and 7:30pm in Vistas Dining Room, top floor of the Sally Borden Building.

Breakfast is served daily between 7 and 9am in the Vistas Dining Room, the top floor of the Sally Borden Building.

Logic, and especially proof theory, have played an important role for understanding computation and programming. For example, formal proofs are largely employed today to certify sensitive properties of algorithms (will the algorithm meet its own specification in every context? Do two algorithms compute the same function?). However, while such applications of proof theory mostly pertain to deterministic programs, probabilistic programming and statistical inference methods have gained today a prominent position among the programming paradigms. The algorithms arising from such methods are not thought to meet some specification exactly, but only up to some probability, nor to compute some given function precisely, but only to approximate its values in an efficient way. In this talk we will discuss how ideas and methods from logic and proof theory, like the Curry-Howard correspondence, can be adapted in order to certify properties of probabilistic functional programs. A particular focus will be put on establishing the probability that a program will terminate, as well as the probability that it will meet a target specification.

KC#301

Cyclic proofs are an expressive proof system for logics with recursively defined operators, such as fixpoints, transitive closure modalities, or common knowledge operators. A cyclic proof tree offers a finite representation of an infinite (non-wellfounded) proof, relying on regularity of the infinite tree. To ensure soundness, cyclic proofs must additionally satisfy a correctness criterion, typically defined as a global condition on trees which is tailored to the logic at hand. Labelled sequent calculi enrich the traditional Gentzen-style sequent formalism by incorporating ‘labels’ encoding semantic information from Kripke (counter-)models. These calculi are highly modular, enabling to define uniform proof systems for large families of modal and non-classical logics. Seeking to combine the expressiveness of cyclic proofs with the generality of labelled calculi, this talk investigates the definition of cyclic proofs within the framework of labelled sequent calculus. Using Gödel-Löb provability logic as a case study, we propose a cyclic labelled proof system, examine its properties, and compare it to related approaches in the literature. Based on joint work with Jan Rooduijn

Lunch is served daily between 11:30am and 1:30pm in the Vistas Dining Room, the top floor of the Sally Borden Building.

Verification of models of biological and medical systems is a promising application of formal verification. Human neural networks have recently been emulated and studied as a biological system. In this work, we provide a model of some crucial neuronal circuits, called archetypes, in the Rocq Prover and prove properties concerning their dynamic behavior. Understanding the behavior of these modules is crucial because they constitute the elementary building blocks of bigger neuronal circuits. We consider a variety of fundamental archetypes and prove an important representative property for most of them.  In building up to our model of archetypes, we also provide a general model of neuronal circuits, and prove a variety of general properties about neurons and circuits. In addition, we have defined our model with a longer term goal of modeling the composition of basic archetypes into larger networks, and structured our libraries with definitions and lemmas useful for proving the properties in both current and future work. This is joint work with Abdorrahim Bahrami, Rebecca Zucchini, and Elisabetta De Maria.

Breakout Rooms available for BIRS participant use: Kinnear Centre #301 Jeane and Peter Lougheed (JPL) #213, #214,#215 TCPL #107

A buffet dinner is served daily between 5:30pm and 7:30pm in Vistas Dining Room, top floor of the Sally Borden Building.

Breakfast is served daily between 7 and 9am in the Vistas Dining Room, the top floor of the Sally Borden Building.

Main Talks: Jeane and Peter Lougheed (JPL) #313 Breakout Rooms: #213, #214,#215 TCPL #107

JPL #313

Main Talks: Jeane and Peter Lougheed (JPL) #313 Breakout Rooms: #213, #214,#215 TCPL #107

5-day workshop participants are welcome to use BIRS facilities (TCPL ) until 3 pm on Friday, although participants are still required to checkout of the guest rooms by 11AM.