POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 16:30 - 16:55 at Amphitheater 44 - Semantic Foundations Chair(s): Lars Birkedal

Program sensitivity measures how robust program’s outputs are to changes in its input. This is a useful measure in fields like differential privacy and cyber-physical systems, in order to guarantee that input changes have a limited effect on the program behavior. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that a k-sensitive function maps inputs that are at distance d to outputs that are at most at distance k*d. Program sensitivity is thus an analog of Lipschitz continuity for programs.

To make these ideas concrete, Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate their expressiveness by giving a model for the deterministic fragment of Fuzz.

Thu 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 17:20: Semantic FoundationsPOPL at Amphitheater 44
Chair(s): Lars BirkedalAarhus University
16:30 - 16:55
Arthur Azevedo de AmorimUniversity of Pennsylvania, USA, Ikram CheriguiENS Paris, Marco GaboardiSUNY Buffalo, USA, Justin Hsu, Shin-ya KatsumataKyoto University
16:55 - 17:20
Steffen SmolkaCornell University, Praveen KumarCornell University, Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London
DOI File Attached