  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.
