Author name cluster

Benjamin Grégoire

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.

5 papers

1 author row

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

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

CSL Conference 2005 Conference Paper

On the Role of Type Decorations in the Calculus of Inductive Constructions

Bruno Barras
Benjamin Grégoire

Abstract In proof systems like Coq [16], proof-checking involves comparing types modulo β -conversion, which is potentially a time-consuming task. Significant speed-ups are achieved by compiling proof terms, see [9]. Since compilation erases some type information, we have to show that convertibility is preserved by type erasure. This article shows the equivalence of the Calculus of Inductive Constructions (formalism of Coq) and its domain-free version where parameters of inductive types are also erased. It generalizes and strengthens significantly a similar result by Barthe and Sørensen [5] on the class of functional Domain-free Pure Type Systems.

Details