| 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 | 94 | 2019 |
| 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 | 89 | 2020 |
| 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 | 28 | 2021 |
| 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 | 28 | 2017 |
| 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 | 23 | 2021 |
| Eliminating reflection from type theory T Winterhalter, M Sozeau, N Tabareau Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 19 | 2019 |
| Formalisation and meta-theory of type theory T Winterhalter Nantes, 2020 | 9 | 2020 |
| Randomized mixed-radix scalar multiplication E Guerrini, L Imbert, T Winterhalter IEEE Transactions on Computers 67 (3), 418-431, 2017 | 7 | 2017 |
| The MetaCoq Project.(June 2019) M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ... | 6 | 2019 |
| Normalization by evaluation for sized dependent types. PACMPL 1, ICFP (2017), 33: 1–33: 30 A Abel, A Vezzosi, T Winterhalter | 6 | 2017 |
| 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 | 4 | 2023 |
| Randomizing scalar multiplication using exact covering systems of congruences E Guerrini, L Imbert, T Winterhalter | 4 | 2015 |
| How to tame your rewrite rules J Cockx, N Tabareau, T Winterhalter Types for Proofs and Programs, TYPES, 2019 | 3 | 2019 |
| Using reflection to eliminate reflection T Winterhalter, M Sozeau, N Tabareau TYPES 2018, 90, 2018 | 2 | 2018 |
| Composable partial functions in Coq, totally for free T Winterhalter 29th International Conference on Types for Proofs and Programs, 2023 | 1 | 2023 |
| The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography PG Haselwarter, BS Hvass, LL Hansen, T Winterhalter, C Hritcu, ... Cryptology ePrint Archive, 2023 | 1 | 2023 |
| Verifying non-terminating programs with IO in F CC Andrici, T Winterhalter, C Hritcu, E Rivas HOPE, 2022 | 1 | 2022 |
| Partial dijkstra monads for all T Winterhalter, CC Andrici, C Hritcu, K Maillard, G Martınez, E Rivas TYPES, 2022 | 1 | 2022 |
| Extensionality of Ghost Dependent Types for Free T Winterhalter | | 2023 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... | | 2023 |
nicolas tabareauInriaVerified email at inria.fr
