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
proof assistants constructive logics proof theory programming language theory Curry-Howard correspondence end-user programming direct manipulation interfaces
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.
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.
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.
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.
I researched novel ways to interact with proof assistants through graphical interfaces. More precisely, I designed direct manipulation principles for constructing proofs incrementally by executing gestures on logical statements. My methodology was based on the exploration and application of techniques from a branch of structural proof theory called deep inference.
I teached algorithms, data structures and object-oriented programming in Java, as well as Web programming in HTML/CSS/JavaScript and PHP.
I teached Python and Java to 1st and 2nd year bachelor students in maths/computer science.
I designed a variant and an extension of the subformula linking technique for intuitionistic logic.
I studied L-nets, a model of computation inspired by ludics and proof-nets, and designed a term syntax for L-nets.
I studied ludics, a foundational theory for mathematical logic based on an abstract notion of interactive computation.
I implemented an OpenAI Gym environment for deep reinforcement learning, where an agent can explore a grid of hand-written digits images.
I built a remote embedded system on a Raspberry Pi to monitor battery levels of a wind turbine from an Android application.
I worked in R&D on the TypeScript compiler integrated in the C#/XAML for HTML5 product.