Gilles Barthe

According to our database, Gilles Barthe authored at least 265 papers between 1995 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

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., March, 2024

Decision and Complexity of Dolev-Yao Hyperproperties.

Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind

Proc. ACM Program. Lang., January, 2024

High-assurance zeroization.

Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe

IACR Trans. Cryptogr. Hardw. Embed. Syst., 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

CoRR, 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

Proceedings of the Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26, 2024

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

CoqQ: Foundational Verification of Quantum Programs.

Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying

Proc. ACM Program. Lang., January, 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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

IACR Trans. Cryptogr. Hardw. Embed. Syst., 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

IACR Cryptol. ePrint Arch., 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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 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

Ultimate SLH: Taking Speculative Load Hardening to the Next Level.

Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom

Proceedings of the 32nd USENIX Security Symposium, 2023

2022

Universal Equivalence and Majority of Probabilistic Programs over Finite Fields.

Gilles Barthe, Charlie Jacomme, Steve Kremer

ACM Trans. Comput. Log., 2022

Safe couplings: coupled refinement types.

Elizaveta Vasilenko, Niki Vazou, Gilles Barthe

Proc. ACM Program. Lang., 2022

On Feller continuity and full abstraction.

Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo

Proc. ACM Program. Lang., 2022

A formal treatment of the role of verified compilers in secure computation.

José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

J. Log. Algebraic Methods Program., 2022

Breaking and Fixing Speculative Load Hardening.

Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom

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

Typing High-Speed Cryptography against Spectre v1.

Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean

IACR Cryptol. ePrint Arch., 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

On Feller Continuity and Full Abstraction (Long Version).

Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo

CoRR, 2022

Flux: Liquid Types for Rust.

Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala

CoRR, 2022

SoK: Practical Foundations for Software Spectre Defenses.

Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan

Proceedings of the 43rd IEEE Symposium on Security and Privacy, 2022

Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs.

Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe

Proceedings of the Static Analysis - 29th International Symposium, 2022

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.

Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

Tidy: Symbolic Verification of Timed Cryptographic Protocols.

Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina

Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, 2022

Symbolic Synthesis of Indifferentiability Attacks.

Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe

Proceedings of the ASIA CCS '22: ACM Asia Conference on Computer and Communications Security, Nagasaki, Japan, 30 May 2022, 2022

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

Deciding accuracy of differential privacy schemes.

Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan

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

Higher-order probabilistic adversarial computations: categorical semantics and program logics.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato

Proc. ACM Program. Lang., 2021

A pre-expectation calculus for probabilistic sensitivity.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Proc. ACM Program. Lang., 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

Structured Leakage and Applications to Cryptographic Constant-Time and Cost.

Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya

IACR Cryptol. ePrint Arch., 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, Li Zhou

IACR Cryptol. ePrint Arch., 2021

SoK: Practical Foundations for Spectre Defenses.

Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan

CoRR, 2021

High-Assurance Cryptography in the Spectre Era.

Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

A Quantum Interpretation of Bunched Logic & Quantum Separation Logic.

Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

Secure Compilation of Constant-Resource Programs.

Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

Scaling Guarantees for Nearest Counterfactual Explanations.

Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera

Proceedings of the AIES '21: AAAI/ACM Conference on AI, 2021

2020

Relational proofs for quantum programs.

Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou

Proc. ACM Program. Lang., 2020

A probabilistic separation logic.

Gilles Barthe, Justin Hsu, Kevin Liao

Proc. ACM Program. Lang., 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

Privacy Profiles and Amplification by Subsampling.

Borja Balle, Gilles Barthe, Marco Gaboardi

J. Priv. Confidentiality, 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

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, David Pichardie

J. Autom. Reason., 2020

High-Assurance Cryptography Software in the Spectre Era.

Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe

IACR Cryptol. ePrint Arch., 2020

PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation.

Gilles Barthe, Roberta De Viti, Peter Druschel, Deepak Garg, Manuel Gomez-Rodriguez, Pierfrancesco Ingo, Matthew Lentz, Aastha Mehta, Bernhard Schölkopf

CoRR, 2020

A survey of algorithmic recourse: definitions, formulations, solutions, and prospects.

Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera

CoRR, 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, Pierre-Yves Strub

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 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

Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Deciding Differential Privacy for Programs with Finite Inputs and Outputs.

Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira

Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 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

Proceedings of the Programming Languages and Systems, 2020

Model-Agnostic Counterfactual Explanations for Consequential Decisions.

Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera

Proceedings of the 23rd International Conference on Artificial Intelligence and Statistics, 2020

Hypothesis Testing Interpretations and Renyi Differential Privacy.

Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato

Proceedings of the 23rd International Conference on Artificial Intelligence and Statistics, 2020

2019

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.

Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu

Proc. ACM Program. Lang., 2019

Relational ⋆⋆\star-Liftings for Differential Privacy.

Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub

Log. Methods Comput. Sci., 2019

Program for TPDP 2016.

Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic

J. Priv. Confidentiality, 2019

Automated Analysis of Cryptographic Assumptions in Generic Group Models.

Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt

J. Cryptol., 2019

System-Level Non-interference of Constant-Time Cryptography. Part I: Model.

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna

J. Autom. Reason., 2019

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.

Patrick Baillot, Gilles Barthe, Ugo Dal Lago

J. Autom. Reason., 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

SoK: Computer-Aided Cryptography.

Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno

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, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran

IACR Cryptol. ePrint Arch., 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, Alley Stoughton, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2019

Automated Methods for Checking Differential Privacy.

Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan

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

Kantorovich Continuity of Probabilistic Programs.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

CoRR, 2019

Coupling Techniques for Reasoning about Quantum Programs.

Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou

CoRR, 2019

Bidirectional type checking for relational properties.

Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 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

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Privacy Amplification by Mixing and Diffusion Mechanisms.

Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek

Proceedings of the Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, 2019

Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy.

Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata

Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, 2019

Verifying Relational Properties using Trace Logic.

Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei

Proceedings of the 2019 Formal Methods in Computer Aided Design, 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

Proceedings of the Computer Security - ESORICS 2019, 2019

Symbolic Methods in Computational Cryptography Proofs.

Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

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, Alley Stoughton, Pierre-Yves Strub

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Monadic refinements for relational cost analysis.

Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger

Proc. ACM Program. Lang., 2018

Proving expected sensitivity of probabilistic programs.

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proc. ACM Program. Lang., 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

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

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

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

IACR Cryptol. ePrint Arch., 2018

Formal verification of higher-order probabilistic programs.

Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu

CoRR, 2018

Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences.

Borja Balle, Gilles Barthe, Marco Gaboardi

Proceedings of the Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, 2018

Almost Sure Productivity.

Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva

Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, 2018

An Assertion-Based Program Logic for Probabilistic Programs.

Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proceedings of the Programming Languages and Systems, 2018

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.

Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg

Proceedings of the Programming Languages and Systems, 2018

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time".

Gilles Barthe, Benjamin Grégoire, Vincent Laporte

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

A relational logic for higher-order programs.

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub

Proc. ACM Program. Lang., 2017

Provably secure compilation of side-channel countermeasures.

Gilles Barthe, Benjamin Grégoire, Vincent Laporte

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

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 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

IACR Cryptol. ePrint Arch., 2017

Reasoning about Divergences for Relaxations of Differential Privacy.

Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata

CoRR, 2017

Relational cost analysis.

Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Coupling proofs are probabilistic product programs.

Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Proving uniformity and independence by self-composition and coupling.

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proceedings of the LPAR-21, 2017

*-Liftings for Differential Privacy.

Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub

Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.

Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh

Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs.

Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns

Proceedings of the Programming Languages and Systems, 2017

Verified Translation Validation of Static Analyses.

Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

Jasmin: High-Assurance and High-Speed Cryptography.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016

Programming language techniques for differential privacy.

Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce

ACM SIGLOG News, 2016

Product programs and relational program logics.

Gilles Barthe, Juan Manuel Crespo, César Kunz

J. Log. Algebraic Methods Program., 2016

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

IET Inf. Secur., 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

Generic Transformations of Predicate Encodings: Constructions and Applications.

Miguel Ambrona, Gilles Barthe, Benedikt Schmidt

IACR Cryptol. ePrint Arch., 2016

Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model.

Miguel Ambrona, Gilles Barthe, Benedikt Schmidt

IACR Cryptol. ePrint Arch., 2016

Advanced Probabilistic Couplings for Differential Privacy.

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

CoRR, 2016

Computer-Aided Verification for Mechanism Design.

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub

Proceedings of the Web and Internet Economics - 12th International Conference, 2016

Verifying Constant-Time Implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi

Proceedings of the 25th USENIX Security Symposium, 2016

Proving Differential Privacy via Probabilistic Couplings.

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Facets of Software Doping.

Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications, 2016

A Program Logic for Union Bounds.

Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Advanced Probabilistic Couplings for Differential Privacy.

Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Differentially Private Bayesian Programming.

Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 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

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Synthesizing Probabilistic Invariants via Doob's Decomposition.

Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

SEFM: software engineering and formal methods.

Gilles Barthe, Alberto Pardo, Gerardo Schneider

Softw. Syst. Model., 2015

High-Assurance Cryptography: Cryptographic Software We Can Trust.

Gilles Barthe

IEEE Secur. Priv., 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

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

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

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

Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181).

Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver

Dagstuhl Reports, 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, Pierre-Yves Strub

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Relational Reasoning via Probabilistic Coupling.

Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Automated Proofs of Pairing-Based Cryptography.

Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt

Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

2014

Formal Verification of an SSA-Based Middle-End for CompCert.

Gilles Barthe, Delphine Demange, David Pichardie

ACM Trans. Program. Lang. Syst., 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

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

System-level non-interference for constant-time cryptography.

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie

IACR Cryptol. ePrint Arch., 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

The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492).

Gilles Barthe, Michael Hicks, Florian Kerschbaum, Dominique Unruh

Dagstuhl Reports, 2014

Leakage Resilience against Concurrent Cache Attacks.

Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Probabilistic relational verification for cryptographic implementations.

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Proving Differential Privacy in Hoare Logic.

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Certified Synthesis of Efficient Batch Verifiers.

Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

2013

Probabilistic Relational Reasoning for Differential Privacy.

Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin

ACM Trans. Program. Lang. Syst., 2013

A certified lightweight non-interference Java bytecode verifier.

Gilles Barthe, David Pichardie, Tamara Rezk

Math. Struct. Comput. Sci., 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 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

Formally Verified Implementation of an Idealized Model of Virtualization.

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, Carlos Luna

Proceedings of the 19th International Conference on Types for Proofs and Programs, 2013

Computer-Aided Security Proofs.

Gilles Barthe

Proceedings of the Quantitative Evaluation of Systems - 10th International Conference, 2013

From relational verification to SIMD loop synthesis.

Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron

Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2013

Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification.

Gilles Barthe, Juan Manuel Crespo, César Kunz

Proceedings of the Logical Foundations of Computer Science, International Symposium, 2013

Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs.

Gilles Barthe, Federico Olmedo

Proceedings of the Automata, Languages, and Programming - 40th International Colloquium, 2013

EasyCrypt: A Tutorial.

Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub

Proceedings of the Foundations of Security Analysis and Design VII, 2013

Verified Computational Differential Privacy with Applications to Smart Metering.

Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin

Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, 2013

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

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

2012

Preface.

Gilles Barthe, Jorge Cuéllar, Javier López, Alexander Pretschner

J. Comput. Secur., 2012

Verified Security of Redundancy-Free Encryption from Rabin and RSA.

Gilles Barthe, David Pointcheval, 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

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

Computer-Aided Cryptographic Proofs.

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin

Proceedings of the Static Analysis - 19th International Symposium, 2012

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs.

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin

Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Computer-Aided Cryptographic Proofs.

Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Secure Multi-Execution through Static Program Transformation.

Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas

Proceedings of the Formal Techniques for Distributed Systems, 2012

A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert.

Gilles Barthe, Delphine Demange, David Pichardie

Proceedings of the Programming Languages and Systems, 2012

Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization.

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Verified Security of Merkle-Damgård.

Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.

Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

An Abstract Model of Certificate Translation.

Gilles Barthe, César Kunz

ACM Trans. Program. Lang. Syst., 2011

Secure information flow by self-composition.

Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk

Math. Struct. Comput. Sci., 2011

Information-theoretic Bounds for Differentially Private Mechanisms.

Gilles Barthe, Boris Köpf

IACR Cryptol. ePrint Arch., 2011

Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language.

Gilles Barthe, Exequiel Rivas

Proceedings of the Trustworthy Global Computing - 6th International Symposium, 2011

Verifiable Security of Boneh-Franklin Identity-Based Encryption.

Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin

Proceedings of the Provable Security - 5th International Conference, 2011

A Computational Indistinguishability Logic for the Bounded Storage Model.

Gilles Barthe, Mathilde Duclos, Yassine Lakhnech

Proceedings of the Foundations and Practice of Security, 2011

Relational Verification Using Product Programs.

Gilles Barthe, Juan Manuel Crespo, César Kunz

Proceedings of the FM 2011: Formal Methods, 2011

Formally Verifying Isolation and Availability in an Idealized Model of Virtualization.

Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna

Proceedings of the FM 2011: Formal Methods, 2011

Beyond Provable Security Verifiable IND-CCA Security of OAEP.

Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin

Proceedings of the Topics in Cryptology - CT-RSA 2011, 2011

Computer-Aided Security Proofs for the Working Cryptographer.

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin

Proceedings of the Advances in Cryptology - CRYPTO 2011, 2011

2010

Security of multithreaded programs by compilation.

Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld

ACM Trans. Inf. Syst. Secur., 2010

Perspectives in Certificate Translation.

Gilles Barthe, César Kunz

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

On the Equality of Probabilistic Terms.

Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Programming Language Techniques for Cryptographic Proofs.

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Functional Framework for Result Checking.

Gilles Barthe, Pablo Buiras, César Kunz

Proceedings of the Functional and Logic Programming, 10th International Symposium, 2010

Robustness Guarantees for Anonymity.

Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

A Machine-Checked Formalization of Sigma-Protocols.

Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud

Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Computational indistinguishability logic.

Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech

Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

2009

Certificate translation for optimizing compilers.

Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk

ACM Trans. Program. Lang. Syst., 2009

Formally Certifying the Security of Digital Signature Schemes.

Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo

Proceedings of the 30th IEEE Symposium on Security and Privacy (SP 2009), 2009

Formal certification of code-based cryptographic proofs.

Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin

Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Implementing a Direct Method for Certificate Translation.

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet

Proceedings of the Formal Methods and Software Engineering, 2009

2008

Preservation of Proof Pbligations for Hybrid Verification Methods.

Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese

Proceedings of the Sixth IEEE International Conference on Software Engineering and Formal Methods, 2008

A Tutorial on Type-Based Termination.

Gilles Barthe, Benjamin Grégoire, Colin Riba

Proceedings of the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24, 2008

Formal Certification of ElGamal Encryption.

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin

Proceedings of the Formal Aspects in Security and Trust, 5th International Workshop, 2008

An Introduction to Certificate Translation.

Gilles Barthe, César Kunz

Proceedings of the Foundations of Security Analysis and Design V, 2008

Certificate translation for specification-preserving advices.

Gilles Barthe, César Kunz

Proceedings of the 7th Workshop on Foundations of Aspect-Oriented Languages, 2008

Certificate Translation in Abstract Interpretation.

Gilles Barthe, César Kunz

Proceedings of the Programming Languages and Systems, 2008

Type-Based Termination with Sized Products.

Gilles Barthe, Benjamin Grégoire, Colin Riba

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Tractable Enforcement of Declassification Policies.

Gilles Barthe, Salvador Cavadini, Tamara Rezk

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Preservation of Proof Obligations from Java to the Java Virtual Machine.

Gilles Barthe, Benjamin Grégoire, Mariela Pavlova

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Certificate Translation.

Gilles Barthe

Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

Certified Reasoning in Memory Hierarchies.

Gilles Barthe, César Kunz, Jorge Luis Sacchini

Proceedings of the Programming Languages and Systems, 6th Asian Symposium, 2008

2007

Secure information flow for a concurrent language with scheduling.

Gilles Barthe, Leonor Prensa Nieto

J. Comput. Secur., 2007

Security types preserving compilation.

Gilles Barthe, Tamara Rezk, Amitabh Basu

Comput. Lang. Syst. Struct., 2007

The MOBIUS Proof Carrying Code Infrastructure.

Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie

Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

07091 Abstracts Collection - Mobility, Ubiquity and Security.

Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld

Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

07091 Executive Summary - Mobility, Ubiquity and Security.

Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld

Proceedings of the Mobility, Ubiquity and Security, 25.02. - 02.03.2007, 2007

2006

Remarks on the equational theory of non-normalizing pure type systems.

Gilles Barthe, Thierry Coquand

J. Funct. Program., 2006

MOBIUS: Mobility, Ubiquity, Security.

Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard

Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

Deriving an Information Flow Checker and Certifying Compiler for Java.

Gilles Barthe, Tamara Rezk, David A. Naumann

Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P 2006), 2006

CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.

Gilles Barthe, Benjamin Grégoire, Fernando Pastawski

Proceedings of the Logic for Programming, 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

Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.

Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu

Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

2005

A computational view of implicit coercions in type theory.

Gilles Barthe

Math. Struct. Comput. Sci., 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

Preventing Timing Leaks Through Transactional Branching Instructions.

Gilles Barthe, Tamara Rezk, Martijn Warnier

Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, 2005

Non-interference for a JVM-like language.

Gilles Barthe, Tamara Rezk

Proceedings of TLDI'05: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2005

Practical Inference for Type-Based Termination in a Polymorphic Setting.

Gilles Barthe, Benjamin Grégoire, Fernando Pastawski

Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

Precise Analysis of Memory Consumption using Program Logics.

Gilles Barthe, Mariela Pavlova, Gerardo Schneider

Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005

Proof Obligations Preserving Compilation.

Gilles Barthe, Tamara Rezk, Ando Saabas

Proceedings of the Formal Aspects in Security and Trust, Third International Workshop, 2005

Formal Methods for Smartcard Security.

Gilles Barthe, Guillaume Dufay

Proceedings of the Foundations of Security Analysis and Design III, 2005

2004

Type-based termination of recursive definitions.

Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto, Tarmo Uustalu

Math. Struct. Comput. Sci., 2004

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming.

Gilles Barthe, Peter Dybjer, Peter Thiemann

J. Funct. Program., 2004

Security Types Preserving Compilation: (Extended Abstract).

Gilles Barthe, Amitabh Basu, Tamara Rezk

Proceedings of the Verification, 2004

A Machine-Checked Formalization of the Random Oracle Model.

Gilles Barthe, Sabrina Tarento

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

A Tool-Assisted Framework for Certified Bytecode Verification.

Gilles Barthe, Guillaume Dufay

Proceedings of the Fundamental Approaches to Software Engineering, 2004

Formally verifying information flow type systems for concurrent and thread systems.

Gilles Barthe, Leonor Prensa Nieto

Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering, 2004

Enforcing High-Level Security Properties for Applets.

Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet

Proceedings of the Smart Card Research and Advanced Applications VI, 2004

A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.

Gilles Barthe, Jan Cederquist, Sabrina Tarento

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003

Setoids in type theory.

Gilles Barthe, Venanzio Capretta, Olivier Pons

J. Funct. Program., 2003

Validation of the JavaCard Platform with Implicit Induction Techniques.

Gilles Barthe, Sorin Stratulat

Proceedings of the Rewriting Techniques and Applications, 14th International Conference, 2003

Pure patterns type systems.

Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

2002

Preface.

Gilles Barthe, Peter Thiemann

Proceedings of the International Workshop in Types in Programming, 2002

A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.

Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa

Proceedings of the Verification, 2002

Efficient Reasoning about Executable Specifications in Coq.

Gilles Barthe, Pierre Courtieu

Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

CPS translating inductive and coinductive types.

Gilles Barthe, Tarmo Uustalu

Proceedings of the 2002 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '02), 2002

Compositional Verification of Secure Applet Interactions.

Gilles Barthe, Dilian Gurov, Marieke Huisman

Proceedings of the Fundamental Approaches to Software Engineering, 2002

Tool-Assisted Specification and Verification of the JavaCard Platform.

Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa

Proceedings of the Algebraic Methodology and Software Technology, 2002

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

An induction principle for pure type systems.

Gilles Barthe, John Hatcliff, Morten Heine Sørensen

Theor. Comput. Sci., 2001

Type Isomorphisms and Proof Reuse in Dependent Type Theory.

Gilles Barthe, Olivier Pons

Proceedings of the Foundations of Software Science and Computation Structures, 2001

A Formal Executable Semantics of the JavaCard Platform.

Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa

Proceedings of the Programming Languages and Systems, 2001

Jakarta: A Toolset for Reasoning about JavaCard.

Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa

Proceedings of the Smart Card Programming and Security, 2001

Tipos principales y cierre semi-completo para sistemas de tipos puros extendidos (trabajo en desarrollo).

Gilles Barthe, Blas C. Ruiz Jiménez

Proceedings of the APPIA-GULP-PRODE 2001: Joint Conference on Declarative Programming, 2001

2000

Domain-free pure type systems.

Gilles Barthe, Morten Heine Sørensen

J. Funct. Program., 2000

Static Reduction Analysis for Imperative Object Oriented Languages.

Gilles Barthe, Bernard P. Serpette

Proceedings of the Logic for Programming and Automated Reasoning, 2000

Constructor Subtyping in the Calculus of Inductive Constructions.

Gilles Barthe, Femke van Raamsdonk

Proceedings of the Foundations of Software Science and Computation Structures, 2000

An Introduction to Dependent Type Theory.

Gilles Barthe, Thierry Coquand

Proceedings of the Applied Semantics, International Summer School, 2000

1999

CPS Translations and Applications: The Cube and Beyond.

Gilles Barthe, John Hatcliff, Morten Heine Sørensen

High. Order Symb. Comput., 1999

Type-checking injective pure type systems.

Gilles Barthe

J. Funct. Program., 1999

Order-Sorted Inductive Types.

Gilles Barthe

Inf. Comput., 1999

Expanding the Cube.

Gilles Barthe

Proceedings of the Foundations of Software Science and Computation Structure, 1999

Partial Evaluation and Non-interference for Object Calculi.

Gilles Barthe, Bernard P. Serpette

Proceedings of the Functional and Logic Programming, 4th Fuji International Symposium, 1999

Constructor Subtyping.

Gilles Barthe, Maria João Frade

Proceedings of the Programming Languages and Systems, 1999

1998

The Semi-Full Closure of Pure Type Systems.

Gilles Barthe

Proceedings of the Mathematical Foundations of Computer Science 1998, 1998

The Relevance of Proof-Irrelevance.

Gilles Barthe

Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998

Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion.

Gilles Barthe

Proceedings of the Computer Science Logic, 12th International Workshop, 1998

1997

Monadic Type Systems: Pure Type Systems for Impure Settings.

Gilles Barthe, John Hatcliff, Peter Thiemann

Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics, 1997

A notion of classical pure type system.

Gilles Barthe, John Hatcliff, Morten Heine Sørensen

Proceedings of the Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, 1997

Reflections on Reflections.

Gilles Barthe, John Hatcliff, Morten Heine Sørensen

Proceedings of the Programming Languages: Implementations, 1997

Termination of Algebraic Type Systems: The Syntactic Approach.

Gilles Barthe, Femke van Raamsdonk

Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

Explicit Substitutions for the Lambda-Calculus.

Gilles Barthe, Fairouz Kamareddine, Alejandro Ríos

Proceedings of the Algebraic and Logic Programming, 6th International Joint Conference, 1997

1996

Towards Lean Proof Checking.

Gilles Barthe, Hugo Elbers

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

On the Subject Reduction Property for Algebraic Type Systems.

Gilles Barthe, Paul-André Melliès

Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995

A Two-Level Approach Towards Lean Proof-Checking.

Gilles Barthe, Mark Ruys, Henk Barendregt

Proceedings of the Types for Proofs and Programs, 1995

Implicit Coercions in Type Systems.

Gilles Barthe

Proceedings of the Types for Proofs and Programs, 1995

Extensions of Pure Type Systems.

Gilles Barthe

Proceedings of the Typed Lambda Calculi and Applications, 1995

Modular Properties of Algebraic Type Systems.

Gilles Barthe, Herman Geuvers

Proceedings of the Higher-Order Algebra, 1995

A Simple Abstract Semantics for Equational Theories.

Gilles Barthe

Proceedings of the Fundamentals of Computation Theory, 10th International Symposium, 1995

Congruence Types.

Gilles Barthe, Herman Geuvers

Proceedings of the Computer Science Logic, 9th International Workshop, 1995