Guillaume Burel

École Nationale Supérieure d’Informatique pour l’Industrie et l’Entreprise — France

Computer Science · Physical Sciences

8h-index166citations41works0.02yr avg
OpenAlex↗Google Scholar↗Lab page↗

Accepting Students?

No reports yet. Know if this professor is taking students?

Research Topics

Logic, programming, and type systems(35), Logic, Reasoning, and Knowledge(26), Formal Methods in Verification(17), Semantic Web and Ontologies(7), Security and Verification in Computing(3)

Publications41 total

Automatically translating proof systems for SMT solvers to the λΠ-calculus
SPIRE - Sciences Po Institutional REpository·2025
Proof Verification with GDV and LambdaPi - It's a Matter of Trust
Proceedings of the ... International Florida Artificial Intelligence Research Society Conference·2025Open Access
Dedukti: a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory
arXiv (Cornell University)·2023· 4 citedOpen Access
Dedukti: a Logical Framework based on the $\\lambda$$\\Pi$-Calculus Modulo\n Theory
arXiv (Cornell University)·2023· 1 citedOpen Access
How can we prove that a proof search method is not an instance of another?
arXiv (Cornell University)·2023Open Access
Linking Focusing and Resolution with Selection
ACM Transactions on Computational Logic·2020· 1 citedOpen Access
First-Order Automated Reasoning with Theories: When Deduction Modulo Theory Meets Practice
Journal of Automated Reasoning·2019· 9 cited
Teaching Formal Methods to Future Engineers
Lecture notes in computer science·2019· 4 citedOpen Access
A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo
EPiC series in computing·2018· 3 citedOpen Access
Linking Focusing and Resolution with Selection
DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)·2018Open Access
Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system
SPIRE - Sciences Po Institutional REpository·2016· 2 cited
Automata, Resolution, and Cut-elimination
SPIRE - Sciences Po Institutional REpository·2016Open Access
A Completion Method to Decide Reachability in Rewrite Systems
Lecture notes in computer science·2015· 1 citedOpen Access
Cut Admissibility by Saturation
Lecture notes in computer science·2014· 3 citedOpen Access
A Shallow Embedding of Resolution and Superposition Proofs into the ??-Calculus Modulo
HAL (Le Centre pour la Communication Scientifique Directe)·2013
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo
2013· 12 citedOpen Access
Detection of First Order Axiomatic Theories
Lecture notes in computer science·2013· 2 citedOpen Access
CoqInE : Translating the calculus of inductive constructions into the ??-calculus modulo.
HAL (Le Centre pour la Communication Scientifique Directe)·2012· 8 cited
Consistency Implies Cut Admissibility
2011· 1 citedOpen Access
Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
Logical Methods in Computer Science·2011· 3 citedOpen Access
page 1 of 3Next →

Frequent Co-authors

Claude Kirchner(9), Gilles Dowek(8), David Delahaye(4), Pierre Halmagrand(4), Olivier Hermant(4), Catherine Dubois(4), Raphaël Cauderlier(3), Ali Assaf(3), Frédéric Gilbert(3), Ronan Saillard(3), Frédéric Blanqui(3), Mathieu Boespflug(2), Ying Jiang(2), Horatiu Cirstea(2), Guillaume Bury(1), Virgile Prévosto(1), Raphal Cauderlier(1), Simon Cruanes(1), Florent Garnier(1), Colin Riba(1)