| 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 | 85 | 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 | 80 | 2020 |
| 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 | 27 | 2017 |
| 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 | 23 | 2021 |
| 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 | 19 | 2021 |
| Eliminating reflection from type theory T Winterhalter, M Sozeau, N Tabareau Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 17 | 2019 |
| Formalisation and meta-theory of type theory T Winterhalter Nantes, 2020 | 8 | 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 |
| Randomizing scalar multiplication using exact covering systems of congruences E Guerrini, L Imbert, T Winterhalter | 4 | 2015 |
| 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, 2021 | 3 | 2021 |
| How to tame your rewrite rules J Cockx, N Tabareau, T Winterhalter Types for Proofs and Programs, TYPES, 2019 | 2 | 2019 |
| Using reflection to eliminate reflection T Winterhalter, M Sozeau, N Tabareau TYPES 2018, 90, 2018 | 2 | 2018 |
| 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 |
| Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... | | 2023 |
| Securely Compiling Verified F* Programs With IO CC Andrici, C Hritcu, G Martínez, E Rivas, T Winterhalter arXiv preprint arXiv:2303.01350, 2023 | | 2023 |
| Securely Compiling F★ Programs With IO and Then Linking Them Against Weakly-Typed Interfaces CC Andrici, C Hriþcu, T Winterhalter | | 2023 |
nicolas tabareauInriaVerified email at inria.fr
