Session Types with Arithmetic Refinements and Their Application to Work Analysis

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.