Guillaume Burel

According to our database, Guillaume Burel authored at least 22 papers between 2006 and 2023.

Collaborative distances:

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

2023

Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory.

Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, Ronan Saillard

CoRR, 2023

2020

Linking Focusing and Resolution with Selection.

Guillaume Burel

ACM Trans. Comput. Log., 2020

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

2019

EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract).

Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

Teaching Formal Methods to Future Engineers.

Catherine Dubois, Virgile Prevosto, Guillaume Burel

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

2015

Translating HOL to Dedukti.

Ali Assaf, Guillaume Burel

Proceedings of the Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, 2015

A Completion Method to Decide Reachability in Rewrite Systems.

Guillaume Burel, Gilles Dowek, Ying Jiang

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

2014

Cut Admissibility by Saturation.

Guillaume Burel

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

2013

Detection of First Order Axiomatic Theories.

Guillaume Burel, Simon Cruanes

Proceedings of the Frontiers of Combining Systems, 2013

A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo.

Guillaume Burel

Proceedings of the Third International Workshop on Proof Exchange for Theorem Proving, 2013

2012

CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo.

Mathieu Boespflug, Guillaume Burel

Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, 2012

2011

Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

Guillaume Burel

Log. Methods Comput. Sci., 2011

Experimenting with Deduction Modulo.

Guillaume Burel

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Regaining cut admissibility in deduction modulo using abstract completion.

Guillaume Burel, Claude Kirchner

Inf. Comput., 2010

Embedding Deduction Modulo into a Prover.

Guillaume Burel

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2009

Bonnes démonstrations en déduction modulo. (Good proofs in deduction modulo).

Guillaume Burel

PhD thesis, 2009

How can we prove that a proof search method is not an instance of another?

Guillaume Burel, Gilles Dowek

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2009

Automating Theories in Intuitionistic Logic.

Guillaume Burel

Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

2008

A First-Order Representation of Pure Type Systems Using Superdeduction.

Guillaume Burel

Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

2007

Cut Elimination in Deduction Modulo by Abstract Completion.

Guillaume Burel, Claude Kirchner

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2007

Unbounded Proof-Length Speed-Up in Deduction Modulo.

Guillaume Burel

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

2006

Completion Is an Instance of Abstract Canonical System Inference.

Guillaume Burel, Claude Kirchner

Proceedings of the Algebra, Meaning, and Computation, 2006