Théo Winterhalter

According to our database, Théo Winterhalter authored at least 24 papers between 2015 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2026

The Rewster: Type Preserving Rewrite Rules for the Rocq Prover.

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter

J. Autom. Reason., June, 2026

Misquoted No More: Securely Extracting F* Programs with IO.

Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter

CoRR, February, 2026

Bounded Sort Polymorphism with Elimination Constraints.

Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter

Proc. ACM Program. Lang., 2026

Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally.

Yann Leray, Théo Winterhalter

Proc. ACM Program. Lang., 2026

2025

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter

J. ACM, February, 2025

SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F.

Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter

Proc. ACM Program. Lang., 2025

2024

Securing Verified IO Programs Against Unverified Code in F.

Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter

Proc. ACM Program. Lang., January, 2024

Dependent Ghosts Have a Reflection for Free.

Théo Winterhalter

Proc. ACM Program. Lang., 2024

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory.

Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter

CoRR, 2024

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.

Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti.

Thiago Felicissimo, Théo Winterhalter

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory.

Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter

Proceedings of the Foundations of Software Science and Computation Structures, 2024

The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.

Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.

Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters

ACM Trans. Program. Lang. Syst., September, 2023

Securely Compiling Verified F* Programs With IO.

Cezar-Constantin Andrici, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Théo Winterhalter

CoRR, 2023

2021

The taming of the rew: a type theory with computational assumptions.

Jesper Cockx, Nicolas Tabareau, Théo Winterhalter

Proc. ACM Program. Lang., 2021

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

Formalisation and Meta-Theory of Type Theory. (Formalisation et Méta-Théorie de la Théorie des Types).

Théo Winterhalter

PhD thesis, 2020

Coq Coq correct! verification of type checking and erasure for Coq, in Coq.

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter

Proc. ACM Program. Lang., 2020

The MetaCoq Project.

Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter

J. Autom. Reason., 2020

2019

Eliminating reflection from type theory.

Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Randomized Mixed-Radix Scalar Multiplication.

Eleonora Guerrini, Laurent Imbert, Théo Winterhalter

IEEE Trans. Computers, 2018

2017

Normalization by evaluation for sized dependent types.

Andreas Abel, Andrea Vezzosi, Théo Winterhalter

Proc. ACM Program. Lang., 2017

2015

Randomizing Scalar Multiplication Using Exact Covering Systems of Congruences.

Eleonora Guerrini, Laurent Imbert, Théo Winterhalter

IACR Cryptol. ePrint Arch., 2015