Principles of Programming Seminar

Monday, October 17, 2016 -
3:30pm to 4:30pm

Location:

Traffic21 Classroom 6501 Gates & Hillman Centers

Speaker:

JUSTIN HSU, Ph.D. Student http://justinh.su/

For More Information, Contact:

bcook@cs.cmu.edu

Probabilistic couplings are a standard mathematical abstraction for reasoning about two distributions. In formal verification, they are often called probabilistic liftings. While these two concepts are quite related, the connection has been little explored. In fact, probabilistic couplings and liftings are a powerful, compositional tool for reasoning about probabilistic programs. I will give a brief survey of different uses of probabilistic liftings, and then show how to use these ideas in the relational program logic pRHL. Joint with Gilles Barthe, Thomas Espitau, Benjamin Gregoire, and Pierre-Yves Strub. — Justin Hsu is a final year graduate student at the University of Pennsylvania, advised by Benjamin Pierce and Aaron Roth. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory. Faculty Host: Matt Fredrikson

Keywords:

Seminar Series