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

Displayed time zone: Tijuana, Baja California change

08:30 - 09:30
Type Systems IPLDI Research Papers at 224AB
Chair(s): Ranjit Jhala University of California, San Diego
Verifying Message-Passing Programs with Dependent Behavioural Types
PLDI Research Papers
Alceste Scalas Aston University, Birmingham, UK, Nobuko Yoshida Imperial College London, Elias Benussi Faculty Science Ltd
Toward Efficient Gradual Typing for Structural Types via Coercions
PLDI Research Papers
Andre Kuhlenschmidt Indiana University, Deyaaeldeen Almahallawi Indiana University, Jeremy G. Siek Indiana University, USA
Bidirectional Type Checking for Relational Properties
PLDI Research Papers
Ezgi Çiçek Facebook London, Weihao Qu University at Buffalo, SUNY, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems
Media Attached