Equivalence Checking for Orthocomplemented Bisemilattices in Log-Linear Time. - Simon Guilloud; Viktor Kuncak (TACAS (2), 2022)

Formula Normalizations in Verification. - Simon Guilloud; Mario Bucev; Dragana Milovancevic; Viktor Kuncak (CAV (3), 2023)

LISA - A Modern Proof System. - Simon Guilloud; Sankalp Gambhir; Viktor Kuncak (ITP, 2023)

Mechanized HOL Reasoning in Set Theory. - Simon Guilloud; Sankalp Gambhir; Andrea Gilot; Viktor Kuncak (ITP, 2024)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus. - Julie Cailler; Simon Guilloud (PAAR+SC²@IJCAR, 2024)

Interpolation and Quantifiers in Ortholattices. - Simon Guilloud; Sankalp Gambhir; Viktor Kuncak (VMCAI (1), 2024)

Orthologic with Axioms. - Simon Guilloud; Viktor Kuncak (Proc. ACM Program. Lang., 2024)

epfl-lara/lisa. - Simon Guilloud; Sankalp Gambhir; Andrea Gilot; Viktor Kuncak (DROPS Artifacts, 2024)

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

Verified and Optimized Implementation of Orthologic Proof Search. - Simon Guilloud; Clément Pit-Claudel (CAV (3), 2025)

Orthologic Type Systems. - Simon Guilloud; Viktor Kuncak (CoRR, 2025)