Pablo Donato

Postdoc

Department of Distributed and Dependable Systems
Faculty of Mathematics and Physics
Charles University

Malostranské náměstí 25
118 00 Praha 1
Czech Republic

E-mail: pablo.donato@tuta.io
Web: https://pablogician.refl.fr
Office: 204, 2nd floor

Research

I work at the intersection between mathematical logic, programming language theory and human-computer interaction, with applications to interactive theorem proving. More precisely, I try to design graphical representations of proofs and programs that are better suited to direct manipulation by humans, but still understandable by computers.

My methodology employs tools and intuitions from many different fields and research communities. This includes primarily formal systems from proof theory and type theory through the Curry-Howard correspondence, but also concepts from visual programming and programming by demonstration, string diagrams from category theory, and even ideas from the famous 19th century philosopher C. S. Peirce.

I am currently attempting to merge all these inspirations in the theory of scroll nets. It is a new diagrammatic formalism for proofs/programs based on Peirce’s existential graphs, with intuitive direct manipulation principles that enjoy a rich metatheory. I will soon start experimenting with a prototype implementation of scroll nets, in the form of an interactive graphical playground running as a web app.

If you are a student and that looks interesting to you, do not hesitate to reach out for a potential student project on these topics!

PhD Dissertation

Deep Inference for Graphical Theorem Proving, Institut Polytechnique de Paris, 2024.

I researched novel ways to interact with proof assistants through graphical interfaces, by developing three interrelated lines of investigations:

• Proof-by-Action is a paradigm where the user builds proofs by executing gestural actions directly on the proof state. Typically, this corresponds to the possibility of clicking, dragging and dropping items which represent the conclusion and hypotheses of the current goal. A prototype implementation of this paradigm called Actema is available online at actema.xyz. With Benjamin Werner and contributors, we have been building coq-actema, a system that extends and integrates the interface of Actema in the Rocq proof assistant.

• Deep inference is a new methodology in proof theory, which aims at overcoming some limitations of Gentzen-style proof systems while preserving their good properties. In the setting of interactive proof building, one interesting feature of deep inference systems is their ability to preserve the context in which reasoning is performed. This gave rise recently to the idea of subformula linking, a method for solving goals incrementally by connecting dual occurrences of subformulas. I designed an extension of subformula linking for intuitionistic first-order logic with equality, which generalizes the behavior of known application and rewriting tactics.

• Existential graphs are among the first diagrammatic proof systems in history, invented by C. S. Peirce as early as 1882. They enable a kind of reasoning free from the linguistic notion of logical connective, which is a promising venue for fully graphical proving interfaces. Initially conceived for classical (boolean) logic, A. Oostra recently introduced an intuitionistic version of existential graphs, based on Peirce’s own intuitions of logical implication. This paves the way for connections with the trend of constructive logics in proof assistants. I developed the Flower Calculus, a variant of Oostra’s graphs for first-order logic with good proof-theoretic properties, and built the Flower Prover, a prototype of GUI for interactive theorem proving based on it.