Simon Guilloud
EPFL IC IINFCOM LARA
INR 318 (Bâtiment INR)
Station 14
1015 Lausanne
Web site: Web site: https://lara.epfl.ch
Current work
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.
Biography
I 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.
Publications
Infoscience publications
2025
Working Papers
* Verified and Optimized Implementation of Orthologic Proof Search
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical propositional logic in automated reasoning tools. We formalize, in the Coq proof assistant, a proof system in sequent-calculus style for orthologic. We then prove its soundness and completeness with respect to the algebraic variety of ortholattices, and we formalize a cut-elimination theorem (in doing so, we discover and fix a missing case in a previously published proof). We then implement and verify a complete proof search procedure for orthologic. A naive implementation is exponential, and to obtain an optimal quadratic runtime, we optimize the implementation by memoizing its results and simulating reference equality testing. We leverage the resulting correctness theorem to implement a reflective Coq tactic. We present benchmarks showing the procedure, under various optimizations, matches its theoretical complexity. Finally, we develop tactics including normalization with respect to orthologic and a boolean solver, which we also benchmark. We make tactics available as a standalone Coq plugin.
2025* Interoperability of Proof Systems with SC-TPTP
We introduce SC-TPTP, an extension of the TPTP derivation format that encompasses sequent formalism, enabling seamless proof exchange between interactive theorem provers and first-order automated theorem provers. We provide a way to represent non-deductive steps-Skolemization, clausification, and Tseitin normal form-as deductive steps within the format. Building upon the existing support in the Lisa proof assistant and the Goéland theorem prover, SC-TPTP ecosystem is further enhanced with proof output interfaces for Egg and Prover9, as well as proof reconstruction support for HOL Light, Lean, and Rocq.
20252024
Conference Papers
* Interpolation and Quantifiers in Ortholattices
We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based proof system for quantified orthologic, which we prove sound and complete for the class of all complete ortholattices. We show that orthologic does not admit quantifier elimination in general. Despite that, we show that interpolants always exist in orthologic. We give an algorithm to compute interpolants efficiently. We expect our result to be useful to quickly establish unreachability as a component of verification algorithms.
2024. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024), London, United Kingdom, January 15-16, 2024.* Mechanized HOL Reasoning in Set Theory
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assume traditional FOL syntax without notation for term-level binders. To embed $\lambda$-terms, we define a notion of context, defining the closure of all abstractions occuring inside a term. We implement the embedding in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory (presented at ITP 2023). We show how to implement type checking and the proof steps of HOL Light as proof-producing tactics in Lisa. The embedded HOL theorems and proofs are interoperable with the existing Lisa library. This yields a form of soft type system supporting top-level polymorphism and ADTs within set theory. The approach offers tools for Lisa users to carry HOL-style proofs within set theory. It also enables the import of HOL Light theorem statements into Lisa, as well as the replay of small HOL Light kernel proofs.
2024. 15th International Conference on Interactive Theorem Proving (ITP 2024), Tbilisi, Georgia, September 9-14, 2024.* Interpolation and Quantifiers in Ortholattices
We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based proof system for quantified orthologic, which we prove sound and complete for the class of all complete ortholattices. We show that orthologic does not admit quantifier elimination in general. Despite that, we show that interpolants always exist in orthologic. We give an algorithm to compute interpolants efficiently. We expect our result to be useful to quickly establish unreachability as a component of verification algorithms.
2024. 25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), London, ENGLAND, JAN 15-16, 2024. p. 235 - 257. DOI : 10.1007/978-3-031-50524-9_11.* SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-order logic: SC-TPTP. To avoid multiplication of standards, our proposed format over-specifies the TPTP derivation format by focusing on sequent formalisms. By doing so, it provides a high level of detail, is faithful to mathematical tradition, and cover multiple existing tools and in particular tableaux-based strategies. We make use of this format to allow the Lisa proof assistant to query the Goéland automated theorem prover , and implement a library of tools able to parse, print and check SC-TPTP proofs, export them into Coq files, and rebuild low-level proof steps from advanced ones.
2024. 9th Workshop on Practical Aspects of Automated Reasoning, Nancy, France, July 2, 2024.* Orthologic with Axioms
We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polynomial-time equivalence checking that is sound with respect to Boolean algebra semantics. We generalize ortholattice reasoning and obtain an algorithm for proving a larger class of classically valid formulas. As the key result, we analyze a proof system for orthologic augmented with axioms. An important feature of the system is that it limits the number of formulas in a sequent to at most two, which makes the extension with axioms non-trivial. We show a generalized form of cut elimination for this system, which implies a sub-formula property. From there we derive a cubic-time algorithm for provability from axioms, or equivalently, for validity in finitely presented ortholattices. We further show that propositional resolution of width 5 proves all formulas provable in orthologic with axioms. We show that orthologic system subsumes resolution of width 2 and arbitrarily wide unit resolution and is complete for reasoning about generalizations of propositional Horn clauses. Moving beyond ground axioms, we introduce effectively propositional orthologic (by analogy with EPR for classical logic), presenting its semantics as well as a sound and complete proof system. Our proof system implies the decidability of effectively propositional orthologic, as well as its fixed-parameter tractability for a bounded maximal number of variables in each axiom. As a special case, we obtain a generalization of Datalog with negation and disjunction.
2024. 51st ACM SIGPLAN Symposium on Principles of Programming Languages, London, United Kingdom, 2024-01-17 - 2024-01-19. DOI : 10.1145/3632881.2023
Conference Papers
* LISA – A Modern Proof System
We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and function symbols. It implements polynomial-time proof checking and uses the axioms of ortholattices (which implies the irrelevance of the order of conjuncts and disjuncts and additional propositional laws). The kernel supports the notion of theorems (whose proofs are not expanded), as well as definitions of predicate symbols and objects whose unique existence is proven. A domain-specific language enables construction of proofs and development of proof tactics with user-friendly tools and presentation, while remaining within the general-purpose language, Scala. We describe the LISA proof system and illustrate the flavour and the level of abstraction of proofs written in LISA. This includes a proof-generating tactic for propositional tautologies, leveraging the ortholattice properties to reduce the size of proofs. We also present early formalization of set theory in LISA, including Cantor's theorem.
2023. 14th Conference on Interactive Theorem Proving, Białystok, Poland, 2023, July 31 - August 4, 2023. DOI : 10.4230/LIPIcs.ITP.2023.17.* Formula Normalizations in Verification
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.
2023. 35th International Conference on Computer Aided Verification, Paris, France.2022
Conference Papers
* 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.