Théo Winterhalter

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

Collaborative distances:

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

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

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

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

IACR Cryptol. ePrint Arch., 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

IACR Cryptol. ePrint Arch., 2021

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