log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
A semantic account of metric preservation
Monday, March 27, 2017, 10:00-11:00 am Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

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 metrics on the input and output spaces, requiring that an r-sensitive function map inputs that are at distance d to outputs that are at distance at most r * d. Program sensitivity is thus an analogue of Lipschitz continuity for programs.

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, 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. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz.

Bio

Arthur Azevedo de Amorim is a graduate student in the Computer and Information Science department at the University of Pennsylvania since 2011. His main research area is programming languages and verification. He was involved in the project SAFE, a clean-slate computer environment aimed at security and correctness, helping with its design and specification. He is currently working on bringing some of the hardware tagging infrastructure that was developed for SAFE to more conventional processor designs, formally verifying that the mechanism can be used for enforcing interesting security policies.

This talk is organized by Mike Hicks