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 | 111 | 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 | 100 | 2020 |
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 | 33 | 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 | 32 | 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 | 31 | 2021 |
Eliminating reflection from type theory T Winterhalter, M Sozeau, N Tabareau Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 24 | 2019 |
Formalisation and meta-theory of type theory T Winterhalter Nantes, 2020 | 13 | 2020 |
Randomized mixed-radix scalar multiplication E Guerrini, L Imbert, T Winterhalter IEEE Transactions on Computers 67 (3), 418-431, 2017 | 7 | 2017 |
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq M Sozeau, Y Forster, M Lennon-Bertrand, JB Nielsen, N Tabareau, ... | 6 | 2023 |
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 | 5 | 2023 |
Randomizing scalar multiplication using exact covering systems of congruences E Guerrini, L Imbert, T Winterhalter Cryptology ePrint Archive, 2015 | 4 | 2015 |
How to tame your rewrite rules J Cockx, N Tabareau, T Winterhalter Types for Proofs and Programs, TYPES, 2019 | 3 | 2019 |
Composable partial functions in Coq, totally for free T Winterhalter 29th International Conference on Types for Proofs and Programs, 2023 | 2 | 2023 |
Partial dijkstra monads for all T Winterhalter, CC Andrici, C Hriþcu, K Maillard, G Martínez, E Rivas TYPES, 2022 | 2 | 2022 |
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 Hriþcu, ... Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024 | 1 | 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 | 1 | 2024 |
Verifying non-terminating programs with IO in F CC Andrici, T Winterhalter, C Hriþcu, E Rivas HOPE, 2022 | 1 | 2022 |