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, Goéland and Egg 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 (and simply because I believe in establishing archive 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

2025
Preprint

Interoperability of Proof Systems with SC-TPTP (Preprint)
Simon Guilloud,Julie Cailler, Sankalp Gambhir, Auguste Poiroux, Yann Herklotz, Thomas Bourgeat.

2024
ITP

Mechanized HOL Reasoning in Set Theory
Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kunčak.
15th International Conference on Interactive Theorem Proving (ITP 2024).

PAAR

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
Julie Cailler, Simon Guilloud.
9th Workshop on Practical Aspects of Automated Reasoning (PAAR 2024).

POPL

Orthologic With Axioms
Simon Guilloud, Viktor Kunčak.
Proceedings of the ACM on Programming Languages (POPL 2024).

VMCAI

Interpolation and Quantifiers in Ortholattices
Simon Guilloud, Sankalp Gambhir, Viktor Kunčak.
Verification, Model Checking, and Abstract Interpretation (VMCAI 2024).

2023
ITP

LISA – A Modern Proof System
Simon Guilloud, Sankalp Gambhir, Andrea Gilot, Viktor Kunčak.
14th International Conference on Interactive Theorem Proving (ITP 2023).

CAV

Formula Normalizations in Verification
Simon Guilloud, Mario Bucev, Dragana Milovančević, Viktor Kunčak.
Computer Aided Verification (CAV 2023).

2022
TACAS

Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time
Simon Guilloud, Viktor Kunčak.
Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022).