A compiled implementation of strong reduction. - Benjamin Grégoire; Xavier Leroy (ICFP, 2002)

A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. - Yves Bertot; Benjamin Grégoire; Xavier Leroy (TYPES, 2004)

On the Role of Type Decorations in the Calculus of Inductive Constructions. - Bruno Barras; Benjamin Grégoire (CSL, 2005)

Practical Inference for Type-Based Termination in a Polymorphic Setting. - Gilles Barthe; Benjamin Grégoire; Fernando Pastawski (TLCA, 2005)

Proving Equalities in a Commutative Ring Done Right in Coq. - Benjamin Grégoire; Assia Mahboubi (TPHOLs, 2005)

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. - Benjamin Grégoire; Laurent Théry (IJCAR, 2006)

A Computational Approach to Pocklington Certificates in Type Theory. - Benjamin Grégoire; Laurent Théry; Benjamin Werner (FLOPS, 2006)

JACK - A Tool for Validation of Security and Behaviour of Java Applications. - Gilles Barthe; Lilian Burdy; Julien Charles; Benjamin Grégoire; Marieke Huisman; Jean-Louis Lanet; Mariela Pavlova; Antoine Requet (FMCO, 2006)

CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. - Gilles Barthe; Benjamin Grégoire; Fernando Pastawski (LPAR, 2006)

MOBIUS: Mobility, Ubiquity, Security. - Gilles Barthe; Lennart Beringer; Pierre Crégut; Benjamin Grégoire; Martin Hofmann 001; Peter Müller 001; Erik Poll; Germán Puebla; Ian Stark; Eric Vétillard (TGC, 2006)

The MOBIUS Proof Carrying Code Infrastructure. - Gilles Barthe; Pierre Crégut; Benjamin Grégoire; Thomas P. Jensen; David Pichardie (FMCO, 2007)

Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. - Benjamin Grégoire; Jorge Luis Sacchini (TGC, 2007)

Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. - Benjamin Grégoire; Loïc Pottier; Laurent Théry (Automated Deduction in Geometry, 2008)

Preservation of Proof Obligations from Java to the Java Virtual Machine. - Gilles Barthe; Benjamin Grégoire; Mariela Pavlova (IJCAR, 2008)

Type-Based Termination with Sized Products. - Gilles Barthe; Benjamin Grégoire; Colin Riba (CSL, 2008)

Formal Certification of ElGamal Encryption. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Santiago Zanella-Béguelin (Formal Aspects in Security and Trust, 2008)

A Tutorial on Type-Based Termination. - Gilles Barthe; Benjamin Grégoire; Colin Riba (LerNet ALFA Summer School, 2008)

A New Elimination Rule for the Calculus of Inductive Constructions. - Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Luis Sacchini (TYPES, 2008)

Implementing a Direct Method for Certificate Translation. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; César Kunz; Anne Pacalet (ICFEM, 2009)

Formal certification of code-based cryptographic proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (POPL, 2009)

Formally Certifying the Security of Digital Signature Schemes. - Santiago Zanella-Béguelin; Gilles Barthe; Benjamin Grégoire; Federico Olmedo (SP, 2009)

Certificate translation for optimizing compilers. - Gilles Barthe; Benjamin Grégoire; César Kunz; Tamara Rezk (ACM Trans. Program. Lang. Syst., 2009)

A Machine-Checked Formalization of Sigma-Protocols. - Gilles Barthe; Daniel Hedin; Santiago Zanella-Béguelin; Benjamin Grégoire; Sylvain Heraud (CSF, 2010)

Extending Coq with Imperative Features and Its Application to SAT Verification. - Michaël Armand; Benjamin Grégoire; Arnaud Spiwack; Laurent Théry (ITP, 2010)

Programming Language Techniques for Cryptographic Proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (ITP, 2010)

On Strong Normalization of the Calculus of Constructions with Type-Based Termination. - Benjamin Grégoire; Jorge Luis Sacchini (LPAR (Yogyakarta), 2010)

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. - Michaël Armand; Germain Faure; Benjamin Grégoire; Chantal Keller; Laurent Théry; Benjamin Werner (CPP, 2011)

Full Reduction at Full Throttle. - Mathieu Boespflug; Maxime Dénès; Benjamin Grégoire (CPP, 2011)

Computer-Aided Security Proofs for the Working Cryptographer. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Santiago Zanella-Béguelin (CRYPTO, 2011)

Beyond Provable Security Verifiable IND-CCA Security of OAEP. - Gilles Barthe; Benjamin Grégoire; Yassine Lakhnech; Santiago Zanella-Béguelin (CT-RSA, 2011)

Certifying compilers using higher-order theorem provers as certificate checkers. - Jan Olaf Blech; Benjamin Grégoire (Formal Methods Syst. Des., 2011)

Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. - Gilles Barthe; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Santiago Zanella-Béguelin (CPP, 2012)

Verified Security of Merkle-Damgård. - Michael Backes 001; Gilles Barthe; Matthias Berg; Benjamin Grégoire; César Kunz; Malte Skoruppa; Santiago Zanella-Béguelin (CSF, 2012)

Computer-Aided Cryptographic Proofs. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Santiago Zanella-Béguelin (ITP, 2012)

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (MPC, 2012)

Computer-Aided Cryptographic Proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (SAS, 2012)

Recent Advances in the Formal Verification of Cryptographic Systems: Turing's Legacy - Benjamin Grégoire (ERCIM News, 2012)

Automated Analysis and Synthesis of Padding-Based Encryption Schemes. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2012)

Fully automated analysis of padding-based encryption in the computational model. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Benedikt Schmidt; Santiago Zanella-Béguelin (CCS, 2013)

Verified Computational Differential Privacy with Applications to Smart Metering. - Gilles Barthe; George Danezis; Benjamin Grégoire; César Kunz; Santiago Zanella-Béguelin (CSF, 2013)

EasyCrypt: A Tutorial. - Gilles Barthe; François Dupressoir; Benjamin Grégoire; César Kunz; Benedikt Schmidt; Pierre-Yves Strub (FOSAD, 2013)

Verified indifferentiable hashing into elliptic curves. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Federico Olmedo; Santiago Zanella-Béguelin (J. Comput. Secur., 2013)

Certified Synthesis of Efficient Batch Verifiers. - Joseph A. Akinyele; Gilles Barthe; Benjamin Grégoire; Benedikt Schmidt; Pierre-Yves Strub (CSF, 2014)

Probabilistic relational verification for cryptographic implementations. - Gilles Barthe; Cédric Fournet; Benjamin Grégoire; Pierre-Yves Strub; Nikhil Swamy; Santiago Zanella-Béguelin (POPL, 2014)

Verified Implementations for Secure and Verifiable Computation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Guillaume Davy; François Dupressoir; Benjamin Grégoire; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2014)

Making RSA-PSS Provably Secure Against Non-Random Faults. - Gilles Barthe; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; Mehdi Tibouchi; Jean-Christophe Zapalowicz (IACR Cryptol. ePrint Arch., 2014)

Synthesis of Fault Attacks on Cryptographic Implementations. - Gilles Barthe; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; Jean-Christophe Zapalowicz (IACR Cryptol. ePrint Arch., 2014)

Automated Proofs of Pairing-Based Cryptography. - Gilles Barthe; Benjamin Grégoire; Benedikt Schmidt (CCS, 2015)

Relational Reasoning via Probabilistic Coupling. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Léo Stefanesco; Pierre-Yves Strub (LPAR, 2015)

Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire (IACR Cryptol. ePrint Arch., 2015)

Verified Proofs of Higher-Order Masking. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2015)

Strong Non-Interference and Type-Directed Higher-Order Masking. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; Pierre-Yves Strub; Rébecca Zucchini (CCS, 2016)

Advanced Probabilistic Couplings for Differential Privacy. - Gilles Barthe; Noémie Fong; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (CCS, 2016)

A Program Logic for Union Bounds. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (ICALP, 2016)

Proving Differential Privacy via Probabilistic Couplings. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (LICS, 2016)

Advanced Probabilistic Couplings for Differential Privacy. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (CoRR, 2016)

Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. - Gilles Barthe; François Dupressoir; Sebastian Faust; Benjamin Grégoire; François-Xavier Standaert; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2016)

Jasmin: High-Assurance and High-Speed Cryptography. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Arthur Blot; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Hugo Pacheco 001; Benedikt Schmidt; Pierre-Yves Strub (CCS, 2017)

Proving uniformity and independence by self-composition and coupling. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (LPAR, 2017)

Coupling proofs are probabilistic product programs. - Gilles Barthe; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (POPL, 2017)

A Fast and Verified Software Stack for Secure Function Evaluation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2017)

A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'. - Gilles Barthe; François Dupressoir; Benjamin Grégoire (IACR Cryptol. ePrint Arch., 2017)

Provably secure compilation of side-channel countermeasures. - Gilles Barthe; Benjamin Grégoire; Vincent Laporte (IACR Cryptol. ePrint Arch., 2017)

Formal Security Proof of CMAC and Its Variants. - Cécile Baritel-Ruet; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire (CSF, 2018)

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". - Gilles Barthe; Benjamin Grégoire; Vincent Laporte (CSF, 2018)

An Assertion-Based Program Logic for Probabilistic Programs. - Gilles Barthe; Thomas Espitau; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (ESOP, 2018)

Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; François-Xavier Standaert; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2018)

maskVerif: a formal tool for analyzing software and hardware masked implementations. - Gilles Barthe; Sonia Belaïd; Pierre-Alain Fouque; Benjamin Grégoire (IACR Cryptol. ePrint Arch., 2018)

Symbolic Proofs for Lattice-Based Cryptography. - Gilles Barthe; Xiong Fan; Joshua Gancher; Benjamin Grégoire; Charlie Jacomme; Elaine Shi (IACR Cryptol. ePrint Arch., 2018)

Vectorizing Higher-Order Masking. - Benjamin Grégoire; Kostas Papagiannopoulos; Peter Schwabe; Ko Stoffelen (IACR Cryptol. ePrint Arch., 2018)

Proving expected sensitivity of probabilistic programs. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (Proc. ACM Program. Lang., 2018)

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. - José Bacelar Almeida; Cécile Baritel-Ruet; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Alley Stoughton; Pierre-Yves Strub (CCS, 2019)

Symbolic Methods in Computational Cryptography Proofs. - Gilles Barthe; Benjamin Grégoire; Charlie Jacomme; Steve Kremer; Pierre-Yves Strub (CSF, 2019)

maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. - Gilles Barthe; Sonia Belaïd; Gaëtan Cassiers; Pierre-Alain Fouque; Benjamin Grégoire; François-Xavier Standaert (ESORICS (1), 2019)

FaCT: a DSL for timing-sensitive computation. - Sunjay Cauligi; Gary Soeller; Brian Johannesmeyer; Fraser Brown; Riad S. Wahby; John Renner; Benjamin Grégoire; Gilles Barthe; Ranjit Jhala; Deian Stefan (PLDI, 2019)

Machine-Checked Proofs for Cryptographic Standards. - José Bacelar Almeida; Cécile Baritel-Ruet; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Alley Stoughton; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2019)

A Machine-Checked Proof of Security for AWS Key Management Service. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Matthew Campagna; Ernie Cohen; Benjamin Grégoire; Vitor Pereira 002; Bernardo Portela; Pierre-Yves Strub; Serdar Tasiran (IACR Cryptol. ePrint Arch., 2019)

Security Analysis of ElGamal Implementations. - Mohamad El Laz; Benjamin Grégoire; Tamara Rezk (ICETE (2), 2020)

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Adrien Koutsos; Vincent Laporte; Tiago Oliveira 004; Pierre-Yves Strub (SP, 2020)

High-Assurance Cryptography Software in the Spectre Era. - Gilles Barthe; Sunjay Cauligi; Benjamin Grégoire; Adrien Koutsos; Kevin Liao; Tiago Oliveira 004; Swarn Priya; Tamara Rezk; Peter Schwabe (IACR Cryptol. ePrint Arch., 2020)

Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; François-Xavier Standaert; Pierre-Yves Strub (J. Cryptogr. Eng., 2020)

Formal verification of a constant-time preserving C compiler. - Gilles Barthe; Sandrine Blazy; Benjamin Grégoire; Rémi Hutin; Vincent Laporte; David Pichardie; Alix Trieu (Proc. ACM Program. Lang., 2020)

High-Assurance Cryptography in the Spectre Era. - Gilles Barthe; Sunjay Cauligi; Benjamin Grégoire; Adrien Koutsos; Kevin Liao; Tiago Oliveira 004; Swarn Priya; Tamara Rezk; Peter Schwabe (SP, 2021)

EasyPQC: Verifying Post-Quantum Cryptography. - Manuel Barbosa; Gilles Barthe; Xiong Fan; Benjamin Grégoire; Shih-Han Hung; Jonathan Katz; Pierre-Yves Strub; Xiaodi Wu 001; Li Zhou 013 (IACR Cryptol. ePrint Arch., 2021)

Structured Leakage and Applications to Cryptographic Constant-Time and Cost. - Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Swarn Priya (IACR Cryptol. ePrint Arch., 2021)

Hardware Private Circuits: From Trivial Composition to Full Verification. - Gaëtan Cassiers; Benjamin Grégoire; Itamar Levi; François-Xavier Standaert (IEEE Trans. Computers, 2021)

Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. - Gilles Barthe; Marc Gourjon; Benjamin Grégoire; Maximilian Orlt; Clara Paglialonga; Lars Porth (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2021)

Typing High-Speed Cryptography against Spectre v1. - Basavesh Ammanaghatta Shivakumar; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Swarn Priya; Peter Schwabe; Lucas Tabary-Maujean (IACR Cryptol. ePrint Arch., 2022)

Enforcing fine-grained constant-time policies. - Basavesh Ammanaghatta Shivakumar; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Swarn Priya (IACR Cryptol. ePrint Arch., 2022)

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. - Benjamin Grégoire; Jean-Christophe Léchenet; Enrico Tassi (CPP, 2023)

Machine-Checked Security for rmXMSS as in RFC 8391 and $ mathrm {SPHINCS^{+}} $. - Manuel Barbosa; François Dupressoir; Benjamin Grégoire; Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (CRYPTO (5), 2023)

Formally verifying Kyber Part I: Implementation Correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2023)

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. - Manuel Barbosa; Gilles Barthe; Christian Doczkal; Jelle Don; Serge Fehr; Benjamin Grégoire; Yu-Hsuan Huang; Andreas Hülsing; Yi Lee; Xiaodi Wu 001 (IACR Cryptol. ePrint Arch., 2023)

Machine-Checked Security for $ mathrm{XMSS}$ as in RFC 8391 and $ mathrm{SPHINCS}^{+}$. - Manuel Barbosa; François Dupressoir; Benjamin Grégoire; Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2023)

Formally verifying Kyber Episode IV: Implementation correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. - Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Adrien Koutsos; Pierre-Yves Strub (ACM Trans. Priv. Secur., 2023)

Provable Security of Cryptographic Primitives: from Algorithms to Assembly. - Benjamin Grégoire (2024)

CV2EC: Getting the Best of Both Worlds. - Bruno Blanchet; Pierre Boutry; Christian Doczkal; Benjamin Grégoire; Pierre-Yves Strub (CSF, 2024)

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. - José Bacelar Almeida; Santiago Arranz-Olmos; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Cameron Low; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; et al. (IACR Cryptol. ePrint Arch., 2024)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (IACR Cryptol. ePrint Arch., 2024)

Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. - Martin Avanzini; Gilles Barthe; Benjamin Grégoire; Georg Moser; Gabriele Vanoni (Proc. ACM Program. Lang., 2024)

High-assurance zeroization. - Santiago Arranz-Olmos; Gilles Barthe; Ruben Gonzalez; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Peter Schwabe (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)

Masking the GLP Lattice-Based Signature Scheme at Any Order. - Gilles Barthe; Sonia Belaïd; Thomas Espitau; Pierre-Alain Fouque; Benjamin Grégoire; Mélissa Rossi; Mehdi Tibouchi (J. Cryptol., 2024)

Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (ASPLOS (2), 2025)

A Quantitative Probabilistic Relational Hoare Logic. - Martin Avanzini; Gilles Barthe; Davide Davoli 001; Benjamin Grégoire (Proc. ACM Program. Lang., 2025)

Preservation of Speculative Constant-Time by Compilation. - Santiago Arranz-Olmos; Gilles Barthe; Lionel Blatter; Benjamin Grégoire; Vincent Laporte (Proc. ACM Program. Lang., 2025)

Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code. - Santiago Arranz-Olmos; Gilles Barthe; Benjamin Grégoire; Jan Jancar; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (Zenodo, 2025)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (Zenodo, 2025)