Recursive Session Logical Relations

TL;DR

This paper extends logical relations to recursive session types, enabling reasoning about noninterference in non-terminating, concurrent session-typed programs with progress sensitivity.

Contribution

It introduces a logical relation for recursive session types, addressing non-termination and concurrency, and develops secrecy-polymorphic processes with a novel step index approach.

Findings

Logical relation for recursive session types established.

Proof of transitivity and soundness achieved.

Enables reasoning about noninterference in complex session-typed programs.

Abstract

Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an observer is shown. A powerful enabler for such proofs are logical relations. Logical relations only recently were adopted for session types--but exclusively for terminating languages. This paper scales logical relations to recursive session types. It develops a logical relation for progress-sensitive noninterference for linear session types, tackling the challenges non-termination and concurrency pose. The contributions include secrecy-polymorphic processes and the logical relation with metatheory. A distinguishing feature is the choice of "step index" of the logical relation, allowing for a natural proof of transitivity and soundness.