Completion Is an Instance of Abstract Canonical System Inference. - Guillaume Burel; Claude Kirchner (Essays Dedicated to Joseph A. Goguen, 2006)

Unbounded Proof-Length Speed-Up in Deduction Modulo. - Guillaume Burel (CSL, 2007)

Cut Elimination in Deduction Modulo by Abstract Completion. - Guillaume Burel; Claude Kirchner (LFCS, 2007)

A First-Order Representation of Pure Type Systems Using Superdeduction. - Guillaume Burel (LICS, 2008)

Automating Theories in Intuitionistic Logic. - Guillaume Burel (FroCoS, 2009)

How can we prove that a proof search method is not an instance of another? - Guillaume Burel; Gilles Dowek (LFMTP, 2009)

Bonnes démonstrations en déduction modulo. (Good proofs in deduction modulo). - Guillaume Burel (2009)

Embedding Deduction Modulo into a Prover. - Guillaume Burel (CSL, 2010)

Regaining cut admissibility in deduction modulo using abstract completion. - Guillaume Burel; Claude Kirchner (Inf. Comput., 2010)

Experimenting with Deduction Modulo. - Guillaume Burel (CADE, 2011)

Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo - Guillaume Burel (Log. Methods Comput. Sci., 2011)

CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. - Mathieu Boespflug; Guillaume Burel (PxTP, 2012)

A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. - Guillaume Burel (PxTP@CADE, 2013)

Detection of First Order Axiomatic Theories. - Guillaume Burel; Simon Cruanes (FroCos, 2013)

Cut Admissibility by Saturation. - Guillaume Burel (RTA-TLCA, 2014)

A Completion Method to Decide Reachability in Rewrite Systems. - Guillaume Burel; Gilles Dowek; Ying Jiang 001 (FroCos, 2015)

Translating HOL to Dedukti. - Ali Assaf 002; Guillaume Burel (PxTP@CADE, 2015)

Teaching Formal Methods to Future Engineers. - Catherine Dubois; Virgile Prevosto; Guillaume Burel (FMTea, 2019)

EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). - Mohamed Yacine El Haddad; Guillaume Burel; Frédéric Blanqui (PxTP, 2019)

First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice. - Guillaume Burel; Guillaume Bury; Raphaël Cauderlier; David Delahaye; Pierre Halmagrand; Olivier Hermant (J. Autom. Reason., 2020)

Linking Focusing and Resolution with Selection. - Guillaume Burel (ACM Trans. Comput. Log., 2020)

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. - Ali Assaf 002; Guillaume Burel; Raphaël Cauderlier; David Delahaye; Gilles Dowek; Catherine Dubois; Frédéric Gilbert 002; Pierre Halmagrand; Olivier Hermant; Ronan Saillard (CoRR, 2023)

Proof Verification with GDV and LambdaPi - It's a Matter of Trust. - Geoff Sutcliffe; Frédéric Blanqui; Guillaume Burel (FLAIRS, 2025)