Pablo
Donato

Hi! Welcome to my webpage.

I am a postdoctoral researcher in computer science, working towards better user interfaces for proving and programming. I want programming systems that make it easier to both create, understand and modify software, so that people can take control over their digital tools.

Previously I did a PhD at École Polytechnique, where I worked within the Partout team of the LIX laboratory under the supervision of Benjamin Werner.

Please feel free to send me a message at

News

  • 25-07-2025 – My latest preprint about scroll nets, the Curry-Howard correspondence for existential graphs, is now public!
    paper arXiv
  • 10-06-2025 – I presented my thesis work, as well as my latest research about the Curry-Howard correspondence for existential graphs, at the D3S seminar in Prague.
    slides
  • 10-01-2025 – I presented the Flower Calculus at the Joint Mathematics Meeting in Seattle, as part of the Compassionate Math session.
    abstract slides video
  • 16-09-2024 – My PhD thesis is now available on official platforms.
    ⟨NNT : 2024IPPAX015⟩ ⟨tel-04698985⟩
  • 30-07-2024 – I am releasing the final version of my PhD thesis manuscript!
    manuscript github
  • 29-05-2024 – I successfully defended my PhD thesis at École polytechnique (bâtiment Turing).
    slides video
  • 22-04-2024 – My paper on The Flower Calculus has been accepted at FSCD 2024!
    article

Research

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

Interests

Curry-Howard correspondence proof theory programming language theory type theory proof assistants end-user programming direct manipulation interfaces

PhD thesis

⟨NNT : 2024IPPAX015⟩ ⟨tel-04698985⟩ manuscript github defense (slides) defense (video)

I developed 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 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.

Manifesto

Since the day I discovered computers, I have been fascinated by their ability to represent and give life to human intentions. I quickly got into programming to unlock their full creative potential, but always felt a discrepancy between the immediacy and intuitiveness of graphical interfaces, and the expressivity and rigidity of programming languages.

Then I discovered formal logic, a field that claims to capture correct reasoning and truth instead of arbitrary computation. This really hit home, as the experience of program debugging deepened my doubts about the meaningfulness of my own thoughts. How could I ever be sure the programs I wrote would always behave in the way I intended them to? Formal logic provided a language to clarify my intent, and guarantee that programs respect it.

Now although I love analysing things under the logico-computational microscope, I feel like it focuses too much on linguistic expressions, and the way they can be classified and checked for validity. It assumes I already know what I want, and how to express it symbolically. What I seek for is a format enabling a true collaboration with the computer, one where I can freely visualize, manipulate, transform and discover new ideas under its guidance, instead of squeezing my thoughts in its pre-existing categories. Meaning should emerge from my interaction with the computer and its users, not from my head.

Today I believe that logic can offer principled ways of designing and evolving such formats. This is because logicians have developed conceptual tools to specify meaning a priori, before knowing its precise embodiment. But to make this reality possible, we need to rethink the architecture of the logical edifice, so that we can articulate formats in a less rigid, more interoperable way. We need to open logic to the world, rather than try to fit the world into logics.

Publications
My dblp profile.

Preprints

2025

Conferences

2024

2022

  • Pablo Donato, Pierre-Yves Strub, Benjamin Werner. Actema : une interface graphique et gestuelle pour preuves formelles (démonstration). 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.267-268. ⟨hal-03626854⟩
  • Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. 2022. A drag-and-drop proof tactic. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022). Association for Computing Machinery, New York, NY, USA, 197–209. https://doi.org/10.1145/3497775.3503692
    paper talk

Projects

Resume/CV
One-page resume

Education

Experience

Academia

Industry

  • C#/XAML for HTML5 – Userware 2018

    I worked in R&D on the TypeScript compiler integrated in the C#/XAML for HTML5 product.

Skills

  • Proof assistants – Lean, Rocq
  • General-purpose programming – OCaml, Python, Java, C#, Prolog, C/C++
  • Web programming – HTML/CSS, JavaScript, TypeScript, Vue.js, Electron, Elm, PHP/MySQL
  • Tooling – GNU/Linux, Unix shell, Git, Nix
  • Typesetting – LaTeX, Typst
  • Languages – French (native), English (fluent)

Miscellaneous
  • I am a member and co-founder of the ReFL, a discussion group on the foundations of logic and computation.
  • I have been playing piano 🎹 since I was 6, and drums 🥁 since highschool. I also dabble in singing 🎤 and composition/improvisation with Ableton Live 🎛. You can find many of my experiments on my SoundCloud.