Gilles Barthe
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
139
Venues
44
Active years
1995–2026
Best venue rank
A*
Where they publish
- A*CCS26 papers
- A*SP10 papers
- AESOP9 papers
- A*LICS8 papers
- A*POPL7 papers
- BLPAR6 papers
- A*CRYPTO5 papers
- A*EuroCrypt5 papers
- A*ICALP5 papers
- BCSL4 papers
- BSAS3 papers
- A*PLDI3 papers
- NationalFLOPS3 papers
- ACADE3 papers
- BFOSSACS3 papers
- A*CAV2 papers
- BAPLAS2 papers
- AAISTATS2 papers
- AESORICS2 papers
- NationalLFCS2 papers
- BITP2 papers
- BFM2 papers
- BSEFM2 papers
- BFASE2 papers
- BVMCAI2 papers
- A*ASPLOS1 paper
- AAsiaCCS1 paper
- CAIES1 paper
- NationalINDOCRYPT1 paper
- BFMCAD1 paper
- A*FSE1 paper
- CISoLA1 paper
- BPKC1 paper
- ACHES1 paper
- BPPoPP1 paper
- BCPP1 paper
- CFORTE1 paper
- BMPC1 paper
- CProvSec1 paper
- CICFEM1 paper
- CCARDIS1 paper
- CPEPM1 paper
- BMFCS1 paper
- BFCT1 paper
Papers
139 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | LICS | Complete Relational Logic for Infinite-Dimensional Quantum Programs with Unbounded Assertions. | Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Tianshi Yu, Li Zhou |
| 2025 | ASPLOS | Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). | Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang |
| 2025 | CAV | D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation. | Yingte Xu, Li Zhou, Gilles Barthe |
| 2025 | CCS | Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, Joo Diogo Duarte, Benjamin Grgoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2025 | LICS | Complete Quantum Relational Hoare Logics from Optimal Transport Duality. | Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou |
| 2025 | SP | 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, Lus Esquvel, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub |
| 2024 | APLAS | OBRA: Oracle-Based, Relational, Algorithmic Type Verification. | Elizaveta Vasilenko, Niki Vazou, Gilles Barthe |
| 2024 | CCS | Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures. | Gilles Barthe, Marcel Bhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom |
| 2024 | CRYPTO | 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, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Jean-Christophe Lchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub |
| 2023 | CRYPTO | Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. | Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grgoire, Yu-Hsuan Huang, Andreas Hlsing, Yi Lee, Xiaodi Wu |
| 2023 | SP | 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 |
| 2023 | SP | Typing High-Speed Cryptography against Spectre v1. | Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean |
| 2022 | AsiaCCS | Symbolic Synthesis of Indifferentiability Attacks. | Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe |
| 2022 | CCS | Tidy: Symbolic Verification of Timed Cryptographic Protocols. | Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina |
| 2022 | CCS | Enforcing Fine-grained Constant-time Policies. | Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grgoire, Vincent Laporte, Swarn Priya |
| 2022 | LICS | Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. | Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying |
| 2022 | SP | SoK: Practical Foundations for Software Spectre Defenses. | Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan |
| 2022 | SP | "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 |
| 2022 | SAS | Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. | Gilles Barthe, Adrien Koutsos, Solne Mirliaz, David Pichardie, Peter Schwabe |
| 2021 | AIES | Scaling Guarantees for Nearest Counterfactual Explanations. | Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera |
| 2021 | CCS | EasyPQC: Verifying Post-Quantum Cryptography. | Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grgoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou |
| 2021 | CCS | Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. | Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Pierre-Yves Strub |
| 2021 | CCS | Structured Leakage and Applications to Cryptographic Constant-Time and Cost. | Gilles Barthe, Benjamin Grgoire, Vincent Laporte, Swarn Priya |
| 2021 | LICS | A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. | Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu |
| 2021 | SP | SoK: Computer-Aided Cryptography. | Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno |
| 2021 | SP | High-Assurance Cryptography in the Spectre Era. | Gilles Barthe, Sunjay Cauligi, Benjamin Grgoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe |
| 2020 | AISTATS | Hypothesis Testing Interpretations and Renyi Differential Privacy. | Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato |
| 2020 | AISTATS | Model-Agnostic Counterfactual Explanations for Consequential Decisions. | Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera |
| 2020 | ESOP | On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. | Gilles Barthe, Raphalle Crubill, Ugo Dal Lago, Francesco Gavazzo |
| 2020 | INDOCRYPT | Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira |
| 2020 | LICS | Deciding Differential Privacy for Programs with Finite Inputs and Outputs. | Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan |
| 2020 | LICS | Universal equivalence and majority of probabilistic programs over finite fields. | Gilles Barthe, Charlie Jacomme, Steve Kremer |
| 2020 | PLDI | Constant-time foundations for the new spectre era. | Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe |
| 2020 | SP | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub |
| 2019 | CCS | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. | Jos Bacelar Almeida, Ccile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub |
| 2019 | CCS | A Machine-Checked Proof of Security for AWS Key Management Service. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grgoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran |
| 2019 | CCS | GALACTICS: Gaussian Sampling for Lattice-Based Constant- Time Implementation of Cryptographic Signatures, Revisited. | Gilles Barthe, Sonia Belad, Thomas Espitau, Pierre-Alain Fouque, Mlissa Rossi, Mehdi Tibouchi |
| 2019 | ESORICS | maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. | Gilles Barthe, Sonia Belad, Gatan Cassiers, Pierre-Alain Fouque, Benjamin Grgoire, Franois-Xavier Standaert |
| 2019 | FMCAD | Verifying Relational Properties using Trace Logic. | Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovcs, Matteo Maffei |
| 2019 | LICS | Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. | Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata |
| 2019 | PLDI | FaCT: a DSL for timing-sensitive computation. | Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grgoire, Gilles Barthe, Ranjit Jhala, Deian Stefan |
| 2019 | PLDI | Bidirectional type checking for relational properties. | Ezgi iek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg |
| 2018 | CCS | Symbolic Proofs for Lattice-Based Cryptography. | Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grgoire, Charlie Jacomme, Elaine Shi |
| 2018 | ESOP | Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. | Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg |
| 2018 | ESOP | An Assertion-Based Program Logic for Probabilistic Programs. | Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2018 | EuroCrypt | Masking the GLP Lattice-Based Signature Scheme at Any Order. | Gilles Barthe, Sonia Belad, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grgoire, Mlissa Rossi, Mehdi Tibouchi |
| 2018 | ICALP | Almost Sure Productivity. | Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva |
| 2017 | CCS | Jasmin: High-Assurance and High-Speed Cryptography. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub |
| 2017 | CCS | A Fast and Verified Software Stack for Secure Function Evaluation. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Vitor Pereira |
| 2017 | CCS | Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions. | Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee |
| 2017 | CRYPTO | Generic Transformations of Predicate Encodings: Constructions and Applications. | Miguel Ambrona, Gilles Barthe, Benedikt Schmidt |
| 2017 | ESOP | Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs. | Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns |
| 2017 | EuroCrypt | Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. | Gilles Barthe, Franois Dupressoir, Sebastian Faust, Benjamin Grgoire, Franois-Xavier Standaert, Pierre-Yves Strub |
| 2017 | ICALP | *-Liftings for Differential Privacy. | Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub |
| 2017 | LPAR | Proving uniformity and independence by self-composition and coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | POPL | Coupling proofs are probabilistic product programs. | Gilles Barthe, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | POPL | Relational cost analysis. | Ezgi iek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann |
| 2016 | CAV | Synthesizing Probabilistic Invariants via Doob's Decomposition. | Gilles Barthe, Thomas Espitau, Luis Mara Ferrer Fioriti, Justin Hsu |
| 2016 | CCS | Strong Non-Interference and Type-Directed Higher-Order Masking. | Gilles Barthe, Sonia Belad, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Pierre-Yves Strub, Rbecca Zucchini |
| 2016 | CCS | Differentially Private Bayesian Programming. | Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jess Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub |
| 2016 | CCS | Advanced Probabilistic Couplings for Differential Privacy. | Gilles Barthe, Nomie Fong, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | EuroCrypt | Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. | Miguel Ambrona, Gilles Barthe, Benedikt Schmidt |
| 2016 | FSE | Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir |
| 2016 | ICALP | A Program Logic for Union Bounds. | Gilles Barthe, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | ISoLA | Facets of Software Doping. | Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns |
| 2016 | LICS | Proving Differential Privacy via Probabilistic Couplings. | Gilles Barthe, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2015 | CCS | Automated Proofs of Pairing-Based Cryptography. | Gilles Barthe, Benjamin Grgoire, Benedikt Schmidt |
| 2015 | EuroCrypt | Verified Proofs of Higher-Order Masking. | Gilles Barthe, Sonia Belad, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Pierre-Yves Strub |
| 2015 | EuroCrypt | Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols. | Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt |
| 2015 | LPAR | Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. | Patrick Baillot, Gilles Barthe, Ugo Dal Lago |
| 2015 | LPAR | Relational Reasoning via Probabilistic Coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Lo Stefanesco, Pierre-Yves Strub |
| 2015 | PKC | Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds. | Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi |
| 2015 | POPL | Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. | Gilles Barthe, Marco Gaboardi, Emilio Jess Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub |
| 2014 | CCS | System-level Non-interference for Constant-time Cryptography. | Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, David Pichardie |
| 2014 | CCS | Synthesis of Fault Attacks on Cryptographic Implementations. | Gilles Barthe, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Jean-Christophe Zapalowicz |
| 2014 | CHES | Making RSA-PSS Provably Secure against Non-random Faults. | Gilles Barthe, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz |
| 2014 | CRYPTO | Automated Analysis of Cryptographic Assumptions in Generic Group Models. | Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt |
| 2014 | POPL | Probabilistic relational verification for cryptographic implementations. | Gilles Barthe, Cdric Fournet, Benjamin Grgoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Bguelin |
| 2013 | CCS | Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir |
| 2013 | CCS | Fully automated analysis of padding-based encryption in the computational model. | Gilles Barthe, Juan Manuel Crespo, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Bguelin |
| 2013 | ICALP | Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. | Gilles Barthe, Federico Olmedo |
| 2013 | LFCS | Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. | Gilles Barthe, Juan Manuel Crespo, Csar Kunz |
| 2013 | PPoPP | From relational verification to SIMD loop synthesis. | Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, Csar Kunz, Mark Marron |
| 2012 | CCS | Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. | Jos Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella-Bguelin |
| 2012 | CCS | Verified security of redundancy-free encryption from Rabin and RSA. | Gilles Barthe, David Pointcheval, Santiago Zanella-Bguelin |
| 2012 | CPP | Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. | Gilles Barthe, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Santiago Zanella-Bguelin |
| 2012 | ESOP | A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. | Gilles Barthe, Delphine Demange, David Pichardie |
| 2012 | FORTE | Secure Multi-Execution through Static Program Transformation. | Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas |
| 2012 | ITP | Computer-Aided Cryptographic Proofs. | Gilles Barthe, Juan Manuel Crespo, Benjamin Grgoire, Csar Kunz, Santiago Zanella-Bguelin |
| 2012 | MPC | Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2012 | POPL | Probabilistic relational reasoning for differential privacy. | Gilles Barthe, Boris Kpf, Federico Olmedo, Santiago Zanella-Bguelin |
| 2012 | SAS | Computer-Aided Cryptographic Proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2011 | CRYPTO | Computer-Aided Security Proofs for the Working Cryptographer. | Gilles Barthe, Benjamin Grgoire, Sylvain Heraud, Santiago Zanella-Bguelin |
| 2011 | FM | Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. | Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna |
| 2011 | FM | Relational Verification Using Product Programs. | Gilles Barthe, Juan Manuel Crespo, Csar Kunz |
| 2011 | ProvSec | Verifiable Security of Boneh-Franklin Identity-Based Encryption. | Gilles Barthe, Federico Olmedo, Santiago Zanella-Bguelin |
| 2010 | CCS | Computational indistinguishability logic. | Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech |
| 2010 | FLOPS | A Functional Framework for Result Checking. | Gilles Barthe, Pablo Buiras, Csar Kunz |
| 2010 | ITP | Programming Language Techniques for Cryptographic Proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2010 | LPAR | On the Equality of Probabilistic Terms. | Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte |
| 2009 | ICFEM | Implementing a Direct Method for Certificate Translation. | Gilles Barthe, Benjamin Grgoire, Sylvain Heraud, Csar Kunz, Anne Pacalet |
| 2009 | POPL | Formal certification of code-based cryptographic proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2009 | SP | Formally Certifying the Security of Digital Signature Schemes. | Santiago Zanella-Bguelin, Gilles Barthe, Benjamin Grgoire, Federico Olmedo |
| 2008 | APLAS | Certified Reasoning in Memory Hierarchies. | Gilles Barthe, Csar Kunz, Jorge Luis Sacchini |
| 2008 | CADE | Certificate Translation. | Gilles Barthe |
| 2008 | CADE | Preservation of Proof Obligations from Java to the Java Virtual Machine. | Gilles Barthe, Benjamin Grgoire, Mariela Pavlova |
| 2008 | CSL | Type-Based Termination with Sized Products. | Gilles Barthe, Benjamin Grgoire, Colin Riba |
| 2008 | ESOP | Certificate Translation in Abstract Interpretation. | Gilles Barthe, Csar Kunz |
| 2008 | SEFM | Preservation of Proof Pbligations for Hybrid Verification Methods. | Gilles Barthe, Csar Kunz, David Pichardie, Julin Samborski-Forlese |
| 2007 | ESOP | A Certified Lightweight Non-interference Java Bytecode Verifier. | Gilles Barthe, David Pichardie, Tamara Rezk |
| 2007 | ESORICS | Security of Multithreaded Programs by Compilation. | Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld |
| 2006 | FLOPS | Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. | Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu |
| 2006 | LPAR | CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. | Gilles Barthe, Benjamin Grgoire, Fernando Pastawski |
| 2006 | SP | Deriving an Information Flow Checker and Certifying Compiler for Java. | Gilles Barthe, Tamara Rezk, David A. Naumann |
| 2006 | SAS | Certificate Translation for Optimizing Compilers. | Gilles Barthe, Benjamin Grgoire, Csar Kunz, Tamara Rezk |
| 2005 | SEFM | Precise Analysis of Memory Consumption using Program Logics. | Gilles Barthe, Mariela Pavlova, Gerardo Schneider |
| 2004 | CADE | A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. | Gilles Barthe, Jan Cederquist, Sabrina Tarento |
| 2004 | CARDIS | Enforcing High-Level Security Properties for Applets. | Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet |
| 2004 | CCS | Formally verifying information flow type systems for concurrent and thread systems. | Gilles Barthe, Leonor Prensa Nieto |
| 2004 | FASE | A Tool-Assisted Framework for Certified Bytecode Verification. | Gilles Barthe, Guillaume Dufay |
| 2004 | VMCAI | Security Types Preserving Compilation: (Extended Abstract). | Gilles Barthe, Amitabh Basu, Tamara Rezk |
| 2003 | POPL | Pure patterns type systems. | Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori |
| 2002 | FASE | Compositional Verification of Secure Applet Interactions. | Gilles Barthe, Dilian Gurov, Marieke Huisman |
| 2002 | PEPM | CPS translating inductive and coinductive types. | Gilles Barthe, Tarmo Uustalu |
| 2002 | VMCAI | A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. | Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simo Melo de Sousa |
| 2001 | ESOP | A Formal Executable Semantics of the JavaCard Platform. | Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simo Melo de Sousa |
| 2001 | FOSSACS | Type Isomorphisms and Proof Reuse in Dependent Type Theory. | Gilles Barthe, Olivier Pons |
| 2000 | FOSSACS | Constructor Subtyping in the Calculus of Inductive Constructions. | Gilles Barthe, Femke van Raamsdonk |
| 2000 | LPAR | Static Reduction Analysis for Imperative Object Oriented Languages. | Gilles Barthe, Bernard P. Serpette |
| 1999 | ESOP | Constructor Subtyping. | Gilles Barthe, Maria Joo Frade |
| 1999 | FLOPS | Partial Evaluation and Non-interference for Object Calculi. | Gilles Barthe, Bernard P. Serpette |
| 1999 | FOSSACS | Expanding the Cube. | Gilles Barthe |
| 1998 | CSL | Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion. | Gilles Barthe |
| 1998 | ICALP | The Relevance of Proof-Irrelevance. | Gilles Barthe |
| 1998 | MFCS | The Semi-Full Closure of Pure Type Systems. | Gilles Barthe |
| 1997 | LFCS | Domain-Free Pure Type Systems. | Gilles Barthe, Morten Heine Srensen |
| 1996 | CSL | On the Subject Reduction Property for Algebraic Type Systems. | Gilles Barthe, Paul-Andr Mellis |
| 1995 | CSL | Congruence Types. | Gilles Barthe, Herman Geuvers |
| 1995 | FCT | A Simple Abstract Semantics for Equational Theories. | Gilles Barthe |