| 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 | 134 | 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 | 125 | 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 | 42 | 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 | 40 | 2021 |
| Eliminating reflection from type theory T Winterhalter, M Sozeau, N Tabareau Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 40 | 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 | 38* | 2017 |
| Formalisation and meta-theory of type theory T Winterhalter Ph. D. thesis, Université de Nantes, 2020 | 19 | 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 | 14 | 2023 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... Journal of the ACM (JACM), 1-76, 2024 | 10 | 2024 |
| 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 | 5 | 2024 |
| 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 |
| 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 | 3 | 2024 |
| Partial dijkstra monads for all T Winterhalter, CC Andrici, C Hriţcu, K Maillard, G Martínez, E Rivas TYPES, 2022 | 3 | 2022 |
| Composable partial functions in Coq, totally for free T Winterhalter 29th International Conference on Types for Proofs and Programs, 2023 | 2 | 2023 |
| Using reflection to eliminate reflection T Winterhalter, M Sozeau, N Tabareau TYPES 2018, 90, 2018 | 2 | 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 -Calculus Modulo Theory V Blot, G Dowek, T Traversié, T Winterhalter International Conference on Foundations of Software Science and Computation …, 2024 | 1 | 2024 |
| 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, 2023 | 1 | 2023 |
nicolas tabareauInriaVerified email at inria.fr
