Seminar tomorrow

[Jan Kofron]

Dear all,

Let me invite you to another seminar in this semester that will take 
place tomorrow, Tuesday, June 10, at 14:00 in S4 [1]. Pablo Donato from 
Grothendieck Institute will talk about "Deep Inference for Graphical 
Theorem Proving". Please find the details below.

[1] https://d3s.mff.cuni.cz/seminar/

Thanks, best regards!
Jan

====

Deep Inference for Graphical Theorem Proving

Abstract: Contemporary proof assistants such as Rocq, Lean and Agda 
provide robust frameworks for constructing and verifying formal proofs, 
and can also be used as very expressive programming languages thanks to 
their powerful type systems. However their interfaces remain largely 
textual, and require users to master mathematical logic and functional 
programming. This poses significant usability barriers, limiting both 
broader adoption and more exploratory, human-centered forms of 
reasoning. This talk introduces Proof-by-Action (PbA), a novel paradigm 
developed in my PhD thesis for interacting with proof assistants through 
direct manipulation in a graphical user interface. Grounded in the 
proof-theoretic framework of deep inference, PbA allows users to 
construct proofs via intuitive gestures—such as clicking and 
dragging—performed directly on logical statements. A live demonstration 
in Rocq will showcase the integration of this paradigm into a 
state-of-the-art proof assistant, enabling gestural proof construction 
within a trusted backend and a rich library ecosystem. I will then 
present a more ambitious research direction: replacing the traditional 
symbolic notations of logic with iconic representations that leverage 
our spatial intuition. I focus on a long-neglected diagrammatic 
formalism introduced by C. S. Peirce at the end of the 19th 
century—existential graphs—and on my intuitionistic extension of them, 
the Flower Calculus. I will conclude with my latest work toward a 
Curry-Howard interpretation of existential graphs, which I hope will 
pave the way for a new kind of interactive programming systems that are 
both strongly typed and genuinely user-friendly.

Bio: Pablo Donato is a postdoctoral researcher in computer science 
currently based in Paris. His research focuses on the design of 
graphical proof languages and interactive tools for formal reasoning, 
with a particular interest in rethinking the user experience of proof 
assistants and programming systems. During his Ph.D., he developed the 
Proof-by-Action paradigm, a novel approach to proof construction based 
on direct manipulation and the proof-theoretic framework of deep 
inference. He also introduced the Flower Calculus, a diagrammatic system 
inspired by C. S. Peirce's existential graphs. His goal is to make 
correct-by-construction programming more feasible by redesigning our 
notations for the dynamic medium. More information can be found on his 
website: https://pablogician.refl.fr/.


-- 
Jan Kofron, Ph.D.
Associate Professor
Department of Distributed and Dependable Systems
Faculty of Mathematics and Physics
Charles University
Malostranske namesti 25
118 00 Praha 1, Czech Republic
Phone: +420 95155 4285
http://d3s.mff.cuni.cz/~kofron
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 236 bytes
Desc: OpenPGP digital signature
URL: <http://d3s.mff.cuni.cz/pipermail/seminar/attachments/20250609/e7e3d2bc/attachment.sig>