Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. - Julian Biendarra; Jasmin Christian Blanchette; Aymeric Bouzy; Martin Desharnais; Mathias Fleury; Johannes Hölzl; Ondrej Kuncar; Andreas Lochbihler; Fabian Meier; Lorenz Panny; Andrei Popescu 001; Christian Sternagel; et al. (FroCoS, 2017)

A Generic Framework for Verified Compilers. - Martin Desharnais (Arch. Formal Proofs, 2020)

Inline Caching and Unboxing Optimization for Interpreters. - Martin Desharnais (Arch. Formal Proofs, 2020)

Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant. - Hans-Jörg Schurr; Mathias Fleury; Martin Desharnais (CADE, 2021)

Towards efficient and verified virtual machines for dynamic languages. - Martin Desharnais; Stefan Brunthaler 001 (CPP, 2021)

Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant. - Hans-Jörg Schurr; Mathias Fleury; Martin Desharnais (SMT, 2021)

The CADE-28 Automated Theorem Proving System Competition - CASC-28. - Geoff Sutcliffe; Martin Desharnais (AI Commun., 2021)

Seventeen Provers Under the Hammer. - Martin Desharnais; Petar Vukmirovic; Jasmin Blanchette; Makarius Wenzel (ITP, 2022)

An Isabelle/HOL Formalization of the SCL(FOL) Calculus. - Martin Bromberger; Martin Desharnais; Christoph Weidenbach (CADE, 2023)

A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic. - Martin Desharnais (Arch. Formal Proofs, 2023)

The 11th IJCAR automated theorem proving system competition - CASC-J11. - Geoff Sutcliffe; Martin Desharnais (AI Commun., 2023)

The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471). - Maria Paola Bonacina; Pascal Fontaine; Cláudia Nalon; Claudia Schon; Martin Desharnais (Dagstuhl Reports, 2023)

A Modular Formalization of Superposition in Isabelle/HOL. - Martin Desharnais; Balázs Tóth; Uwe Waldmann; Jasmin Blanchette; Sophie Tourret (ITP, 2024)

Abstract Substitution. - Martin Desharnais (Arch. Formal Proofs, 2024)

Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering. - Martin Desharnais (Arch. Formal Proofs, 2024)

SCL Simulates Nonredundant Ground Resolution. - Martin Desharnais (Arch. Formal Proofs, 2024)

A Modular Formalization of Superposition. - Martin Desharnais; Balázs Tóth (Arch. Formal Proofs, 2024)

The CADE-29 Automated Theorem Proving System Competition - CASC-29. - Geoff Sutcliffe; Martin Desharnais (AI Commun., 2024)

IsaFoL/Superposition_Calculus. - Martin Desharnais; Balázs Tóth (DROPS Artifacts, 2024)

A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution. - Martin Bromberger; Martin Desharnais; Christoph Weidenbach (CADE, 2025)