Congruence Types. - Gilles Barthe; Herman Geuvers (CSL, 1995)

A Simple Abstract Semantics for Equational Theories. - Gilles Barthe (FCT, 1995)

Modular Properties of Algebraic Type Systems. - Gilles Barthe; Herman Geuvers (HOA, 1995)

Extensions of Pure Type Systems. - Gilles Barthe (TLCA, 1995)

Implicit Coercions in Type Systems. - Gilles Barthe (TYPES, 1995)

A Two-Level Approach Towards Lean Proof-Checking. - Gilles Barthe; Mark Ruys; Henk Barendregt (TYPES, 1995)

On the Subject Reduction Property for Algebraic Type Systems. - Gilles Barthe; Paul-André Melliès (CSL, 1996)

Towards Lean Proof Checking. - Gilles Barthe; Hugo Elbers (DISCO, 1996)

Explicit Substitutions for the Lambda-Calculus. - Gilles Barthe; Fairouz Kamareddine; Alejandro Ríos 001 (ALP/HOA, 1997)

Termination of Algebraic Type Systems: The Syntactic Approach. - Gilles Barthe; Femke van Raamsdonk (ALP/HOA, 1997)

Reflections on Reflections. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (PLILP, 1997)

A notion of classical pure type system. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (MFPS, 1997)

Monadic Type Systems: Pure Type Systems for Impure Settings. - Gilles Barthe; John Hatcliff; Peter Thiemann 001 (HOOTS, 1997)

Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion. - Gilles Barthe (CSL, 1998)

The Relevance of Proof-Irrelevance. - Gilles Barthe (ICALP, 1998)

The Semi-Full Closure of Pure Type Systems. - Gilles Barthe (MFCS, 1998)

Constructor Subtyping. - Gilles Barthe; Maria João Frade (ESOP, 1999)

Partial Evaluation and Non-interference for Object Calculi. - Gilles Barthe; Bernard P. Serpette (Fuji International Symposium on Functional and Logic Programming, 1999)

Expanding the Cube. - Gilles Barthe (FoSSaCS, 1999)

Order-Sorted Inductive Types. - Gilles Barthe (Inf. Comput., 1999)

Type-checking injective pure type systems. - Gilles Barthe (J. Funct. Program., 1999)

CPS Translations and Applications: The Cube and Beyond. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (High. Order Symb. Comput., 1999)

An Introduction to Dependent Type Theory. - Gilles Barthe; Thierry Coquand (APPSEM, 2000)

Constructor Subtyping in the Calculus of Inductive Constructions. - Gilles Barthe; Femke van Raamsdonk (FoSSaCS, 2000)

Static Reduction Analysis for Imperative Object Oriented Languages. - Gilles Barthe; Bernard P. Serpette (LPAR, 2000)

Domain-free pure type systems. - Gilles Barthe; Morten Heine Sørensen (J. Funct. Program., 2000)

Tipos principales y cierre semi-completo para sistemas de tipos puros extendidos (trabajo en desarrollo). - Gilles Barthe; Blas C. Ruiz Jiménez (APPIA-GULP-PRODE, 2001)

Jakarta: A Toolset for Reasoning about JavaCard. - Gilles Barthe; Guillaume Dufay; Marieke Huisman; Simão Melo de Sousa (E-smart, 2001)

A Formal Executable Semantics of the JavaCard Platform. - Gilles Barthe; Guillaume Dufay; Line Jakubiec; Bernard P. Serpette; Simão Melo de Sousa (ESOP, 2001)

Type Isomorphisms and Proof Reuse in Dependent Type Theory. - Gilles Barthe; Olivier Pons (FoSSaCS, 2001)

An induction principle for pure type systems. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (Theor. Comput. Sci., 2001)

Weak normalization implies strong normalization in a class of non-dependent pure type systems. - Gilles Barthe; John Hatcliff; Morten Heine Sørensen (Theor. Comput. Sci., 2001)

Tool-Assisted Specification and Verification of the JavaCard Platform. - Gilles Barthe; Pierre Courtieu; Guillaume Dufay; Simão Melo de Sousa (AMAST, 2002)

Compositional Verification of Secure Applet Interactions. - Gilles Barthe; Dilian Gurov; Marieke Huisman (FASE, 2002)

CPS translating inductive and coinductive types. - Gilles Barthe; Tarmo Uustalu (PEPM, 2002)

Efficient Reasoning about Executable Specifications in Coq. - Gilles Barthe; Pierre Courtieu (TPHOLs, 2002)

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. - Gilles Barthe; Guillaume Dufay; Line Jakubiec; Simão Melo de Sousa (VMCAI, 2002)

Preface. - Gilles Barthe; Peter Thiemann 001 (TIP@MPC, 2002)

Pure patterns type systems. - Gilles Barthe; Horatiu Cirstea; Claude Kirchner; Luigi Liquori (POPL, 2003)

Validation of the JavaCard Platform with Implicit Induction Techniques. - Gilles Barthe; Sorin Stratulat (RTA, 2003)

Setoids in type theory. - Gilles Barthe; Venanzio Capretta; Olivier Pons (J. Funct. Program., 2003)

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. - Gilles Barthe; Jan Cederquist; Sabrina Tarento (IJCAR, 2004)

Enforcing High-Level Security Properties for Applets. - Mariela Pavlova; Gilles Barthe; Lilian Burdy; Marieke Huisman; Jean-Louis Lanet (CARDIS, 2004)

Formally verifying information flow type systems for concurrent and thread systems. - Gilles Barthe; Leonor Prensa Nieto (FMSE, 2004)

A Tool-Assisted Framework for Certified Bytecode Verification. - Gilles Barthe; Guillaume Dufay (FASE, 2004)

A Machine-Checked Formalization of the Random Oracle Model. - Gilles Barthe; Sabrina Tarento (TYPES, 2004)

Security Types Preserving Compilation: (Extended Abstract). - Gilles Barthe; Amitabh Basu; Tamara Rezk (VMCAI, 2004)

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. - Gilles Barthe; Peter Dybjer; Peter Thiemann 001 (J. Funct. Program., 2004)

Type-based termination of recursive definitions. - Gilles Barthe; Maria João Frade; Eduardo Giménez 001; Luís Pinto 001; Tarmo Uustalu (Math. Struct. Comput. Sci., 2004)

Formal Methods for Smartcard Security. - Gilles Barthe; Guillaume Dufay (FOSAD, 2005)

Proof Obligations Preserving Compilation. - Gilles Barthe; Tamara Rezk; Ando Saabas (Formal Aspects in Security and Trust, 2005)

Precise Analysis of Memory Consumption using Program Logics. - Gilles Barthe; Mariela Pavlova; Gerardo Schneider (SEFM, 2005)

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

Non-interference for a JVM-like language. - Gilles Barthe; Tamara Rezk (TLDI, 2005)

Preventing Timing Leaks Through Transactional Branching Instructions. - Gilles Barthe; Tamara Rezk; Martijn Warnier (QAPL, 2005)

Tool-Assisted Specification and Verification of Typed Low-Level Languages. - Gilles Barthe; Pierre Courtieu; Guillaume Dufay; Simão Melo de Sousa (J. Autom. Reason., 2005)

A computational view of implicit coercions in type theory. - Gilles Barthe (Math. Struct. Comput. Sci., 2005)

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. - Gilles Barthe; Julien Forest; David Pichardie; Vlad Rusu (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)

Deriving an Information Flow Checker and Certifying Compiler for Java. - Gilles Barthe; Tamara Rezk; David A. Naumann (S&P, 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)

Remarks on the equational theory of non-normalizing pure type systems. - Gilles Barthe; Thierry Coquand (J. Funct. Program., 2006)

07091 Executive Summary - Mobility, Ubiquity and Security. - Gilles Barthe; Heiko Mantel; Peter Müller 001; Andrew C. Myers; Andrei Sabelfeld (Mobility, Ubiquity and Security, 2007)

07091 Abstracts Collection - Mobility, Ubiquity and Security. - Gilles Barthe; Heiko Mantel; Peter Müller 001; Andrew C. Myers; Andrei Sabelfeld (Mobility, Ubiquity and Security, 2007)

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

Security types preserving compilation. - Gilles Barthe; Tamara Rezk; Amitabh Basu (Comput. Lang. Syst. Struct., 2007)

Secure information flow for a concurrent language with scheduling. - Gilles Barthe; Leonor Prensa Nieto (J. Comput. Secur., 2007)

Certified Reasoning in Memory Hierarchies. - Gilles Barthe; César Kunz; Jorge Luis Sacchini (APLAS, 2008)

Certificate Translation. - Gilles Barthe (VERIFY, 2008)

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

Tractable Enforcement of Declassification Policies. - Gilles Barthe; Salvador Cavadini; Tamara Rezk (CSF, 2008)

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

Certificate Translation in Abstract Interpretation. - Gilles Barthe; César Kunz (ESOP, 2008)

Certificate translation for specification-preserving advices. - Gilles Barthe; César Kunz (FOAL, 2008)

An Introduction to Certificate Translation. - Gilles Barthe; César Kunz (FOSAD, 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)

Preservation of Proof Pbligations for Hybrid Verification Methods. - Gilles Barthe; César Kunz; David Pichardie; Julián Samborski-Forlese (SEFM, 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)

Computational indistinguishability logic. - Gilles Barthe; Marion Daubignard; Bruce M. Kapron; Yassine Lakhnech (CCS, 2010)

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

Robustness Guarantees for Anonymity. - Gilles Barthe; Alejandro Hevia; Zhengqin Luo; Tamara Rezk; Bogdan Warinschi (CSF, 2010)

A Functional Framework for Result Checking. - Gilles Barthe; Pablo Buiras; César Kunz (FLOPS, 2010)

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

On the Equality of Probabilistic Terms. - Gilles Barthe; Marion Daubignard; Bruce M. Kapron; Yassine Lakhnech; Vincent Laporte (LPAR (Dakar), 2010)

Perspectives in Certificate Translation. - Gilles Barthe; César Kunz (TGC, 2010)

Security of multithreaded programs by compilation. - Gilles Barthe; Tamara Rezk; Alejandro Russo; Andrei Sabelfeld (ACM Trans. Inf. Syst. Secur., 2010)

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)

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001 (FM, 2011)

Relational Verification Using Product Programs. - Gilles Barthe; Juan Manuel Crespo; César Kunz (FM, 2011)

A Computational Indistinguishability Logic for the Bounded Storage Model. - Gilles Barthe; Mathilde Duclos; Yassine Lakhnech (FPS, 2011)

Verifiable Security of Boneh-Franklin Identity-Based Encryption. - Gilles Barthe; Federico Olmedo; Santiago Zanella-Béguelin (ProvSec, 2011)

Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language. - Gilles Barthe; Exequiel Rivas (TGC, 2011)

Information-theoretic Bounds for Differentially Private Mechanisms. - Gilles Barthe; Boris Köpf (IACR Cryptol. ePrint Arch., 2011)

Secure information flow by self-composition. - Gilles Barthe; Pedro R. D'Argenio; Tamara Rezk (Math. Struct. Comput. Sci., 2011)

An Abstract Model of Certificate Translation. - Gilles Barthe; César Kunz (ACM Trans. Program. Lang. Syst., 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)

Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001 (CSF, 2012)

A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. - Gilles Barthe; Delphine Demange; David Pichardie (ESOP, 2012)

Secure Multi-Execution through Static Program Transformation. - Gilles Barthe; Juan Manuel Crespo; Dominique Devriese; Frank Piessens; Exequiel Rivas (FMOODS/FORTE, 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)

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. - José Bacelar Almeida; Manuel Barbosa; Endre Bangerter; Gilles Barthe; Stephan Krenn; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 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)

Verified Security of Redundancy-Free Encryption from Rabin and RSA. - Gilles Barthe; David Pointcheval; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2012)

Preface. - Gilles Barthe; Jorge Cuéllar; Javier López 001; Alexander Pretschner (J. Comput. Secur., 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)

Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. - Gilles Barthe; Federico Olmedo (ICALP (2), 2013)

Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. - Gilles Barthe; Juan Manuel Crespo; César Kunz (LFCS, 2013)

From relational verification to SIMD loop synthesis. - Gilles Barthe; Juan Manuel Crespo; Sumit Gulwani; César Kunz; Mark Marron (PPoPP, 2013)

Computer-Aided Security Proofs. - Gilles Barthe (QEST, 2013)

Formally Verified Implementation of an Idealized Model of Virtualization. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Jesús Mauricio Chimento; Carlos Luna 001 (TYPES, 2013)

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir (IACR Cryptol. ePrint Arch., 2013)

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

A certified lightweight non-interference Java bytecode verifier. - Gilles Barthe; David Pichardie; Tamara Rezk (Math. Struct. Comput. Sci., 2013)

Probabilistic Relational Reasoning for Differential Privacy. - Gilles Barthe; Boris Köpf; Federico Olmedo; Santiago Zanella-Béguelin (ACM Trans. Program. Lang. Syst., 2013)

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

Proving Differential Privacy in Hoare Logic. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; César Kunz; 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)

Leakage Resilience against Concurrent Cache Attacks. - Gilles Barthe; Boris Köpf; Laurent Mauborgne; Martín Ochoa (POST, 2014)

The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492). - Gilles Barthe; Michael Hicks 001; Florian Kerschbaum; Dominique Unruh (Dagstuhl Reports, 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)

System-level non-interference for constant-time cryptography. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; David Pichardie (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)

Formal Verification of an SSA-Based Middle-End for CompCert. - Gilles Barthe; Delphine Demange; David Pichardie (ACM Trans. Program. Lang. Syst., 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)

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (POPL, 2015)

Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181). - Gilles Barthe; Andrew D. Gordon 001; Joost-Pieter Katoen; Annabelle McIver (Dagstuhl Reports, 2015)

Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir (IACR Cryptol. ePrint Arch., 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)

Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. - Gilles Barthe; Juan Manuel Crespo; Yassine Lakhnech; Benedikt Schmidt (IACR Cryptol. ePrint Arch., 2015)

High-Assurance Cryptography: Cryptographic Software We Can Trust. - Gilles Barthe (IEEE Secur. Priv., 2015)

SEFM: software engineering and formal methods. - Gilles Barthe; Alberto Pardo; Gerardo Schneider (Softw. Syst. Model., 2015)

Synthesizing Probabilistic Invariants via Doob's Decomposition. - Gilles Barthe; Thomas Espitau; Luis María Ferrer Fioriti; Justin Hsu (CAV (1), 2016)

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)

Differentially Private Bayesian Programming. - Gilles Barthe; Gian Pietro Farina; Marco Gaboardi; Emilio Jesús Gallego Arias; Andy Gordon 001; Justin Hsu; Pierre-Yves Strub (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)

Facets of Software Doping. - Gilles Barthe; Pedro R. D'Argenio; Bernd Finkbeiner; Holger Hermanns (ISoLA (2), 2016)

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

Verifying Constant-Time Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Michael Emmi (USENIX Security Symposium, 2016)

Computer-Aided Verification for Mechanism Design. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (WINE, 2016)

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

Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. - Miguel Ambrona; Gilles Barthe; Benedikt Schmidt (IACR Cryptol. ePrint Arch., 2016)

Generic Transformations of Predicate Encodings: Constructions and Applications. - Miguel Ambrona; Gilles Barthe; Benedikt Schmidt (IACR Cryptol. ePrint Arch., 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)

Strongly-optimal structure preserving signatures from Type II pairings: synthesis and lower bounds. - Gilles Barthe; Edvard Fagerholm; Dario Fiore 001; Andre Scedrov; Benedikt Schmidt; Mehdi Tibouchi (IET Inf. Secur., 2016)

Product programs and relational program logics. - Gilles Barthe; Juan Manuel Crespo; César Kunz (J. Log. Algebraic Methods Program., 2016)

Programming language techniques for differential privacy. - Gilles Barthe; Marco Gaboardi; Justin Hsu; Benjamin C. Pierce (ACM SIGLOG News, 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)

Verified Translation Validation of Static Analyses. - Gilles Barthe; Sandrine Blazy; Vincent Laporte; David Pichardie; Alix Trieu (CSF, 2017)

Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs. - Pedro R. D'Argenio; Gilles Barthe; Sebastian Biewer; Bernd Finkbeiner; Holger Hermanns (ESOP, 2017)

Reasoning about Probabilistic Defense Mechanisms against Remote Attacks. - Martín Ochoa; Sebastian Banescu; Cynthia Disenfeld; Gilles Barthe; Vijay Ganesh 001 (EuroS&P, 2017)

*-Liftings for Differential Privacy. - Gilles Barthe; Thomas Espitau; Justin Hsu; Tetsuya Sato 001; Pierre-Yves Strub (ICALP, 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)

Relational cost analysis. - Ezgi Çiçek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Jan Hoffmann 002 (POPL, 2017)

Reasoning about Divergences for Relaxations of Differential Privacy. - Tetsuya Sato 001; Gilles Barthe; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (CoRR, 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)

Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions. - Miguel Ambrona; Gilles Barthe; Romain Gay; Hoeteck Wee (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)

A relational logic for higher-order programs. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Pierre-Yves Strub (Proc. ACM Program. Lang., 2017)

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

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. - Alejandro Aguirre 001; Gilles Barthe; Lars Birkedal; Ales Bizjak; Marco Gaboardi; Deepak Garg 001 (ESOP, 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)

Almost Sure Productivity. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Alexandra Silva 001 (ICALP, 2018)

Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences. - Borja Balle; Gilles Barthe; Marco Gaboardi (NeurIPS, 2018)

Formal verification of higher-order probabilistic programs. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (CoRR, 2018)

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (IACR Cryptol. ePrint Arch., 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)

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

Monadic refinements for relational cost analysis. - Ivan Radicek; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Florian Zuleger (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)

Verifying Relational Properties using Trace Logic. - Gilles Barthe; Renate Eilers; Pamina Georgiou; Bernhard Gleiss; Laura Kovács; Matteo Maffei (FMCAD, 2019)

Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. - Tetsuya Sato 001; Gilles Barthe; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (LICS, 2019)

Privacy Amplification by Mixing and Diffusion Mechanisms. - Borja Balle; Gilles Barthe; Marco Gaboardi; Joseph Geumlek (NeurIPS, 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)

Bidirectional type checking for relational properties. - Ezgi Çiçek; Weihao Qu; Gilles Barthe; Marco Gaboardi; Deepak Garg 001 (PLDI, 2019)

Coupling Techniques for Reasoning about Quantum Programs. - Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu; Li Zhou 013 (CoRR, 2019)

Kantorovich Continuity of Probabilistic Programs. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (CoRR, 2019)

Towards Constant-Time Foundations for the New Spectre Era. - Sunjay Cauligi; Craig Disselkoen; Klaus von Gleissenthall; Deian Stefan; Tamara Rezk; Gilles Barthe (CoRR, 2019)

Automated Methods for Checking Differential Privacy. - Gilles Barthe; Rohit Chadha; Vishal Jagannath; A. Prasad Sistla; Mahesh Viswanathan 001 (CoRR, 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)

SoK: Computer-Aided Cryptography. - Manuel Barbosa; Gilles Barthe; Karthikeyan Bhargavan; Bruno Blanchet; Cas Cremers; Kevin Liao; Bryan Parno (IACR Cryptol. ePrint Arch., 2019)

GALACTICS: Gaussian Sampling for Lattice-Based Constant-Time Implementation of Cryptographic Signatures, Revisited. - Gilles Barthe; Sonia Belaïd; Thomas Espitau; Pierre-Alain Fouque; Mélissa Rossi; Mehdi Tibouchi (IACR Cryptol. ePrint Arch., 2019)

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. - Patrick Baillot; Gilles Barthe; Ugo Dal Lago (J. Autom. Reason., 2019)

System-Level Non-interference of Constant-Time Cryptography. Part I: Model. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001 (J. Autom. Reason., 2019)

Automated Analysis of Cryptographic Assumptions in Generic Group Models. - Gilles Barthe; Edvard Fagerholm; Dario Fiore 001; John C. Mitchell; Andre Scedrov; Benedikt Schmidt (J. Cryptol., 2019)

Program for TPDP 2016. - Gilles Barthe; Christos Dimitrakakis; Marco Gaboardi; Andreas Haeberlen; Aaron Roth 001; Aleksandra B. Slavkovic (J. Priv. Confidentiality, 2019)

Relational ⋆⋆ star-Liftings for Differential Privacy. - Gilles Barthe; Thomas Espitau; Justin Hsu; Tetsuya Sato 001; Pierre-Yves Strub (Log. Methods Comput. Sci., 2019)

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (Proc. ACM Program. Lang., 2019)

Probabilistic Couplings from Program Logics. - Gilles Barthe; Justin Hsu (Foundations of Probabilistic Programming, 2020)

Hypothesis Testing Interpretations and Renyi Differential Privacy. - Borja Balle; Gilles Barthe; Marco Gaboardi; Justin Hsu; Tetsuya Sato 001 (AISTATS, 2020)

Model-Agnostic Counterfactual Explanations for Consequential Decisions. - Amir-Hossein Karimi; Gilles Barthe; Borja Balle; Isabel Valera (AISTATS, 2020)

On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. - Gilles Barthe; Raphaëlle Crubillé; Ugo Dal Lago; Francesco Gavazzo (ESOP, 2020)

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Vincent Laporte; Tiago Oliveira 004 (INDOCRYPT, 2020)

Deciding Differential Privacy for Programs with Finite Inputs and Outputs. - Gilles Barthe; Rohit Chadha; Vishal Jagannath; A. Prasad Sistla; Mahesh Viswanathan 001 (LICS, 2020)

Constant-time foundations for the new spectre era. - Sunjay Cauligi; Craig Disselkoen; Klaus von Gleissenthall; Dean M. Tullsen; Deian Stefan; Tamara Rezk; Gilles Barthe (PLDI, 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)

A survey of algorithmic recourse: definitions, formulations, solutions, and prospects. - Amir-Hossein Karimi; Gilles Barthe; Bernhard Schölkopf; Isabel Valera (CoRR, 2020)

PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation. - Gilles Barthe; Roberta De Viti; Peter Druschel; Deepak Garg 001; Manuel Gomez-Rodriguez; Pierfrancesco Ingo; Matthew Lentz; Aastha Mehta; Bernhard Schölkopf (CoRR, 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)

System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. - Gilles Barthe; Gustavo Betarte; Juan Diego Campo; Carlos Luna 001; David Pichardie (J. Autom. Reason., 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)

Privacy Profiles and Amplification by Subsampling. - Borja Balle; Gilles Barthe; Marco Gaboardi (J. Priv. Confidentiality, 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)

A probabilistic separation logic. - Gilles Barthe; Justin Hsu; Kevin Liao (Proc. ACM Program. Lang., 2020)

Relational proofs for quantum programs. - Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu; Li Zhou 013 (Proc. ACM Program. Lang., 2020)

Scaling Guarantees for Nearest Counterfactual Explanations. - Kiarash Mohammadi; Amir-Hossein Karimi; Gilles Barthe; Isabel Valera (AIES, 2021)

Secure Compilation of Constant-Resource Programs. - Gilles Barthe; Sandrine Blazy; Rémi Hutin; David Pichardie (CSF, 2021)

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. - Li Zhou 013; Gilles Barthe; Justin Hsu; Mingsheng Ying; Nengkun Yu (LICS, 2021)

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)

SoK: Practical Foundations for Spectre Defenses. - Sunjay Cauligi; Craig Disselkoen; Daniel Moghimi; Gilles Barthe; Deian Stefan (CoRR, 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)

âTheyâre not that hard to mitigateâ: What Cryptographic Library Developers Think About Timing Attacks. - Jan Jancar; Marcel Fourné; Daniel De Almeida Braga; Mohamed Sabt; Peter Schwabe; Gilles Barthe; Pierre-Alain Fouque; Yasemin Acar (IACR Cryptol. ePrint Arch., 2021)

A pre-expectation calculus for probabilistic sensitivity. - Alejandro Aguirre 001; Gilles Barthe; Justin Hsu; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Christoph Matheja (Proc. ACM Program. Lang., 2021)

Higher-order probabilistic adversarial computations: categorical semantics and program logics. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Shin-ya Katsumata; Tetsuya Sato 001 (Proc. ACM Program. Lang., 2021)

On continuation-passing transformations and expected cost analysis. - Martin Avanzini; Gilles Barthe; Ugo Dal Lago (Proc. ACM Program. Lang., 2021)

Deciding accuracy of differential privacy schemes. - Gilles Barthe; Rohit Chadha; Paul Krogmeier; A. Prasad Sistla; Mahesh Viswanathan 001 (Proc. ACM Program. Lang., 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)

Symbolic Synthesis of Indifferentiability Attacks. - Itsaka Rakotonirina; Miguel Ambrona; Alejandro Aguirre 001; Gilles Barthe (AsiaCCS, 2022)

Tidy: Symbolic Verification of Timed Cryptographic Protocols. - Gilles Barthe; Ugo Dal Lago; Giulio Malavolta; Itsaka Rakotonirina (CCS, 2022)

Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. - Gilles Barthe; Adrien Koutsos; Solène Mirliaz; David Pichardie; Peter Schwabe (SAS, 2022)

SoK: Practical Foundations for Software Spectre Defenses. - Sunjay Cauligi; Craig Disselkoen; Daniel Moghimi; Gilles Barthe; Deian Stefan (SP, 2022)

Flux: Liquid Types for Rust. - Nico Lehmann; Adam T. Geller; Gilles Barthe; Niki Vazou; Ranjit Jhala (CoRR, 2022)

On Feller Continuity and Full Abstraction (Long Version). - Gilles Barthe; Raphaëlle Crubillé; Ugo Dal Lago; Francesco Gavazzo (CoRR, 2022)

Spectre Declassified: Reading from the Right Place at the Wrong Time. - Basavesh Ammanaghatta Shivakumar; Jack Barnes; Gilles Barthe; Sunjay Cauligi; Chitchanok Chuengsatiansup; Daniel Genkin; Sioli O'Connell; Peter Schwabe; Rui Qi Sim; Yuval Yarom (IACR Cryptol. ePrint Arch., 2022)

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)

Breaking and Fixing Speculative Load Hardening. - Zhiyuan Zhang 005; Gilles Barthe; Chitchanok Chuengsatiansup; Peter Schwabe; Yuval Yarom (IACR Cryptol. ePrint Arch., 2022)

A formal treatment of the role of verified compilers in secure computation. - José Carlos Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (J. Log. Algebraic Methods Program., 2022)

On Feller continuity and full abstraction. - Gilles Barthe; Raphaëlle Crubillé; Ugo Dal Lago; Francesco Gavazzo (Proc. ACM Program. Lang., 2022)

Safe couplings: coupled refinement types. - Elizaveta Vasilenko; Niki Vazou; Gilles Barthe (Proc. ACM Program. Lang., 2022)

Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. - Gilles Barthe; Charlie Jacomme; Steve Kremer (ACM Trans. Comput. Log., 2022)

Ultimate SLH: Taking Speculative Load Hardening to the Next Level. - Zhiyuan Zhang 005; Gilles Barthe; Chitchanok Chuengsatiansup; Peter Schwabe; Yuval Yarom (USENIX Security Symposium, 2023)

A Survey of Algorithmic Recourse: Contrastive Explanations and Consequential Recommendations. - Amir-Hossein Karimi; Gilles Barthe; Bernhard Schölkopf; Isabel Valera (ACM Comput. Surv., 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)

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)

CoqQ: Foundational Verification of Quantum Programs. - Li Zhou 013; Gilles Barthe; Pierre-Yves Strub; Junyi Liu 002; Mingsheng Ying (Proc. ACM Program. Lang., 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)

OBRA: Oracle-Based, Relational, Algorithmic Type Verification. - Elizaveta Vasilenko; Niki Vazou; Gilles Barthe (APLAS, 2024)

Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures. - Gilles Barthe; Marcel Böhme; Sunjay Cauligi; Chitchanok Chuengsatiansup; Daniel Genkin; Marco Guarnieri; David Mateos Romero; Peter Schwabe; David Wu; Yuval Yarom (CCS, 2024)

They're not that hard to mitigate: What Cryptographic Library Developers Think About Timing Attacks. - Jan Jancar; Marcel Fourné; Daniel De Almeida Braga; Mohamed Sabt; Peter Schwabe; Gilles Barthe; Pierre-Alain Fouque; Yasemin Acar (Software Engineering, 2024)

Laws of Quantum Programming. - Mingsheng Ying; Li Zhou 013; Gilles Barthe (CoRR, 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)

"These results must be false": A usability evaluation of constant-time analysis tools. - Marcel Fourné; Daniel De Almeida Braga; Jan Jancar; Mohamed Sabt; Peter Schwabe; Gilles Barthe; Pierre-Alain Fouque; Yasemin Acar (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)

A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. - Vineet Rajani; Gilles Barthe; Deepak Garg 001 (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)

Decision and Complexity of Dolev-Yao Hyperproperties. - Itsaka Rakotonirina; Gilles Barthe; Clara Schneidewind (Proc. ACM Program. Lang., 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)

D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation. - Yingte Xu; Li Zhou 013; Gilles Barthe (CAV (4), 2025)

Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt. - José Bacelar Almeida; Gustavo Xavier Delerue Marinho Alves; Manuel Barbosa; Gilles Barthe; Luís Esquível; Vincent Hwang; Tiago Oliveira 004; Hugo Pacheco 001; Peter Schwabe; Pierre-Yves Strub (SP, 2025)

CT-LLVM: Automatic Large-Scale Constant-Time Analysis. - Zhiyuan Zhang; Gilles Barthe (IACR Cryptol. ePrint Arch., 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)

Automating Equational Proofs in Dirac Notation. - Yingte Xu; Gilles Barthe; Li Zhou 013 (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)

Transparent Decompilation for Timing Side-Channel Analyses. - Santiago Arranz-Olmos; Gilles Barthe; Lionel Blatter; Sören van der Wall; Zhiyuan Zhang 005 (CoRR, 2025)

Complete Quantum Relational Hoare Logics from Optimal Transport Duality. - Gilles Barthe; Minbo Gao; Theo Wang; Li Zhou 013 (CoRR, 2025)

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. - Junyi Liu 002; Li Zhou 013; Gilles Barthe; Mingsheng Ying (J. ACM, 2025)