Computing Sensitivity By Parametricity: An Approach to Higher-Order Functions

Abstract

In the digital era, companies routinely gather and publish sensitive user information, raising significant privacy concerns. Differential privacy offers a robust solution by adding controlled noise to query results, ensuring individual privacy even against adversaries with additional information. This noise level is determined by the query’s sensitivity, necessitating automated systems to compute it accurately. The programming language SPAR, based on the λSpar calculus and embedded in Haskell, addresses this need by leveraging Haskells function space for tracking sensitivity. This thesis advances SPAR with an independent function space. We explores mechanisms for extending a shallow-embedded language to support both shallow and deep embeddings. We showcase normalization by evaluation techniques for evaluating a somewhat dependent type language. We provide a soundness proof for λSpar with the function space and l1 norm.