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.

Conference Day
Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Type Systems IPLDI Research Papers at 224AB
Chair(s): Ranjit JhalaUniversity of California, San Diego
Verifying Message-Passing Programs with Dependent Behavioural Types
PLDI Research Papers
Alceste ScalasAston University, Birmingham, UK, Nobuko YoshidaImperial College London, Elias BenussiFaculty Science Ltd
Toward Efficient Gradual Typing for Structural Types via Coercions
PLDI Research Papers
Andre KuhlenschmidtIndiana University, Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA
Bidirectional Type Checking for Relational Properties
PLDI Research Papers
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