279 citations · 1.1k across the 46 of their papers we have counts for
4 papers · 2 filters
Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe +2
Relational type systems have been designed for several applications including information flow, differential privacy, and cost analysis. In order to achieve the best results, these…
Relational Cost Analysis for Functional-Imperative Programs
Weihao Qu, Marco Gaboardi, Deepak Garg
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost anal…
Probabilistic Relational Reasoning via Metrics
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +1
The Fuzz programming language [Reed and Pierce, 2010] uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity prope…
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Alejandro Aguirre, Gilles Barthe, Lars Birkedal +3
We extend the simply-typed guarded -calculus with discrete probabilities and endow it with a program logic for reasoning about relational properties of guarded probabilistic com…