Accéder directement au contenu
NT

Nicolas Tabareau

4
Documents

Présentation

Publications

gaetan-gilbert
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

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
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

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