Session Types with Arithmetic Refinements and Their Application to Work Analysis

TL;DR

This paper extends session types with arithmetic refinements to specify and verify data structure properties and amortized costs, introducing new algorithms and demonstrating practical verification examples.

Contribution

It introduces a novel extension of session types using linear arithmetic refinements to express and verify cost properties, along with algorithms for type checking and reconstruction.

Findings

Type equality is undecidable with arithmetic refinements.

A practical incomplete algorithm for type equality is proposed.

The system can verify amortized cost properties in process protocols.

Abstract

Session types statically prescribe bidirectional communication protocols for message-passing processes and are in a Curry-Howard correspondence with linear logic propositions. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system by using index refinements from linear arithmetic capturing intrinsic attributes of data structures and algorithms so that we can express and verify amortized cost of programs using ergometric types. We show that, despite the decidability of Presburger arithmetic, type equality and therefore also type checking are now undecidable, which stands in contrast to analogous dependent refinement type systems from functional languages. We also present a practical incomplete algorithm for type equality and an algorithm for type checking which is complete relative to an oracle for type equality. Process expressions in this explicit language are rather verbose, so we also introduce an implicit form and a sound and complete algorithm for reconstructing explicit programs, borrowing ideas from the proof-theoretic technique of focusing. We conclude by illustrating our systems and algorithms with a variety of examples that have been verified in our implementation.