Théo Winterhalter

28 papers A 1B 4Journal 21Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
Bounded Sort Polymorphism with Elimination Constraints.
Proc. ACM Program. Lang.
Johann Rosain, Tomás Díaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter
2026 J jnl
Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally.
Proc. ACM Program. Lang.
Yann Leray, Théo Winterhalter
2026 J jnl
Misquoted No More: Securely Extracting F* Programs with IO.
CoRR
Cezar-Constantin Andrici, Abigail Pribisova, Danel Ahman, Catalin Hritcu, Exequiel Rivas, Théo Winterhalter
2026 J jnl
The Rewster: Type Preserving Rewrite Rules for the Rocq Prover.
J. Autom. Reason.
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
2025 J jnl
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.
J. ACM
Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
2025 J jnl
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F.
CoRR
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
2025 J jnl
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F.
Proc. ACM Program. Lang.
Cezar-Constantin Andrici, Danel Ahman, Catalin Hritcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
2024 J jnl
Dependent Ghosts Have a Reflection for Free.
Proc. ACM Program. Lang.
Théo Winterhalter
2024 — conf
From Rewrite Rules to Axioms in the $\lambda \varPi $-Calculus Modulo Theory.
FoSSaCS (2)
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
2024 J jnl
From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory.
CoRR
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
2024 B conf
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti.
FSCD
Thiago Felicissimo, Théo Winterhalter
2024 J jnl
Securing Verified IO Programs Against Unverified Code in F.
Proc. ACM Program. Lang.
Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter
2024 B conf
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
CPP
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
2024 B conf
The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant.
ITP
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, Théo Winterhalter
2023 J jnl
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
ACM Trans. Program. Lang. Syst.
Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Carmine Abate, Nikolaj Sidorenco, Catalin Hritcu, Kenji Maillard, Bas Spitters
2023 J jnl
Securely Compiling Verified F* Programs With IO.
CoRR
Cezar-Constantin Andrici, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Théo Winterhalter
2023 J jnl
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography.
IACR Cryptol. ePrint Arch.
Philipp G. Haselwarter, Benjamin Salling Hvass, Lasse Letager Hansen, Théo Winterhalter, Catalin Hritcu, Bas Spitters
2021 A conf
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
CSF
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
2021 J jnl
SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq.
IACR Cryptol. ePrint Arch.
Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, Bas Spitters
2021 J jnl
The taming of the rew: a type theory with computational assumptions.
Proc. ACM Program. Lang.
Jesper Cockx, Nicolas Tabareau, Théo Winterhalter
2020 J jnl
Coq Coq correct! verification of type checking and erasure for Coq, in Coq.
Proc. ACM Program. Lang.
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
2020 — —
Formalisation and Meta-Theory of Type Theory. (Formalisation et Méta-Théorie de la Théorie des Types).
Théo Winterhalter
2020 J jnl
The MetaCoq Project.
J. Autom. Reason.
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
2019 B conf
Eliminating reflection from type theory.
CPP
Théo Winterhalter, Matthieu Sozeau, Nicolas Tabareau
2018 J jnl
Randomized Mixed-Radix Scalar Multiplication.
IEEE Trans. Computers
Eleonora Guerrini, Laurent Imbert, Théo Winterhalter
2017 J jnl
Normalization by evaluation for sized dependent types.
Proc. ACM Program. Lang.
Andreas Abel, Andrea Vezzosi, Théo Winterhalter
2016 J jnl
Randomized Mixed-Radix Scalar Multiplication.
IACR Cryptol. ePrint Arch.
Eleonora Guerrini, Laurent Imbert, Théo Winterhalter
2015 J jnl
Randomizing Scalar Multiplication Using Exact Covering Systems of Congruences.
IACR Cryptol. ePrint Arch.
Eleonora Guerrini, Laurent Imbert, Théo Winterhalter