My main domains of research are proof assistants and algorithms for logic-related problems.
I also have interests in various areas of computer science and mathematics and their applicability in proof systems such as probabilistic proofs, type theory, quantum computing and more.

My main domains of research are proof assistants and algorithms for logic-related problems.
I also have interests in various areas of computer science and mathematics and their applicability in proof systems such as probabilistic proofs, type theory, quantum computing and more.

My recent and current research focuses on the following topics:
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).
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. More recently, I have studied the applicability of orthologic as a basis to type systems with union and disjunction types.