The metacoq project M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ...
Journal of automated reasoning 64 (5), 947-999, 2020
135 2020 Coq coq correct! verification of type checking and erasure for coq, in coq M Sozeau, S Boulier, Y Forster, N Tabareau, T Winterhalter
Proceedings of the ACM on Programming Languages 4 (POPL), 1-28, 2019
121 2019 Ssprove: A foundational framework for modular cryptographic proofs in coq C Abate, PG Haselwarter, E Rivas, A Van Muylder, T Winterhalter, ...
2021 IEEE 34th Computer Security Foundations Symposium (CSF), 1-15, 2021
45 2021 The taming of the rew: a type theory with computational assumptions J Cockx, N Tabareau, T Winterhalter
Proceedings of the ACM on Programming Languages 5 (POPL), 1-29, 2021
41 2021 Eliminating reflection from type theory T Winterhalter, M Sozeau, N Tabareau
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
41 2019 Normalization by evaluation for sized dependent types A Abel, A Vezzosi, T Winterhalter
Proceedings of the ACM on Programming Languages 1 (ICFP), 1-30, 2017
37 * 2017 Formalisation and meta-theory of type theory T Winterhalter
Nantes, 2020
22 2020 SSProve: A foundational framework for modular cryptographic proofs in Coq PG Haselwarter, E Rivas, A Van Muylder, T Winterhalter, C Abate, ...
ACM Transactions on Programming Languages and Systems 45 (3), 1-61, 2023
15 2023 Correct and Complete Type Checking and Certified Erasure for Coq , in Coq M Sozeau, Y Forster, M Lennon-Bertrand, J Nielsen, N Tabareau, ...
Journal of the ACM 72 (1), 1-74, 2025
14 2025 Randomized mixed-radix scalar multiplication E Guerrini, L Imbert, T Winterhalter
IEEE Transactions on Computers 67 (3), 418-431, 2017
8 2017 The last yard: Foundational end-to-end verification of high-speed cryptography PG Haselwarter, BS Hvass, LL Hansen, T Winterhalter, C Hriţcu, ...
Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024
6 2024 Securing Verified IO Programs Against Unverified Code in F CC Andrici, Ș Ciobâcă, C Hriţcu, G Martínez, E Rivas, É Tanter, ...
Proceedings of the ACM on Programming Languages 8 (POPL), 2226-2259, 2024
4 2024 Composable partial functions in Coq, totally for free T Winterhalter
29th International Conference on Types for Proofs and Programs, 2023
4 2023 Partial dijkstra monads for all T Winterhalter, CC Andrici, C Hriţcu, K Maillard, G Martínez, E Rivas
Proceedings of the International Conference on Types for Proofs and Programs …, 2022
4 2022 How to tame your rewrite rules J Cockx, N Tabareau, T Winterhalter
Types for Proofs and Programs, TYPES, 2019
4 2019 Randomizing scalar multiplication using exact covering systems of congruences E Guerrini, L Imbert, T Winterhalter
Cryptology ePrint Archive, 2015
4 2015 The Rewster: The Coq Proof Assistant with Rewrite Rules G Gilbert, Y Leray, N Tabareau, T Winterhalter
TYPES 2023-29th International Conference on Types for Proofs and Programs, 1-3, 2023
3 2023 Using reflection to eliminate reflection T Winterhalter, M Sozeau, N Tabareau
TYPES 2018, 90, 2018
3 2018 Towards a logical framework modulo rewriting and equational theories B Barras, T Felicissimo, T Winterhalter
30th International Conference on Types for Proofs and Programs (TYPES 2024 …, 2024
1 2024 From Rewrite Rules to Axioms in the V Blot, G Dowek, T Traversié, T Winterhalter
International Conference on Foundations of Software Science and Computation …, 2024
1 2024 
nicolas tabareauInriaE-mail confirmado em inria.fr