279 citations · 1.1k across the 46 of their papers we have counts for
12 papers · 1 filter
Higher-order probabilistic adversarial computations: Categorical semantics and program logics
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi +3
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with pri…
Graded Hoare Logic and its Categorical Semantics
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard +1
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend o…
Formal verification of higher-order probabilistic programs
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe +3
Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic prog…
An Assertion-Based Program Logic for Probabilistic Programs
Gilles Barthe, Thomas Espitau, Marco Gaboardi +3
Research on deductive verification of probabilistic programs has considered expectation-based logics, where pre- and post-conditions are real-valued functions on states, and assert…
Advanced Probabilistic Couplings for Differential Privacy
Gilles Barthe, Noémie Fong, Marco Gaboardi +3
Differential privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information.…
A program logic for union bounds
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire +2
We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analy…
Proving Differential Privacy via Probabilistic Couplings
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire +2
In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based…
Really Natural Linear Indexed Type Checking
Arthur Azevedo de Amorim, Emilio Jesús Gallego Arias, Marco Gaboardi +1
Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices,…
Proving differential privacy in Hoare logic
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias +3
Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a sin…
Linear Dependent Types and Relative Completeness
Ugo Dal Lago, Marco Gaboardi
A system of linear dependent types for the lambda calculus with full higher-order recursion, called dlPCF, is introduced and proved sound and relatively complete. Completeness hold…
An Implicit Characterization of PSPACE
Marco Gaboardi, Jean-Yves Marion, Simona Ronchi Della Rocca
We present a type system for an extension of lambda calculus with a conditional construction, named STAB, that characterizes the PSPACE class. This system is obtained by extending…
Categorical Models for a Semantically Linear Lambda-calculus
Marco Gaboardi, Mauro Piccolo
This paper is about a categorical approach to model a very simple Semantically Linear lambda calculus, named Sll-calculus. This is a core calculus underlying the programming langua…