Fields of expertise
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.
Current workMy main current work consists in designing and developping the LISA proof assistant (work in progress).
I also study applicability of decision procedures and datastructures for lattice-like algebras as partial solutions for propositional logic problems.
BiographyI am a PhD student at EPFL working in the Laboratory of Automated Reasoning and Analysis with Prof. Viktor Kunčak.
I have previously completed my Bachelor and Master degree at EPFL and made an internship in quantum computing.
* Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
We present a quasilinear time algorithm to decide the word problem on a natural algebraic structures we call orthocomplemented bisemilattices, a subtheory of boolean algebra. We use as a base a variation of Hopcroft, Ullman and Aho algorithm for tree isomorphism which we combine with a term rewriting system to decide equivalence of two terms. We prove that the rewriting system is terminating and confluent and hence the existence of a normal form, and that our algorithm is computing it. We also discuss applications and present an effective implementation in Scala.2022. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (ETAPS 2022), Munich, Germany, April 2-7, 2022. p. 196-214. DOI : 10.1007/978-3-030-99527-0_11.
* On Polynomial Algorithms for Normalizing Formulas
We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem for two subtheories of Boolean algebra, giving a sound procedure for propositional logical equivalence that is incomplete in general but complete with respect to a subset of Boolean algebra axioms. We first show a new algorithm to produce a normal form for expressions in the theory of ortholattices (OL) in time O(n^2). We also consider an algorithm, recently presented but never evaluated in practice, producing a normal form for a slightly weaker theory, orthocomplemented bisemilattices (OCBSL), in time O(n log(n)^2). For both algorithms, we present an implementation and show efficiency in two domains. First, we evaluate the algorithms on large propositional expressions, specifically combinatorial circuits from a benchmark suite, as well as on large random formulas. Second, we implement and evaluate the algorithms in the Stainless verifier, a tool for verifying the correctness of Scala programs. We used these algorithms as a basis for a new formula simplifier, which is applied before valid verification conditions are saved into a persistent cache. The results show that normalization substantially increases cache hit ratio in large benchmarks.2022-10-14