Martin Desharnais

20 papers A 3B 4Journal 11Unranked 2
YearRankTypeTitle / Venue / Authors
2025 A conf
A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution.
CADE
Martin Bromberger, Martin Desharnais, Christoph Weidenbach
2025 B conf
Sledgehammering Without ATPs (Short Paper).
ITP
Martin Desharnais, Jasmin Blanchette
2024 B conf
A Modular Formalization of Superposition in Isabelle/HOL.
ITP
Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret
2024 J jnl
A Modular Formalization of Superposition.
Arch. Formal Proofs
Martin Desharnais, Balázs Tóth
2024 J jnl
Abstract Substitution.
Arch. Formal Proofs
Martin Desharnais
2024 J jnl
Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering.
Arch. Formal Proofs
Martin Desharnais
2024 J jnl
SCL Simulates Nonredundant Ground Resolution.
Arch. Formal Proofs
Martin Desharnais
2024 J jnl
The CADE-29 Automated Theorem Proving System Competition - CASC-29.
AI Commun.
Geoff Sutcliffe, Martin Desharnais
2023 J jnl
A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic.
Arch. Formal Proofs
Martin Desharnais
2023 A conf
An Isabelle/HOL Formalization of the SCL(FOL) Calculus.
CADE
Martin Bromberger, Martin Desharnais, Christoph Weidenbach
2023 J jnl
The 11th IJCAR automated theorem proving system competition - CASC-J11.
AI Commun.
Geoff Sutcliffe, Martin Desharnais
2023 J jnl
The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471).
Dagstuhl Reports
Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, Martin Desharnais
2022 B conf
Seventeen Provers Under the Hammer.
ITP
Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel
2021 — conf
Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant.
SMT
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
2021 A conf
Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant.
CADE
Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais
2021 J jnl
The CADE-28 Automated Theorem Proving System Competition - CASC-28.
AI Commun.
Geoff Sutcliffe, Martin Desharnais
2021 B conf
Towards efficient and verified virtual machines for dynamic languages.
CPP
Martin Desharnais, Stefan Brunthaler
2020 J jnl
A Generic Framework for Verified Compilers.
Arch. Formal Proofs
Martin Desharnais
2020 J jnl
Inline Caching and Unboxing Optimization for Interpreters.
Arch. Formal Proofs
Martin Desharnais
2017 — conf
Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic.
FroCoS
Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, Dmitriy Traytel