Rencontre, 13 mars 2025

Programme

10:30 – 12:00

Maribel Fernandez (King's College (UK))

Invited talk: Specifying Calculi with Binders in Rewriting Logic

Formalising languages with binders (such as programming languages and logics) within a logical framework with zero representational distance (i.e., the calculus and its representation look the same) poses non-trivial challenges, including: faithful representation of syntax and binding operators; support for calculus-specific equivalences; faithful representation of the language dynamics (operational semantics); and generation of correct-by-construction implementations.

We show how to use rewriting logic to meet these challenges. More precisely, we show how a general notion of binder signature can be axiomatised in rewriting logic following the nominal approach, and we propose a general methodology to specify languages with binders, including their structural congruences and operational semantics. We also show how rewriting logic methods provide executable specifications of languages with binders. We use the pi-calculus as a running example because it illustrates well the above-mentioned challenges.

(Joint work with Jose Meseguer)

13:45 – 14:45

Victoria Barrett (Partout, INRIA)

Invited talk: Subatomic logic and eversion in deep inference

Deep inference is a methodology for the design of proof formalisms, motivated by the pursuit of linearity in the composition mechanisms. Proofs can be composed not only by inference rules but also sequentially and horizontally by connective. This allows for proof systems in which all structural rules are decomposed to their atomic forms, supplemented by linear rule schemes which only move information around.

Subatomic logic is a recent area of development in deep inference in which even the atomic rules are given linearly, by taking atoms not as base elements of a proof but as non-commutative binary connectives whose arguments are their truth values.

I will present some recent work in a subatomic system for propositional classical logic, in particular the 'eversion lemma' and two of its applications, one of which has to do with proof compression and the other with cut elimination, and I will discuss some future directions for research.

Link to CSL paper

15:15 – 16:15

Elena di Lavore (University of Oxford (UK))

Invited talk: Kleene-cartesian bicategories for program logics.

We introduce Kleene bicategories. In the same way that cartesian bicategories of relations capture the structure of relations with cartesian product, Kleene bicategories capture the structure of relations with disjoint union. Kleene-cartesian bicategories combine these two structures by distributing the cartesian product over the disjoint union, and are expressive enough to deal with imperative programs. The derivation rules of Hoare logic follow from the axioms of Kleene-cartesian bicategories.

This talk is based on recent joint work with Filippo Bonchi and Alessandro Di Giorgio.