Gilles Barthe -

Registered user since Mon 11 Nov 2019

Name:Gilles Barthe

Bio:

I am scientific director at MPI-SP, Bochum, Germany and a part-time research professor at IMDEA Software Institute, Madrid, Spain. My research interests include programming languages and program verification, software and system security, cryptography, privacy, and mathematical logic. My most recent research develops programming language techniques and verification methods for security, with a focus on relational verification and its applications to cryptography and differential privacy.

Country:Germany

Affiliation:MPI-SP; IMDEA Software Institute

Personal website:http://gbarthe.github.io

Research interests:Formal methods, programming languages and program verification, software and system security, cryptography and privacy

Contributions

POPL 2023	Author of CoqQ: Foundational Verification of Quantum Programs within the POPL-track
SAS 2022	Author of Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs within the SAS-track
ICFP 2022	Author of Safe Couplings: Coupled Refinement Types within the ICFP Papers and Events-track Author of On Feller Continuity and Full Abstraction within the ICFP Papers and Events-track
PLDI 2022	Author of (POPL 2021) A Pre-Expectation Calculus for Probabilistic Sensitivity within the SIGPLAN Track-track Author of (PLDI 2020) Constant-Time Foundations for the New Spectre Era within the SIGPLAN Track-track
ICFP 2021	Author of On Continuation-Passing Transformations and Expected Cost Analysis within the Research Papers-track Author of Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics within the Research Papers-track
POPL 2021	Author of Deciding Accuracy of Differential Privacy Schemes within the POPL-track Author of A Pre-Expectation Calculus for Probabilistic Sensitivity within the POPL-track
PriSC 2021	Author of High-Assurance Cryptography in the Spectre Era within the PriSC 2021-track
PLDI 2020	Author of Constant-Time Foundations for the New Spectre Era within the PLDI Research Papers-track
POPL 2020	Author of Formal Verification of a Constant-Time Preserving C Compiler within the Research Papers-track Author of Relational Proofs for Quantum Programs within the Research Papers-track Author of A Probabilistic Separation Logic within the Research Papers-track
PLDI 2019	Author of Bidirectional Type Checking for Relational Properties within the PLDI Research Papers-track Author of FaCT: A DSL for Timing-Sensitive Computation within the PLDI Research Papers-track
ETAPS 2019	Author of ETAPS Steering committee meeting within the Social-track Satellite Events in Executive Board
POPL 2019	Author of Formal Verification of Higher-Order Probabilistic Programs within the Research Papers-track
PriSC 2019	Committee Member in Program Committee within the PriSC 2019-track
POPL 2018	Committee Member in Program Committee within the Research Papers-track Author of Monadic refinements for relational cost analysis within the Research Papers-track Author of Proving Expected Sensitivity of Probabilistic Programs within the Artifact Evaluation-track Author of Proving expected sensitivity of probabilistic programs within the Research Papers-track
ICFP 2017	Author of A Relational Logic for Higher-Order Programs within the Research Papers-track
POPL 2017	Author of Coupling proofs are probabilistic product programs within the POPL-track Author of Relational Cost Analysis within the POPL-track
ESOP 2015	Committee Member in Program Committee within the ESOP-track