Martin Desharnais-Schäfer

According to our database, Martin Desharnais-Schäfer authored at least 24 papers between 2017 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

A Formalization of the Exponential Blowup in the Transformations between CNF and DNF.

Leon Raffael Schulz, Martin Desharnais-Schäfer, Jan Johannsen

Arch. Formal Proofs, 2026

Adding Sorts to an Isabelle Formalization of Superposition.

Balázs Tóth, Martin Desharnais-Schäfer, Jasmin Blanchette

Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2026

2025

Formal verification of logical calculi and simulations in Isabelle/HOL. (Vérification formelle des calculs logiques et des simulations dans Isabelle/HOL).

Martin Desharnais

PhD thesis, 2025

Sledgehammering Without ATPs (Short Paper).

Martin Desharnais, Jasmin Blanchette

Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

A Stepwise Refinement Proof that SCL(FOL) Simulates Ground Ordered Resolution.

Martin Bromberger, Martin Desharnais, Christoph Weidenbach

Proceedings of the Automated Deduction - CADE 30, 2025

2024

IsaFoL/Superposition_Calculus.

Martin Desharnais, Balázs Tóth

Dataset, November, 2024

The CADE-29 Automated Theorem Proving System Competition - CASC-29.

Geoff Sutcliffe, Martin Desharnais

AI Commun., 2024

A Modular Formalization of Superposition.

Martin Desharnais, Balázs Tóth

Arch. Formal Proofs, 2024

SCL Simulates Nonredundant Ground Resolution.

Martin Desharnais

Arch. Formal Proofs, 2024

Minimal, Maximal, Least, and Greatest Elements w.r.t. Restricted Ordering.

Martin Desharnais

Arch. Formal Proofs, 2024

Abstract Substitution.

Martin Desharnais

Arch. Formal Proofs, 2024

A Modular Formalization of Superposition in Isabelle/HOL.

Martin Desharnais, Balázs Tóth, Uwe Waldmann, Jasmin Blanchette, Sophie Tourret

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

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

The 11th IJCAR automated theorem proving system competition - CASC-J11.

Geoff Sutcliffe, Martin Desharnais

AI Commun., 2023

A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic.

Martin Desharnais

Arch. Formal Proofs, 2023

An Isabelle/HOL Formalization of the SCL(FOL) Calculus.

Martin Bromberger, Martin Desharnais, Christoph Weidenbach

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Seventeen Provers Under the Hammer.

Martin Desharnais, Petar Vukmirovic, Jasmin Blanchette, Makarius Wenzel

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

The CADE-28 Automated Theorem Proving System Competition - CASC-28.

Geoff Sutcliffe, Martin Desharnais

AI Commun., 2021

Abstract: Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant.

Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais

Proceedings of the 19th International Workshop on Satisfiability Modulo Theories co-located with 33rd International Conference on Computer Aided Verification(CAV 2021), 2021

Towards efficient and verified virtual machines for dynamic languages.

Martin Desharnais, Stefan Brunthaler

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant.

Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Inline Caching and Unboxing Optimization for Interpreters.

Martin Desharnais

Arch. Formal Proofs, 2020

A Generic Framework for Verified Compilers.

Martin Desharnais

Arch. Formal Proofs, 2020

2017

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, Christian Sternagel, René Thiemann, Dmitriy Traytel

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017