BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
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 DBLP: Barthe:Gilles

Facilitated 5 volumes:

ASE 2012DemoTrackPrCo
ASE 2012ToCo
ESOP 2011Ed
SEFM 2011Ed
VMCAI 2010Ed

Contributed to:

POPL 20152015
POPL 20142014
ICALP (2) 20132013
PPoPP 20132013
ESOP 20122012
POPL 20122012
SAS 20122012
FM 20112011
FLOPS 20102010
POPL 20092009
CSL 20082008
ESOP 20082008
IJCAR 20082008
SEFM 20082008
ESOP 20072007
FLOPS 20062006
SAS 20062006
QAPL 20052006
SEFM 20052005
TLCA 20052005
FASE 20042004
IJCAR 20042004
VMCAI 20042004
POPL 20032003
RTA 20032003
FASE 20022002
PEPM 20022002
VMCAI 20022002
ESOP 20012001
FoSSaCS 20012001
FoSSaCS 20002000
ESOP 19991999
FLOPS 19991999
FoSSaCS 19991999
CSL 19981998
ICALP 19981998
ALP/HOA 19971997
PLILP 19971997
CSL 19961996
TLCA 19951995
ESOP 20172017
ESOP 20182018
CAV (1) 20162016
POPL 20172017
POPL 20182018
PLDI 20192019
POPL 20192019
POPL 20202020

Wrote 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 (, 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 (, 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.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.