Principals of Programming Seminar

Thursday, February 23, 2017 -
3:00pm to 4:00pm

Location:

8102 Gates Hillman Center

Speaker:

ARTHUR AZEVEDO DE AMORIM, Ph.D. Student https://www.cis.upenn.edu/~aarthur/

Event Website:

https://www.cs.cmu.edu/Groups/pop/seminar.html

For More Information, Contact:

angieb@cs.cmu.edu

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.—Arthur Azevedo is graduate student in the Computer and Information Science department at the University of Pennsylvania since 2011. I work with Benjamin Pierce. My main research area is programming languages and verification. I was involved in the project of SAFE, a clean-slate computer environment aimed at security and correctness, helping with its design and specification. I am currently working on bringing some of the hardware tagging infrastructure that we developed for SAFE to more conventional processor designs, formally verifying that the mechanism can be used for enforcing interesting security policies.Faculty Host: Jan Hoffmann

Keywords:

Seminar Series