Program equivalence is the heart of reasoning about and proving properties of programs. To assert noninterference, for example, a program is shown to be equivalent to itself up to the confidentiality level of an observer. A powerful enabler for such proofs are logical relations, which, guided by the type structure, prescribe when two programs are indistinguishable. Logical relations enjoy ample exploration in functional languages, including languages with general recursion and a higher-order store—yet logical relations for session types only exist for terminating languages. This paper scales logical relations to general recursive session types. It develops a logical relation for progress-sensitive equivalence for intuitionistic linear logic session types, tackling the challenges non-termination and concurrency pose. In particular, the relation only equates a diverging program with another diverging one and accounts for nondeterminism of scheduling. The logical relation has two distinguishing characteristics: it is (i) indexed with an intuitionistic linear sequent, validating cut reductions and affording biorthogonal closure, and (ii) bound by an observation index, stratifying the logical relation in the presence of recursion. Biorthogonal closure validates the logical relation, proving that the induced equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition. Soundness guarantees that the equivalence has enough discriminatory power, completeness ensures that it is maximally permissive. The logical relation is then put to test on the example of noninterference.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Recursive Logical Relations for Intuitionistic Linear Logic Session Types

  • Stephanie Balzer,
  • Farzaneh Derakhshan,
  • Robert Harper,
  • Yue Yao

摘要

Program equivalence is the heart of reasoning about and proving properties of programs. To assert noninterference, for example, a program is shown to be equivalent to itself up to the confidentiality level of an observer. A powerful enabler for such proofs are logical relations, which, guided by the type structure, prescribe when two programs are indistinguishable. Logical relations enjoy ample exploration in functional languages, including languages with general recursion and a higher-order store—yet logical relations for session types only exist for terminating languages. This paper scales logical relations to general recursive session types. It develops a logical relation for progress-sensitive equivalence for intuitionistic linear logic session types, tackling the challenges non-termination and concurrency pose. In particular, the relation only equates a diverging program with another diverging one and accounts for nondeterminism of scheduling. The logical relation has two distinguishing characteristics: it is (i) indexed with an intuitionistic linear sequent, validating cut reductions and affording biorthogonal closure, and (ii) bound by an observation index, stratifying the logical relation in the presence of recursion. Biorthogonal closure validates the logical relation, proving that the induced equivalence is sound and complete with regard to closure of weak bisimilarity under parallel composition. Soundness guarantees that the equivalence has enough discriminatory power, completeness ensures that it is maximally permissive. The logical relation is then put to test on the example of noninterference.