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。该精化类型系统已实现为类型检查器，通过局部安全理论支持保密多态进程。