Gaëtan Gilbert

According to our database, Gaëtan Gilbert authored at least 9 papers between 2015 and 2024.

Collaborative distances:

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

2024

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2022

The Advantages of Maintaining a Multitask, Project-Specific Bot: An Experience Report.

Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert

IEEE Softw., 2022

Advantages of maintaining a multi-task project-specific bot: an experience report.

Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert

CoRR, 2022

2021

Extending the team with a project-specific bot.

Théo Zimmermann, Julien Coolen, Jason Gross, Pierre-Marie Pédrot, Gaëtan Gilbert

CoRR, 2021

2019

A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle).

Gaëtan Gilbert

PhD thesis, 2019

Definitional proof-irrelevance without K.

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau

Proc. ACM Program. Lang., 2019

2017

Formalising real numbers in homotopy type theory.

Gaëtan Gilbert

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

Design and Implementation of the Andromeda Proof Assistant.

Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

2015

Normalisation by Completeness with Heyting Algebras.

Gaëtan Gilbert, Olivier Hermant

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015