Gaëtan Gilbert

13 papers B 3Journal 8Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
The Rewster: Type Preserving Rewrite Rules for the Rocq Prover.
J. Autom. Reason.
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
2025 J jnl
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants.
Proc. ACM Program. Lang.
Josselin Poiret, Gaëtan Gilbert, Kenji Maillard, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter
2024 B conf
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.
ITP
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
2022 J jnl
Advantages of maintaining a multi-task project-specific bot: an experience report.
CoRR
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
2022 J jnl
The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report.
IEEE Softw.
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
2021 J jnl
Extending the team with a project-specific bot.
CoRR
Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert
2019 — —
A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle).
Gaëtan Gilbert
2019 J jnl
Definitional proof-irrelevance without K.
Proc. ACM Program. Lang.
Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau
2018 J jnl
Design and Implementation of the Andromeda Proof Assistant.
CoRR
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone
2017 B conf
Formalising real numbers in homotopy type theory.
CPP
Gaëtan Gilbert
2016 — conf
Design and Implementation of the Andromeda Proof Assistant.
TYPES
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone
2016 J jnl
Formalising Real Numbers in Homotopy Type Theory.
CoRR
Gaëtan Gilbert
2015 B conf
Normalisation by Completeness with Heyting Algebras.
LPAR
Gaëtan Gilbert, Olivier Hermant