Principals of Programming Seminar

Monday, May 1, 2017 - 3:30pm to 4:30pm


Traffic21 Classroom 6501 Gates Hillman Centers


MARCO GABOARDI, Assistant Professor

Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs.  Relational program verification can be used for reasoning about a broad range of properties: information flow security, relative cost, sensitivity or continuity, differential privacy, etc. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.In this talk, he will present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed λ-calculus with inductive types and recursive definitions.  RHOL retains the type-directed flavor of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms.  He will present some of the property of RHOL, some examples and sound embeddings for several existing relational type systems.  He will then briefly discuss two extensions of the basic RHOL for guarded recursion and for probabilistic programs.Joint work with Alejandro Aguille, Gilles Barthe, Deepak Garg, and Pierre-Yves Strub—Marco Gaboardi is an assistant professor at the University at Buffalo, SUNY. Previously, he was a faculty at the University of Dundee, Scotland. He received his PhD from the University of Torino, Italy, and the Institute National Polytechnique de Lorraine, France.  He was a visitor scholar at the University of Pennsylvania and at Harvard’s CRCS center, and recipient of a EU Marie Curie Fellowship.  His research is in programming language design and implementation, and in differential privacy.Faculty Host: Jan Hoffmann

Event Website:

For More Information, Contact:


Seminar Series