Linear Dependent Types for Differential Privacy TypeChecker
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
doc
emacs
examples/dfuzz
lib
src
LICENSE
Makefile
README.md
README.users
dFuzz.why

README.md

dfuzz: Linear Dependent Types for Differential Privacy

This repository implements a type checker for the linear dependent lambda calculus of [1].

The details of the algorithm are on a IFL 2014 paper:

http://arxiv.org/abs/1503.04522

[1] Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. 2013. Linear dependent types for differential privacy. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '13). ACM, New York, NY, USA, 357-370. DOI=10.1145/2429069.2429113 http://doi.acm.org/10.1145/2429069.2429113