We present an expressive framework, called PrivInfer, for writing and verifying differentially private machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic language with constructs for performing Bayesian inference. Then, differential privacy of programs is established using a relational refinement type system, in which refinements on probability types are indexed by a metric on distributions. Our framework leverages recent developments in Bayesian inference, probabilistic program- ming languages, and in relational refinement types. We demonstrate the expressiveness of PrivInfer by verifying privacy for several examples of private Bayesian inference.
Marco Gaboardi is an assistant professor in the Department of Computer Science and Engineering at the University at Buffalo, SUNY. Previously, he was a faculty at the University of Dundee, Scotland. He received his PhD from the University of Torino, Italy, and the Institute National Polytechnique de Lorraine, France. He was a visitor scholar at the University of Pennsylvania and at Harvard’s CRCS center. He has been the recipient of a EU Marie Curie Fellowship. His research is in programming language design and implementation, and in differential privacy.