Guillaume Burel

25 papers A* 1A 1B 3Misc 2Journal 6Unranked 11
YearRankTypeTitle / Venue / Authors
2025 Misc conf
Proof Verification with GDV and LambdaPi - It's a Matter of Trust.
FLAIRS
Geoff Sutcliffe, Frédéric Blanqui, Guillaume Burel
2023 J jnl
Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory.
CoRR
Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard
2023 J jnl
How can we prove that a proof search method is not an instance of another?
CoRR
Guillaume Burel, Gilles Dowek
2020 J jnl
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice.
J. Autom. Reason.
Guillaume Burel, Guillaume Bury, Raphaël Cauderlier, David Delahaye, Pierre Halmagrand, Olivier Hermant
2020 J jnl
Linking Focusing and Resolution with Selection.
ACM Trans. Comput. Log.
Guillaume Burel
2019 — conf
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract).
PxTP
Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui
2019 — conf
Teaching Formal Methods to Future Engineers.
FMTea
Catherine Dubois, Virgile Prevosto, Guillaume Burel
2018 B conf
Linking Focusing and Resolution with Selection.
MFCS
Guillaume Burel
2015 — conf
A Completion Method to Decide Reachability in Rewrite Systems.
FroCos
Guillaume Burel, Gilles Dowek, Ying Jiang
2015 — conf
Translating HOL to Dedukti.
PxTP@CADE
Ali Assaf, Guillaume Burel
2014 — conf
Cut Admissibility by Saturation.
RTA-TLCA
Guillaume Burel
2013 — conf
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo.
PxTP@CADE
Guillaume Burel
2013 — conf
Detection of First Order Axiomatic Theories.
FroCos
Guillaume Burel, Simon Cruanes
2012 — conf
CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo.
PxTP
Mathieu Boespflug, Guillaume Burel
2011 J jnl
Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
Log. Methods Comput. Sci.
Guillaume Burel
2011 A conf
Experimenting with Deduction Modulo.
CADE
Guillaume Burel
2010 B conf
Embedding Deduction Modulo into a Prover.
CSL
Guillaume Burel
2010 J jnl
Regaining cut admissibility in deduction modulo using abstract completion.
Inf. Comput.
Guillaume Burel, Claude Kirchner
2009 — conf
Automating Theories in Intuitionistic Logic.
FroCoS
Guillaume Burel
2009 — —
Bonnes démonstrations en déduction modulo. (Good proofs in deduction modulo).
Guillaume Burel
2009 — conf
How can we prove that a proof search method is not an instance of another?
LFMTP
Guillaume Burel, Gilles Dowek
2008 A* conf
A First-Order Representation of Pure Type Systems Using Superdeduction.
LICS
Guillaume Burel
2007 Misc conf
Cut Elimination in Deduction Modulo by Abstract Completion.
LFCS
Guillaume Burel, Claude Kirchner
2007 B conf
Unbounded Proof-Length Speed-Up in Deduction Modulo.
CSL
Guillaume Burel
2006 — conf
Completion Is an Instance of Abstract Canonical System Inference.
Essays Dedicated to Joseph A. Goguen
Guillaume Burel, Claude Kirchner