Gilles Barthe
where else to find them
no profile links on file
what they talk about
all 5 in the filters
where they keep going back
- POPL4 editions2021–2025
all 7 in the filters
on a stage with
all 41 in the filters
who talks about the same things
- Benjamin Gregoire6 talks
- Martin Avanzini4 talks
- Benjamin Lucien Kaminski14 talks
- Joost-Pieter Katoen14 talks
- Michael Carbin14 talks
- Pierre-Yves Strub4 talks
| title | conference | date |
|---|---|---|
| Traq: Estimating the Quantum Cost of Classical Programs | PLanQC 2026 | 2026-01-12 |
Traq provides an automated pipeline that compiles a classical CPL source language to unitary quantum code, extracts three cost functions (worst-case have cost… | ||
| Decompiling for Constant-Time Analysis | PriSC 2026 | 2026-01-11 |
Claims that mainstream decompilers can hide timing leaks by turning branches into conditional moves, tests five popular decompilers and finds unsoundness for… | ||
| Preservation of Speculative Constant-time by Compilation | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Shows that common compilers (GCC -O0 and -O1 and Jasmin) produce speculatively insecure binaries from speculatively constant-time sources, then builds a… | ||
| Preservation of speculative constant-time by compilation | POPL 2025 | 2025-01-19 |
Shows that mainstream compilers (GCC -O0/-O1 and Jasmin) can break speculative constant-time by removing or introducing Spectre-v1 leaks, gives concrete… | ||
| Automating equational proofs in Dirac notation | POPL 2025 | 2025-01-19 |
Proves that Dirac notation’s first-order theory is decidable by reducing formulas to the theory of real closed fields (Tarski) and shows practical equivalence… | ||
| A quantitative probabilistic relational Hoare logic | POPL 2025 | 2025-01-19 |
eRHL is a program logic whose pre/post-conditions are nonnegative real-valued functions on pairs of states, and it gives upper bounds on expectations… | ||
| Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…) | OOPSLA 2024 | 2024-10-20 |
Proposes a EHL + pRHL hopping rule that reduces expectation-based proof goals to related programs, implements it inside EasyCrypt integration, and proves… | ||
| A modal type-theory of expected cost in higher-order probabilistic programs | OOPSLA 2024 | 2024-10-20 |
pλ-amor is a graded modal type theory that encodes probabilities, potentials and expected cost at the type level and proves bounds for higher-order… | ||
| Decision and Complexity of Dolev-Yao Hyperproperties | POPL 2024 | 2024-01-14 |
Provides the first decision procedure for Dolev–Yao hyperproperties under a bounded number of sessions and subterm-convergent equational theories, proving… | ||
| CoqQ: Foundational Verification of Quantum Programs | POPL 2023 | 2023-01-15 |
CoqQ is a Coq framework that formalizes a quantum language, proves a program logic sound with respect to a denotational semantics built on MathComp and… | ||
| Safe Couplings: Coupled Refinement Types | ICFP 2022 | 2022-09-11 |
Enhances refinement types with a coupling-based connective that captures relational properties like expected sensitivity and proves that output-distance is… | ||
| On Feller Continuity and Full Abstraction | ICFP 2022 | 2022-09-11 |
Shows that in a call-by-value higher-order lambda calculus with sampling and only continuous real-valued primitives, Feller-continuity on the induced labelled… | ||
| A Pre-Expectation Calculus for Probabilistic Sensitivity | POPL 2021 | 2021-01-17 |
A relational pre-expectation calculus gives computable upper bounds on the Kantorovich lifting of output distributions, proved sound and (in cases) continuous… | ||
| Deciding Accuracy of Differential Privacy Schemes | POPL 2021 | 2021-01-17 |
Introduces accuracy as a parametric notion based on distance to disagreement (dd) and output closeness γ, yielding an explicit alpha–beta–gamma claim: e.g. for… | ||
| Verifying Constant-Time Implementations | USENIX Security '16 | 2016-08-10 |
Claims an automated verifier, ct-verif, that proves constant-time for optimized LLVM code by reducing the two-execution security property to safety of a… | ||
| nothing matches | ||