Marco Gaboardi (University at Buffalo, SUNY), A semantic account of metric preservation in presence of probabilities.



Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metric preservation with respect to the metrics on the input and output spaces: requiring that an r-sensitive function maps inputs that are at distance d to outputs that are at distance at most r*d. I will present some recent work where we started the study of program sensitivity and metric preservation from a denotational point of view. I will introduced metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity and metric preservation. I will then discuss how to extend this structure to account for metrics over probability distributions. In particular, I will discuss how these metrics can be used to guarantee programs differentially private.