Bidirectional Type Checking for Relational Properties

TL;DR

This paper introduces a bidirectional relational type checking approach that enhances the practicality and precision of relational type systems by reducing annotations and combining various components for expressive analysis.

Contribution

It develops the first bidirectional relational type checking framework with refinements and effects, improving usability and foundational understanding.

Findings

Reduces need for typing annotations

Combines multiple components for expressive relational analysis

Enhances practicality of relational type systems

Abstract

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 foundations 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.