23 citations · 40 across the 7 of their papers we have counts for
7 papers · 1 filter
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. Hirsch, Deepak Garg
We present Pirouette, a language for typed higher-order functional choreographic programming. Pirouette offers programmers the ability to write a centralized functional program and…
Trace-Relating Compiler Correctness and Secure Compilation
Carmine Abate, Roberto Blanco, Stefan Ciobaca +6
Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equiva…
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…
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…
Robustly Safe Compilation or, Efficient, Provably Secure Compilation
Marco Patrignani, Deepak Garg
Secure compilers generate compiled code that withstands many target-level attacks such as alteration of control flow, data leaks or memory corruption. Many existing secure compiler…