Randomizing Scalar Multiplication Using Exact Covering Systems of Congruences. - Eleonora Guerrini; Laurent Imbert; Théo Winterhalter (IACR Cryptol. ePrint Arch., 2015)

Normalization by evaluation for sized dependent types. - Andreas Abel 001; Andrea Vezzosi; Théo Winterhalter (Proc. ACM Program. Lang., 2017)

Randomized Mixed-Radix Scalar Multiplication. - Eleonora Guerrini; Laurent Imbert; Théo Winterhalter (IEEE Trans. Computers, 2018)

Eliminating reflection from type theory. - Théo Winterhalter; Matthieu Sozeau; Nicolas Tabareau (CPP, 2019)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

Coq Coq correct! verification of type checking and erasure for Coq, in Coq. - Matthieu Sozeau; Simon Boulier; Yannick Forster 002; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2020)

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)

The taming of the rew: a type theory with computational assumptions. - Jesper Cockx; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2021)

Securely Compiling Verified F* Programs With IO. - Cezar-Constantin Andrici; Catalin Hritcu; Guido Martínez; Exequiel Rivas; Théo Winterhalter (CoRR, 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)

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., 2023)

From Rewrite Rules to Axioms in the $ lambda varPi $-Calculus Modulo Theory. - Valentin Blot; Gilles Dowek; Thomas Traversié; Théo Winterhalter (FoSSaCS (2), 2024)

Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. - Thiago Felicissimo; Théo Winterhalter (FSCD, 2024)

The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. - Yann Leray; Gaëtan Gilbert; Nicolas Tabareau; Théo Winterhalter (ITP, 2024)

From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory. - Valentin Blot; Gilles Dowek; Thomas Traversié; Théo Winterhalter (CoRR, 2024)

Dependent Ghosts Have a Reflection for Free. - Théo Winterhalter (Proc. ACM Program. Lang., 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., 2024)

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. - Matthieu Sozeau; Yannick Forster 002; Meven Lennon-Bertrand; Jakob Botsch Nielsen; Nicolas Tabareau; Théo Winterhalter (J. ACM, 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 (CoRR, 2025)