Follow
Théo Winterhalter
Théo Winterhalter
Inria Saclay
Verified email at inria.fr - Homepage
Title
Cited by
Cited by
Year
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
1272020
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
1202019
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
402021
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
382021
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
Eliminating reflection from type theory
T Winterhalter, M Sozeau, N Tabareau
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
342019
Formalisation and meta-theory of type theory
T Winterhalter
Ph. D. thesis, Université de Nantes, 2020
182020
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
122023
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, 2023
102023
Randomized mixed-radix scalar multiplication
E Guerrini, L Imbert, T Winterhalter
IEEE Transactions on Computers 67 (3), 418-431, 2017
82017
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
42024
How to tame your rewrite rules
J Cockx, N Tabareau, T Winterhalter
Types for Proofs and Programs, TYPES, 2019
42019
Randomizing scalar multiplication using exact covering systems of congruences
E Guerrini, L Imbert, T Winterhalter
Cryptology ePrint Archive, 2015
42015
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
32024
Partial dijkstra monads for all
T Winterhalter, CC Andrici, C Hriţcu, K Maillard, G Martínez, E Rivas
TYPES, 2022
32022
Composable partial functions in Coq, totally for free
T Winterhalter
29th International Conference on Types for Proofs and Programs, 2023
22023
Using reflection to eliminate reflection
T Winterhalter, M Sozeau, N Tabareau
TYPES 2018, 90, 2018
22018
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
12024
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
12024
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
12023
The system can't perform the operation now. Try again later.
Articles 1–20