Travelled to:1 × Australia
1 × China
1 × Czech Republic
1 × Denmark
1 × Estonia
1 × Hungary
1 × India
1 × Korea
1 × Latvia
1 × Portugal
1 × South Africa
2 × France
2 × Germany
2 × Ireland
2 × Spain
3 × The Netherlands
3 × United Kingdom
4 × Italy
4 × Japan
5 × USA
Collaborated with:B.Grégoire ∅ C.Kunz J.Hsu D.Pichardie M.Gaboardi T.Rezk S.Z.Béguelin F.v.Raamsdonk P.Strub G.Dufay D.G.0001 F.Olmedo B.P.Serpette M.Pavlova T.Espitau J.M.Crespo S.Stratulat T.Uustalu O.Pons M.J.Frade P.Melliès L.Jakubiec S.M.d.Sousa E.Çiçek D.Demange P.Buiras C.Riba M.Warnier G.Schneider F.Pastawski J.Cederquist S.Tarento A.Basu D.Gurov M.Huisman F.Kamareddine A.Ríos J.Hatcliff M.H.Sørensen A.A.0001 Kevin Liao B.Köpf G.Betarte J.D.Campo C.Luna J.Samborski-Forlese J.Forest V.Rusu H.Cirstea C.Kirchner L.Liquori L.M.F.Fioriti S.Gulwani M.Marron P.R.D'Argenio S.Biewer B.Finkbeiner H.Hermanns J.H.0002 I.Radicek F.Zuleger Weihao Qu M.Ying Nengkun Yu L.Zhou E.J.G.Arias A.Roth C.Fournet N.Swamy L.Birkedal A.Bizjak T.Sato S.Blazy Rémi Hutin V.Laporte Alix Trieu Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner R.Jhala D.Stefan
Talks about:type (13) relat (11) probabilist (10) program (10) formal (9) proof (9) verif (8) java (6) system (5) base (5)
♂ Person: Gilles Barthe
DBLP: Barthe:Gilles
Facilitated 5 volumes:
DemoTrackPrCoToCo
Ed
Ed
EdContributed to:
20152014
2013
201320122012
2012
2011
20102009
20082008
20082008200720062006
20062005
2005
2004200420042003
20032002
200220022001
2001200019991999199919981998
199719971996199520172018
201620172018
201920192020Wrote 56 papers:
- POPL-2015-BartheGAHRS #approximate #design #difference #higher-order #privacy #refinement #relational
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy (GB, MG, EJGA, JH, AR, PYS), pp. 55–68.
- POPL-2014-BartheFGSSB #encryption #implementation #probability #relational #verification
- Probabilistic relational verification for cryptographic implementations (GB, CF, BG, PYS, NS, SZB), pp. 193–206.
- ICALP-v2-2013-BartheO #composition #difference #logic #privacy #probability #relational #source code #theorem
- Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs (GB, FO), pp. 49–60.
- PPoPP-2013-BartheCKGM #relational #synthesis #verification
- From relational verification to SIMD loop synthesis (GB, JMC, SG, CK, MM), pp. 123–134.
- ESOP-2012-BartheDP
- A Formally Verified SSA-Based Middle-End — Static Single Assignment Meets CompCert (GB, DD, DP), pp. 47–66.
- POPL-2012-BartheKOB #difference #privacy #probability #reasoning #relational
- Probabilistic relational reasoning for differential privacy (GB, BK, FO, SZB), pp. 97–110.
- SAS-2012-BartheGB #encryption #proving
- Computer-Aided Cryptographic Proofs (GB, BG, SZB), pp. 1–2.
- FM-2011-BartheBCL #verification
- Formally Verifying Isolation and Availability in an Idealized Model of Virtualization (GB, GB, JDC, CL), pp. 231–245.
- FM-2011-BartheCK #relational #source code #using #verification
- Relational Verification Using Product Programs (GB, JMC, CK), pp. 200–214.
- FLOPS-2010-BartheBK #framework #functional
- A Functional Framework for Result Checking (GB, PB, CK), pp. 72–86.
- POPL-2009-BartheGB #certification #encryption #proving
- Formal certification of code-based cryptographic proofs (GB, BG, SZB), pp. 90–101.
- CSL-2008-BartheGR #termination #type system
- Type-Based Termination with Sized Products (GB, BG, CR), pp. 493–507.
- ESOP-2008-BartheK #abstract interpretation
- Certificate Translation in Abstract Interpretation (GB, CK), pp. 368–382.
- IJCAR-2008-BartheGP #java #proving #virtual machine
- Preservation of Proof Obligations from Java to the Java Virtual Machine (GB, BG, MP), pp. 83–99.
- SEFM-2008-BartheKPS #hybrid #proving #verification
- Preservation of Proof Pbligations for Hybrid Verification Methods (GB, CK, DP, JSF), pp. 127–136.
- ESOP-2007-BarthePR #bytecode #java #lightweight #verification
- A Certified Lightweight Non-interference Java Bytecode Verifier (GB, DP, TR), pp. 125–140.
- FLOPS-2006-BartheFPR #coq #proving #reasoning #recursion
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (GB, JF, DP, VR), pp. 114–129.
- SAS-2006-BartheGKR #compilation #optimisation
- Certificate Translation for Optimizing Compilers (GB, BG, CK, TR), pp. 301–317.
- QAPL-2005-BartheRW06 #branch #transaction
- Preventing Timing Leaks Through Transactional Branching Instructions (GB, TR, MW), pp. 33–55.
- SEFM-2005-BarthePS #analysis #logic #memory management #precise #using
- Precise Analysis of Memory Consumption using Program Logics (GB, MP, GS), pp. 86–95.
- TLCA-2005-BartheGP #polymorphism #termination #type system
- Practical Inference for Type-Based Termination in a Polymorphic Setting (GB, BG, FP), pp. 71–85.
- FASE-2004-BartheD #bytecode #framework #verification
- A Tool-Assisted Framework for Certified Bytecode Verification (GB, GD), pp. 99–113.
- IJCAR-2004-BartheCT #formal method #random
- A Machine-Checked Formalization of the Generic Model and the Random Oracle Model (GB, JC, ST), pp. 385–399.
- VMCAI-2004-BartheBR #compilation #security
- Security Types Preserving Compilation: (GB, AB, TR), pp. 2–15.
- POPL-2003-BartheCKL #type system
- Pure patterns type systems (GB, HC, CK, LL), pp. 250–261.
- RTA-2003-BartheS #framework #induction #platform #validation
- Validation of the JavaCard Platform with Implicit Induction Techniques (GB, SS), pp. 337–351.
- FASE-2002-BartheGH #composition #interactive #verification
- Compositional Verification of Secure Applet Interactions (GB, DG, MH), pp. 15–32.
- PEPM-2002-BartheU #continuation #induction
- CPS translating inductive and coinductive types (GB, TU), pp. 131–142.
- VMCAI-2002-BartheDJS #virtual machine
- A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines (GB, GD, LJ, SMdS), pp. 32–45.
- ESOP-2001-BartheDJSS #execution #framework #platform #semantics
- A Formal Executable Semantics of the JavaCard Platform (GB, GD, LJ, BPS, SMdS), pp. 302–319.
- FoSSaCS-2001-BartheP #dependent type #morphism #proving #reuse #type system
- Type Isomorphisms and Proof Reuse in Dependent Type Theory (GB, OP), pp. 57–71.
- FoSSaCS-2000-BartheR #calculus #induction #type system
- Constructor Subtyping in the Calculus of Inductive Constructions (GB, FvR), pp. 17–34.
- ESOP-1999-BartheF #type system
- Constructor Subtyping (GB, MJF), pp. 109–127.
- FLOPS-1999-BartheS #calculus #partial evaluation
- Partial Evaluation and Non-inference for Object Calculi (GB, BPS), pp. 53–67.
- FoSSaCS-1999-Barthe
- Expanding the Cube (GB), pp. 90–103.
- CSL-1998-Barthe #normalisation #type system
- Existence and Uniqueness of Normal Forms in Pure Type Systems with βη-Conversion (GB), pp. 241–259.
- ICALP-1998-Barthe
- The Relevance of Proof-Irrelevance (GB), pp. 755–768.
- ALP-1997-BartheKR #λ-calculus
- Explicit Substitutions for the λ-Calculus (GB, FK, AR), pp. 209–223.
- ALP-1997-BartheR #algebra #approach #termination #type system
- Termination of Algebraic Type Systems: The Syntactic Approach (GB, FvR), pp. 174–193.
- PLILP-1997-BartheHS
- Reflections on Reflections (GB, JH, MHS), pp. 241–258.
- CSL-1996-BartheM #algebra #on the #reduction #type system
- On the Subject Reduction Property for Algebraic Type Systems (GB, PAM), pp. 34–57.
- TLCA-1995-Barthe #type system
- Extensions of Pure Type Systems (GB), pp. 16–31.
- ESOP-2017-DArgenioBBFH #analysis #formal method #source code
- Is Your Software on Dope? - Formal Analysis of Surreptitiously “enhanced” Programs (PRD, GB, SB, BF, HH), pp. 83–110.
- ESOP-2018-0001BBBG0 #markov #probability #reasoning #relational #λ-calculus
- Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus (AA0, GB, LB, AB, MG, DG0), pp. 214–241.
- ESOP-2018-BartheEGGHS #logic #probability #source code
- An Assertion-Based Program Logic for Probabilistic Programs (GB, TE, MG, BG, JH, PYS), pp. 117–144.
- CAV-2016-BartheEFH #composition #invariant #probability
- Synthesizing Probabilistic Invariants via Doob's Decomposition (GB, TE, LMFF, JH), pp. 43–61.
- POPL-2017-BartheGHS #probability #proving #source code
- Coupling proofs are probabilistic product programs (GB, BG, JH, PYS), pp. 161–174.
- POPL-2017-CicekBG0H #cost analysis #relational
- Relational cost analysis (EÇ, GB, MG, DG0, JH0), pp. 316–329.
- POPL-2018-BartheEGHS #probability #proving #source code
- Proving expected sensitivity of probabilistic programs (GB, TE, BG, JH, PYS), p. 29.
- POPL-2018-RadicekBG0Z #cost analysis #monad #relational
- Monadic refinements for relational cost analysis (IR, GB, MG, DG0, FZ), p. 32.
- PLDI-2019-CauligiSJBWRGBJ #domain-specific language #named
- FaCT: a DSL for timing-sensitive computation (SC, GS, BJ, FB, RSW, JR, BG, GB, RJ, DS), pp. 174–189.
- PLDI-2019-CicekQBG0 #bidirectional #relational #type checking
- Bidirectional type checking for relational properties (EÇ, WQ, GB, MG, DG0), pp. 533–547.
- POPL-2019-SatoABGGH #approximate #convergence #higher-order #optimisation #probability #reasoning #source code #verification
- Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization (TS, AA0, GB, MG, DG0, JH), p. 30.
- POPL-2020-BartheBGHLPT #c #compilation #verification
- Formal verification of a constant-time preserving C compiler (GB, SB, BG, RH, VL, DP, AT), p. 30.
- POPL-2020-BartheHL #logic #probability
- A probabilistic separation logic (GB, JH, KL), p. 30.
- POPL-2020-BartheHYYZ #proving #quantum #relational #source code
- Relational proofs for quantum programs (GB, JH, MY, NY, LZ), p. 29.