Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

7 résultats
Page :
triés par
Image document

Definitional Proof-Irrelevance without K

 Gaëtan Gilbert , Jesper Cockx , Matthieu Sozeau , Nicolas Tabareau
Proceedings of the ACM on Programming Languages, 2019, POPL'19, pp.1-28. ⟨10.1145/329031610.1145/3290316⟩
Article dans une revue hal-01859964v2
Image document

Formalising Real Numbers in Homotopy Type Theory

 Gaëtan Gilbert
6th ACM SIGPLAN Conference on Certified Programs and Proofs , Jan 2017, Paris, France. pp.112 - 124, ⟨10.1145/3018610.3018614⟩
Communication dans un congrès hal-01449326v1
Image document

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 Software, 2022, pp.2-7. ⟨10.1109/MS.2022.3179773⟩
Article dans une revue hal-03479327v2
Image document

Normalization by Completeness with Heyting Algebras

 Gaëtan Gilbert , Olivier Hermant
LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji
Communication dans un congrès hal-01204599v1
Image document

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

 Yann Leray , Gaëtan Gilbert , Nicolas Tabareau , Théo Winterhalter
2024
Pré-publication, Document de travail hal-04511667v1
Image document

The Rewster: The Coq Proof Assistant with Rewrite Rules

 Gaëtan Gilbert , Yann Leray , Nicolas Tabareau , Théo Winterhalter
TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-3
Communication dans un congrès hal-04403667v1
Image document

From Lost to the River: Embracing Sort Proliferation

 Gaëtan Gilbert , Pierre-Marie Pédrot , Matthieu Sozeau , Nicolas Tabareau
TYPES 2023 - 29th International Conference on Types for Proofs and Programs, Jun 2023, Valencia, Spain. pp.1-2
Communication dans un congrès hal-04378939v1
Page :