Gaëtan Gilbert

According to our database1, Gaëtan Gilbert authored at least 10 papers between 2015 and 2025.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of five.

Timeline

2016
2018
2020
2022
2024
0
1
2
3
1
2
1
1
1
1
1
1
1

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2025
All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants.
Proc. ACM Program. Lang., 2025

2024
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.
Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

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

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

2021
Extending the team with a project-specific bot.
CoRR, 2021

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

Definitional proof-irrelevance without K.
Proc. ACM Program. Lang., 2019

2017
Formalising real numbers in homotopy type theory.
Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016
Design and Implementation of the Andromeda Proof Assistant.
Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

2015
Normalisation by Completeness with Heyting Algebras.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015


  Loading...