LFCS Seminar: Tuesday 7th July: Pablo Donato | LFCS

Title: Towards a Curry-Howard correspondence for existential graphs

Abstract: In this talk, I will introduce "scroll nets", a novel diagrammatic

formalism for representing proofs and programs. As the name

indicates, it is based on the "scroll", a topological notation for

logical implication invented by Charles S. Peirce at the end of the 19th

century for his system of existential graphs (EGs). In order to obtain a

proper notion of static proof object from the inference rules of EGs, we

add on top of the scroll a graphical syntax inspired by proof nets which

turns out to be an instance of Milner's notion of bigraph, thus also

enjoying an algebraic term syntax.

I will first motivate the diagrammatic notation from a philosophical

standpoint, arguing that it captures the smallest motions of

deductive reasoning in a very natural way, abstaining from any

symbolic means of representation. I will then show how to express

proofs in minimal implicative logic by simulating the rules of natural

deduction. Through the Curry-Howard correspondence, this will lead

us to identify a notion of detour that seems to generalize that of

simply-typed lambda-calculus. I will present ongoing work to provide

operational and denotational semantics to scroll nets, as well as an

adaptation of the normalization-by-evaluation technique to this new

setting. If time remains, I will sketch how to capture: 1. classical

logic and intuitionistic disjunction by considering a horizontal

generalization of the scroll first proposed by Oostra; 2.

intuitionistic subtraction through a further vertical

generalization of my own.

This article was published on Monday 6 July 2026