Author name cluster

Gilles Barthe

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

15 papers

2 author rows

NeurIPS Conference 2019 Conference Paper

Privacy Amplification by Mixing and Diffusion Mechanisms

Borja Balle
Gilles Barthe
Marco Gaboardi
Joseph Geumlek

A fundamental result in differential privacy states that the privacy guarantees of a mechanism are preserved by any post-processing of its output. In this paper we investigate under what conditions stochastic post-processing can amplify the privacy of a mechanism. By interpreting post-processing as the application of a Markov operator, we first give a series of amplification results in terms of uniform mixing properties of the Markov process defined by said operator. Next we provide amplification bounds in terms of coupling arguments which can be applied in cases where uniform mixing is not available. Finally, we introduce a new family of mechanisms based on diffusion processes which are closed under post-processing, and analyze their privacy via a novel heat flow argument. On the applied side, we generalize the analysis of "privacy amplification by iteration" in Noisy SGD and show it admits an exponential improvement in the strongly convex case, and study a mechanism based on the Ornstein–Uhlenbeck diffusion process which contains the Gaussian mechanism with optimal post-processing on bounded inputs as a special case.

PDF Details

NeurIPS Conference 2018 Conference Paper

Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences

Borja Balle
Gilles Barthe
Marco Gaboardi

Differential privacy comes equipped with multiple analytical tools for the design of private data analyses. One important tool is the so-called "privacy amplification by subsampling" principle, which ensures that a differentially private mechanism run on a random subsample of a population provides higher privacy guarantees than when run on the entire population. Several instances of this principle have been studied for different random subsampling methods, each with an ad-hoc analysis. In this paper we present a general method that recovers and improves prior analyses, yields lower bounds and derives new instances of privacy amplification by subsampling. Our method leverages a characterization of differential privacy as a divergence which emerged in the program verification community. Furthermore, it introduces new tools, including advanced joint convexity and privacy profiles, which might be of independent interest.

PDF Details

LPAR Conference 2017 Conference Paper

Proving uniformity and independence by self-composition and coupling

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

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL—whose proofs are formal versions of proofs by coupling—can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant.

Details

LPAR Conference 2015 Conference Paper

Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs

Patrick Baillot
Gilles Barthe
Ugo Dal Lago

Abstract We define a call-by-value variant of Gödel’s System \(\mathsf {T} \) with references, and equip it with a linear dependent type and effect system, called \(\mathsf {d}\ell \mathsf {T} \), that can estimate the complexity of programs, as a function of the size of their inputs. We prove that the type system is intentionally sound, in the sense that it over-approximates the complexity of executing the programs on a variant of the CEK abstract machine. Moreover, we define a sound and complete type inference algorithm which critically exploits the subrecursive nature of \(\mathsf {d}\ell \mathsf {T} \). Finally, we demonstrate the usefulness of \(\mathsf {d}\ell \mathsf {T} \) for analyzing the complexity of cryptographic reductions by providing an upper bound for the constructed adversary of the Goldreich-Levin theorem.

Details

LPAR Conference 2015 Conference Paper

Relational Reasoning via Probabilistic Coupling

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

Abstract Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance —a probabilistic version of a monotonicity property. While the mathematical definition of coupling looks rather complex and cumbersome to manipulate, we show that the relational program logic pRHL—the logic underlying the EasyCrypt cryptographic proof assistant—already internalizes a generalization of probabilistic coupling. With this insight, constructing couplings is no harder than constructing logical proofs. We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verify several couplings in EasyCrypt.

Details

CSL Conference 2008 Conference Paper

Type-Based Termination with Sized Products

Gilles Barthe
Benjamin Grégoire
Colin Riba

Abstract Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursive calls operate on smaller arguments. However, many systems using type-based termination rely on a semantical anomaly to guarantee strong normalization; namely, they impose that non-recursive elements of a datatype, e. g. the empty list, have size 1 instead of 0. This semantical anomaly also prevents functions such as quicksort to be given a precise typing. The main contribution of this paper is a type system that remedies this anomaly, and still ensures termination. In addition, our type system features prenex stage polymorphism, a weakening of existential quantification over stages, and is precise enough to type quicksort as a non-size increasing function. Moreover, our system accomodate stage addition with all positive inductive types.

Details

LPAR Conference 2006 Conference Paper

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

Gilles Barthe
Benjamin Grégoire
Fernando Pastawski

Abstract Sized types provides a type-based mechanism to enforce termination of recursive definitions in typed λ -calculi. Previous work has provided strong indications that type-based termination provides an appropriate foundation for proof assistants based on type theory; however, most work to date has been confined to non-dependent type systems. In this article, we introduce a variant of the Calculus of Inductive Constructions with sized types and study its meta theoretical properties: subject reduction, normalization, and thus consistency and decidability of type-checking and of size-inference. A prototype implementation has been developed alongside case studies.

Details

TCS Journal 2001 Journal Article

An induction principle for pure type systems

Gilles Barthe
John Hatcliff
Morten Heine B. Sørensen

We present an induction principle for pure type systems and use that principle to define CPS translations and to solve the problem of expansion postponement for a large class of pure type systems. Our principle strengthens and generalises similar principles by Dowek et al. [12] and Barthe et al. [6], which have been respectively used to define η-long normal forms and CPS translations for the systems of Barendregt's λ-cube [2, 3].

Details DOI

TCS Journal 2001 Journal Article

Weak normalization implies strong normalization in a class of non-dependent pure type systems

Gilles Barthe
John Hatcliff
Morten Heine Sørensen

The Barendregt–Geuvers–Klop conjecture states that every weakly normalizing pure type system is also strongly normalizing. We show that this is true for a uniform class of systems which includes, e. g. , the left-hand side of Barendregt's λ-cube as well as the system λU. This seems to be the first result giving a positive answer to the conjecture not merely for some concrete systems for which strong normalization is known to hold, but for a uniform class of systems in which not all systems are strongly normalizing.

Details DOI

LPAR Conference 2000 Conference Paper

Static Reduction Analysis for Imperative Object Oriented Languages

Gilles Barthe
Bernard P. Serpette

Abstract we define a generic control-flow sensitive static analysis, Static Reduction Analysis (SRA), for an untyped object-oriented language featuring side-effects and exceptions. While its aims and range of applications closely relate to Control Flow Analysis (CFA), SRA exhibits a distinguishing feature: it only deals with abstract syntax tree (AST) nodes and does not involve approximations of environments nor stores.

Details

CSL Conference 1999 Conference Paper

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

Gilles Barthe

Abstract Pure Type Systems ( PTS β s) provide a parametric framework for typed λ -calculi à la Church [1, 2, 10, 11]. One important aspect of PTS β s is to feature a definitional equality based on β -conversion. In some instances however, one desires a stronger definitional equality based on βη -conversion. The need for such a strengthened definitional equality arises for example when using type theory as a logical framework or in categorical type theory.

Details

I&C Journal 1999 Journal Article

Order-Sorted Inductive Types

Gilles Barthe

SystemF ω ⩽is an extension of systemF ω with subtyping and bounded quantification. Order-sorted algebra is an extension of many-sorted algebra with overloading and subtyping. We combine both formalisms to obtainIF ω ⩽, a higher-order typedλ-calculus with subtyping, bounded quantification, and order-sorted inductive types, i. e. , data types with built-in subtyping and overloading. Moreover we show thatIF ω ⩽enjoys important meta-theoretic properties, including confluence, strong normalization, subject reduction, and decidability of type checking.

Details DOI

MFCS Conference 1998 Conference Paper

The Semi-Full Closure of Pure Type Systems

Gilles Barthe

Abstract We show that every functional Pure Type System may be extended to a semi-full Pure Type System. Moreover, the extension is conservative and preserves weak normalization. Based on these results, we give a new, conceptually simple type-checking algorithm for functional Pure Type Systems.

Details

CSL Conference 1997 Conference Paper

On the Subject Reduction Property for Algebraic Type Systems

Gilles Barthe
Paul-André Melliès

Abstract Algebraic type systems provide a general framework for the study of the interaction between typed λ-calculi and typed rewriting systems. A major problem in the development of a general theory for algebraic type systems is to prove that typing is preserved under reduction (Subject Reduction lemma). In this paper, we propose a general technique to prove Subject Reduction for a large class of algebraic type systems. The idea is to consider for every (functional) algebraic type system a labelled syntax for which Subject Reduction is easy to prove and then prove the equivalence between the labelled and standard syntaxes whenever the labelled system is strongly normalising. The equivalence can then be used to recover confluence, strong normalisation and subject reduction for the standard syntax.

Details

CSL Conference 1996 Conference Paper

Congruence Types

Gilles Barthe
Herman Geuvers

Abstract We introduce a type-theoretical framework in which canonical term rewriting systems can be represented faithfully both from the logical and the computational points of view. The framework is based on congruence types, a new syntax which combines inductive, algebraic and quotient types. Congruence types improve on existing work to combine type theories with algebraic rewriting by making explicit the fact that the term-rewriting systems under consideration are initial models of an equational theory. As a result, the interaction gustavo: thesisween the type theory and the algebraic types (rewriting systems) is much more powerful than in previous work. Congruence types can be used (i) to introduce initial models of canonical term-rewriting systems (ii) to obtain a suitable computational behavior of a definable operation (iii) to provide an elegant solution to the problem of equational reasoning in type theory.

Details