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 Times are displayed in 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 | |||
08:30 - 08:50 Talk | Verifying Message-Passing Programs with Dependent Behavioural Types PLDI Research Papers Alceste ScalasAston University, Birmingham, UK, Nobuko YoshidaImperial College London, Elias BenussiFaculty Science Ltd Pre-print | ||
08:50 - 09:10 Talk | Toward Efficient Gradual Typing for Structural Types via Coercions PLDI Research Papers Andre KuhlenschmidtIndiana University, Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA | ||
09:10 - 09:30 Talk | 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 |