Hi! Welcome to my webpage.
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
I develop 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, 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. Benjamin Werner implemented the elaborator for most graphical actions, and I designed and built everything else.
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 Python and Java to 1st and 2nd year bachelor students in maths/computer science.
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.