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
Install
You need ocaml >= 4.07.1 plus dune, and the why3 dependencies plus standard gnu tools like gcc and make.
You can obtain all that by doing:
$ opam install --deps-only -d -t .
then run
$ why3 config --detect
$ dune build
to compile the tool
How to compile and run programs
To typecheck a program type:
$ dune exec -- dfuzz examples/dfuzz/cdf.fz
Running the program is still not supported in dFuzz.