I am a PhD student at EPFL, working with professor Viktor Kunčak. My research focuses on formal methods, logic, logic-related decision procedures, in particular orthologic. More broadly, my interest include foundations of mathematics, set theory, type theory and theoretical computer science in general. I am the main developer of Lisa, a proof assistant based on first order logic and set theory. Are you a student interested in doing a semester project, master thesis or internship? Look here!
Research
My recent and current research focuses on the following topics:
Orthologic
Orthologic is a weakening of propositional logic where the law of distributivity does not necessarily hold. I have shown a variety of properties and developed efficient algorithms related to orthologic, such as quadratic-time normal form computation, which have application in automated reasoning software. Orthologic-based reasoning is implemented in Lisa's kernel, where it makes proof shorter and mroe intuitive. It is also a part of the Stainless program verifier, increasing cache-hit ratio and simplifying formulas.
Lisa
Lisa is a general-purpose proof assistant based on set theory, for which I have developed a logical kernel, a proof interface and multiple proof-producing decision procedures (Tableaux, DPLL-like, congruence closure with e-graphs, OL-normalization...). I have studied and implemented embedding of type systems, in particular higher order logic, in first order logic with set theory. Lisa is designed around the six virtues of modern proof systems: efficiency, trust, usability, predictability, interoperability and programmability. One of the unique feature of Lisa is its proof and tactic language, which are entirely compatible with Lisa's host language (Scala).
Proof System for First Order Logic
In collaboration with Julie Cailler, I am developping SC-TPTP, a unified proof format for first order logic to allow interoperability between tools, in particular automated theorem provers and interactive theorem provers. SC-TPTP is an extension of the standard TPTP format used by automated theorem provers. Presently, Lisa, HOL Light, Lean, Goéland, Egg and Prover 9 are able to respectively import or output SC-TPTP proofs, and more tools are being worked on. I also hope that a unified proof format like SC-TPTP will allow to establish a large library of available proofs to train AI models. More generally, I believe in establishing archives of knowledge. Collaborations are more than welcome, so if the project is of interest to you, please do not hesitate to send an email.
Publications
Orthologic Type Systems
Mechanized HOL Reasoning in Set Theory
(Publisher)
(arXiv)
15th International Conference on Interactive
Theorem Proving (ITP 2024).
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
(publisher)
(infoscience)
9th Workshop on Practical Aspects of Automated Reasoning (PAAR 2024).
Orthologic With Axioms
(publisher)
(arXiv)
Proceedings of the ACM on Programming Languages (POPL 2024).
Interpolation and Quantifiers in Ortholattices
(publisher)
Verification, Model Checking, and AbstractInterpretation (VMCAI 2024).
LISA – A Modern Proof System
(publisher)
14th International Conference on Interactive
Theorem Proving (ITP 2023).
Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
(publisher)
(arXiv)
Tools and Algorithms for the Construction and Analysis of Systems (TACAS
2022).