Hi! Welcome to my webpage.
I am a 3ʳᵈ year PhD student 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. More precisely, 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 deep inference existential graphs programming language theory Curry-Howard correspondence end-user programming direct manipulation interfaces
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 already 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.
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.