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.
Research
My current research and my doctoral thesis focus on two aspects:
Orthologic
Orthologic is a weakening of propositional logic where the law of distributivity does not necessarily hold. It has low-complexity decision procedure and interesting logical properties, making it a strong candidate to predictably and efficiently approximate propositional logic.
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...)
Publications
Mechanized HOL Reasoning in Set Theory
15th International Conference on Interactive Theorem Proving (ITP 2024).
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
9th Workshop on Practical Aspects of Automated Reasoning (PAAR 2024).
Interpolation and Quantifiers in Ortholattices
Verification, Model Checking, and Abstract Interpretation (VMCAI 2024).
LISA - A Modern Proof System
14th International Conference on Interactive Theorem Proving (ITP 2023).
Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022).