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 general recursive session types. It develops a logical relation for progress-sensitive noninterference (PSNI) for intuitionistic linear logic session types (ILLST), tackling the challenges non-termination and concurrency pose, and shows that logical equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition, using a biorthogonality argument. A distinguishing feature of the logical relation is its stratification with an observation index (as opposed to a step or unfolding index), a crucial shift to make the logical relation closed under parallel composition in a concurrent setting. To demonstrate practicality of the logical relation, the paper develops an information flow control (IFC) refinement type system for ILLST, with support of secrecy-polymorphic processes, and shows that well-typed programs are self-related by the logical relation and thus enjoy PSNI. The refinement type system has been implemented in a type checker, featuring local security theories to support secrecy-polymorphic processes.

翻译：程序等价性是对程序进行推理和证明程序性质的关键。例如，在非干涉性中，需要证明程序等价性达到观察者秘密级别。逻辑关系是此类证明的有力工具。逻辑关系最近才被应用于会话类型——但仅限于终止性语言。本文将其推广至一般递归会话类型。本文针对直觉线性逻辑会话类型（ILLST）开发了一种针对进度敏感的非干涉性（PSNI）的逻辑关系，解决了非终止性和并发性带来的挑战，并利用双正交性论证证明了逻辑等价性相对于弱互模拟在并行组合下的封闭性是可靠且完备的。该逻辑关系的一个显著特征是其按观测索引（而非步骤或展开索引）进行分层，这一关键转变使得逻辑关系在并发环境下对并行组合封闭。为展示该逻辑关系的实用性，本文为ILLST开发了一种支持秘密多态进程的信息流控制（IFC）精化类型系统，并证明了良类型程序在该逻辑关系下是自相关的，从而满足PSNI。该精化类型系统已在一个类型检查器中实现，并具有支持秘密多态进程的局部安全理论。