Pablo
Donato

Hi! Welcome to my webpage.

I am a post-doctoral researcher at the Grothendieck Institute, working on the formalization of topos theory in the Lean proof assistant. Previously I did a PhD in computer science, working within the Partout team of the LIX laboratory under the supervision of Benjamin Werner.

My work lies at the intersection between mathematical logic 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.

Please feel free to send me a message at

News

Research

Interests

proof assistants constructive logics proof theory programming language theory Curry-Howard correspondence 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 Mathis Bouverot, we are currently building coq-actema, a system that extends and integrates the interface of Actema in the Coq 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.

    To handle quantification and equality, Peirce and Oostra use so-called lines of identity, a string diagram-like notation well-suited to the intensional analysis of relations. But state-of-the-art proof assistants are based on type theory — and thus at their core on the λ-calculus, which is an intensional theory of functions. Hence I designed a fully inductive variant of Oostra's graphs, based on the standard notions of binder and variable at the root of λ-calculus. This eases the development of a formalized metatheory, as well as the connection with type theory. I named it flower calculus, because of the way I like to draw the graphs as nested flowers.

Publications

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
    article talk

Projects
  • Flower Prover 2023-Present

    I am building in Elm the Flower Prover, a prototype of GUI in the Proof-by-Action paradigm based on the flower calculus. It is a mobile-friendly structural editor based on a modal interface, a bit like the vim text editor: proofs are built in Proof mode, edited in Edit mode, and (can soon be) navigated in Navigation mode.

    try it! github
  • coq-actema 2022-Present

    coq-actema is a system that integrates the interface of Actema in the Coq proof assistant as an interactive proof view. Actema is packaged as an Electron application that receives goals from Coq over HTTP, and sends back graphical actions to a Coq plugin that compiles them into proof terms.

    talk github
  • Actema 2020-2022

    Actema is a prototype of GUI for interactive theorem proving by direct manipulation of formulas in goals. Its development was started by Pierre-Yves Strub and Benjamin Werner in 2019. I contributed many new features during my Master's thesis, and took over most of its development during my PhD thesis.

    try it! frontend backend

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 – Coq
  • 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 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.