Théo Winterhalter

Publication Activity (10 Years)

Years Active: 2015-2024
Publications (10 Years): 18

Top Topics

Scalar Multiplication

Top Venues

Proc. ACM Program. Lang.

IACR Cryptol. ePrint Arch.

Publications

Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. CPP (2024)
Thiago Felicissimo, Théo Winterhalter
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. FSCD (2024)
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter
Securing Verified IO Programs Against Unverified Code in F. Proc. ACM Program. Lang. 8 (POPL) (2024)
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. CoRR (2024)
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory. FoSSaCS (2) (2024)
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. ACM Trans. Program. Lang. Syst. 45 (3) (2023)
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. IACR Cryptol. ePrint Arch. 2023 (2023)
Cezar-Constantin Andrici, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
Securely Compiling Verified F* Programs With IO. CoRR (2023)
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. IACR Cryptol. ePrint Arch. 2021 (2021)
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. CSF (2021)
Jesper Cockx, Nicolas Tabareau, Théo Winterhalter
The taming of the rew: a type theory with computational assumptions. Proc. ACM Program. Lang. 5 (POPL) (2021)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
Eliminating reflection from type theory. CPP (2019)
Eleonora Guerrini, Laurent Imbert, Théo Winterhalter
Randomized Mixed-Radix Scalar Multiplication. IEEE Trans. Computers 67 (3) (2018)
Andreas Abel, Andrea Vezzosi, Théo Winterhalter
Normalization by evaluation for sized dependent types. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Eleonora Guerrini, Laurent Imbert, Théo Winterhalter
Randomized Mixed-Radix Scalar Multiplication. IACR Cryptol. ePrint Arch. 2016 (2016)
Eleonora Guerrini, Laurent Imbert, Théo Winterhalter
Randomizing Scalar Multiplication Using Exact Covering Systems of Congruences. IACR Cryptol. ePrint Arch. 2015 (2015)