23 citations · 40 across the 7 of their papers we have counts for
9 papers · 1 filter
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…
Finding Safety in Numbers with Secure Allegation Escrows
Venkat Arun, Aniket Kate, Deepak Garg +2
For fear of retribution, the victim of a crime may be willing to report it only if other victims of the same perpetrator also step forward. Common examples include 1) identifying 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…
Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation
Carmine Abate, Roberto Blanco, Deepak Garg +3
(CROPPED TO FIT IN ARXIV'S SILLY LIMIT. SEE PDF FOR COMPLETE ABSTRACT.) We are the first to thoroughly explore a large space of formal secure compilation criteria based on robust p…
Types for Information Flow Control: Labeling Granularity and Semantic Models
Vineet Rajani, Deepak Garg
Language-based information flow control (IFC) tracks dependencies within a program using sensitivity labels and prohibits public outputs from depending on secret inputs. In particu…