Tue 25 Jun 2019 09:10 - 09:30 at 224AB - Type Systems I Chair(s): Ranjit Jhala

Relational type systems have been designed for several applications
including information flow, differential privacy, and cost analysis.
In order to achieve the best results, these systems often use
relational refinements and relational effects to
maximally exploit the similarity in the structure of the two programs
being compared. Relational type systems are appealing for relational
properties because they deliver simpler and more precise verification
than what could be derived from typing the two programs
separately. However, relational type systems do not yet achieve the
practical appeal of their non-relational counterpart, in part because
of the lack of a general foundation for implementing them.

In this paper, we take a step in this direction by developing
bidirectional relational type checking for systems with
relational refinements and effects. Our approach achieves the benefits
of bidirectional type checking, in a relational setting. In
particular, it significantly reduces the need for typing annotations
through the combination of type checking and type inference. In order
to highlight the foundational nature of our approach, we develop
bidirectional versions of several relational type systems which
incrementally combine many different components needed for expressive
relational analysis.

Tue 25 Jun

pldi-2019-papers
08:30 - 09:30: PLDI Research Papers - Type Systems I at 224AB
Chair(s): Ranjit JhalaUniversity of California, San Diego
pldi-2019-papers08:30 - 08:50
Talk
Alceste ScalasAston University, Birmingham, UK, Nobuko YoshidaImperial College London, Elias BenussiFaculty Science Ltd
Pre-print
pldi-2019-papers08:50 - 09:10
Talk
Andre KuhlenschmidtIndiana University, Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA
pldi-2019-papers09:10 - 09:30
Talk
Ezgi ÇiçekFacebook London, Weihao QuUniversity at Buffalo, SUNY, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems
Media Attached