论文标题
递归会话逻辑关系
Recursive Session Logical Relations
论文作者
论文摘要
程序等效性是用于推理和证明程序属性的支点。例如，为非干预，显示了直到观察者的保密级别的程序等效性。此类证明的强大推动力是逻辑关系。逻辑关系直到最近才用于会话类型，但专门用于终止语言。本文将逻辑关系扩展到递归会话类型。它为线性会话类型的进度敏感性非干预提供了逻辑关系，应对非终止和并发姿势的挑战。这些贡献包括保密性 - 造型过程以及与元心理的逻辑关系。一个区别的特征是选择逻辑关系的“步骤索引”，从而可以自然的传递性和声音证明。
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.
