pith. sign in

arxiv: 2309.00192 · v2 · submitted 2023-09-01 · 💻 cs.PL

Logical Relations for Session-Typed Concurrency

Stephanie Balzer , Farzaneh Derakhshan , Robert Harper , Yue Yao This is my paper

Pith reviewed 2026-05-24 07:05 UTC · model grok-4.3

classification 💻 cs.PL
keywords logical relationssession typesprogress-sensitive noninterferenceinformation flow controlrecursionconcurrencybiorthogonalityweak bisimilarity
0
0 comments X

The pith

Logical equivalence defined by an observation-indexed relation is sound and complete for weak bisimilarity closed under parallel composition in recursive session types.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a logical relation for intuitionistic linear logic session types that accommodates general recursion and concurrency. Stratification by an observation index rather than step or unfolding index allows the relation to be closed under parallel composition. The induced logical equivalence is proved sound and complete with respect to the closure of weak bisimilarity under parallel composition by a biorthogonality argument. An information flow control refinement type system with secrecy polymorphism is introduced, and well-typed programs are shown to be self-related by the logical relation, hence to satisfy progress-sensitive noninterference. The work supplies a method for establishing program equivalence up to secrecy level in a concurrent recursive setting.

Core claim

The logical relation, stratified by an observation index, defines logical equivalence that is sound and complete with respect to closure of weak bisimilarity under parallel composition for intuitionistic linear logic session types; well-typed programs in the associated information flow control refinement type system are self-related and therefore enjoy progress-sensitive noninterference.

What carries the argument

The observation-index stratified logical relation, which carries the biorthogonality argument to establish closure under parallel composition.

If this is right

  • Logical equivalence can be used to prove progress-sensitive noninterference for concurrent recursive session-typed programs.
  • Well-typed programs in the information flow control refinement type system are self-related and satisfy progress-sensitive noninterference.
  • The refinement type system supports secrecy-polymorphic processes through local security theories.
  • The type checker implementation allows practical verification of the noninterference property.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The stratification technique may transfer to logical relations in other process calculi that combine recursion with concurrency.
  • The soundness and completeness result could support equivalence-based proofs of additional security properties beyond noninterference.
  • Automated checking of self-relatedness might be integrated into session-type compilers to enforce noninterference by construction.

Load-bearing premise

The observation-index stratification suffices to make the logical relation closed under parallel composition in the presence of recursion and concurrency.

What would settle it

A pair of programs related by the logical relation whose parallel composition fails to be weakly bisimilar, or a well-typed program in the refinement type system that violates progress-sensitive noninterference.

Figures

Figures reproduced from arXiv: 2309.00192 by Farzaneh Derakhshan, Robert Harper, Stephanie Balzer, Yue Yao.

Figure 1
Figure 1. Figure 1: Running example: (a) pre-/post-state of process configurations, (b) session types. Bob or any walk-in customer ("guest"). The same must hold for Bob. We can express this policy by defining corresponding secrecy levels and a lattice over them: guest ⊑ alice ⊑ bank guest ⊑ bob ⊑ bank [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Process term typing rules and signature checking rules of SESSION. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Two implementations of the verifier process: (left) secure version, (right) insecure version. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Configuration typing rules of SESSION. Spawn proc(𝑦𝛼, (𝑥 ← 𝑋 [𝛾] ← Δ1);𝑄) ↦→ (Δ ′ 1 ⊢ 𝑋 = 𝑃 :: 𝑥 ′ : 𝐵 ∈ Σ) proc(𝑥0,𝛾ˆ(𝑃)) proc(𝑦𝛼, [𝑥0/𝑥]𝑄) (Δ ′ 1 , 𝑥′ ⊩ 𝛾 : Δ1, 𝑥0, 𝑥0 fresh) D-Fwd proc(𝑦𝛼, 𝐹𝑌 [𝛾]) ↦→ (𝑥 ′ : 𝐶 ⊢ 𝐹𝑦 = Fwd𝐶,𝑦′←𝑥 ′ :: 𝑦 ′ : 𝐶 ∈ Σ) proc(𝑦𝛼, Fwd𝐶,𝑦𝛼←𝑥𝛽 ) (𝑥 ′ , 𝑦′ ⊩ 𝛾 : 𝑥𝛽 , 𝑦𝛼 ) 1snd proc(𝑦𝛼, (close𝑦𝛼 )) ↦→ msg(close𝑦𝛼 ) 1rcv msg(close𝑦𝛼 ) proc(𝑥𝛽 , (wait𝑦𝛼 ;𝑄)) ↦→ proc(𝑥𝛽 , 𝑄) ⊕snd proc(𝑦𝛼,… view at source ↗
Figure 5
Figure 5. Figure 5: Asynchronous dynamics of SESSION. generation of the carrier channel 𝑦𝛼 upon receipt in its continuation proc(𝑢𝛾 , ( [𝑥𝛽 /𝑤] [𝑦𝛼+1/𝑦𝛼 ]𝑃)) as well (see rule ⊗rcv). Generations are a convenient way of allocating new names, while guaranteeing proper linkage between a message and the sender’s continuation. Like bound variables, bound channels are subject to 𝛼-variance and capture-avoiding substitution, as usua… view at source ↗
Figure 6
Figure 6. Figure 6: Recursive session logical relation (RSLR) for ILLST. [PITH_FULL_IMAGE:figures/full_fig_p011_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Labeled transition system induced by RSLR. [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Process term typing rules and signature checking rules of CONSESSION. [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Configuration typing rules of CONSESSION. [PITH_FULL_IMAGE:figures/full_fig_p018_9.png] view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a logical relation for recursive intuitionistic linear logic session types (ILLST), stratified by an observation index rather than step or unfolding indices. It proves that the induced logical equivalence is sound and complete with respect to the closure of weak bisimilarity under parallel composition, via a biorthogonality argument. It further presents an information-flow-control refinement type system supporting secrecy polymorphism, shows that well-typed programs are self-related (hence satisfy progress-sensitive noninterference), and implements the type checker.

Significance. If the central claims hold, the work is a notable advance in applying logical relations to non-terminating concurrent session types. The observation-index stratification and biorthogonality argument directly address closure under parallel composition, a key obstacle for recursion and concurrency. The IFC refinement system and its implementation provide a concrete demonstration of utility for PSNI proofs.

major comments (2)
  1. [§4 (logical relation definition and closure lemma)] The soundness and completeness theorems rest on the logical relation being closed under parallel composition (invoked in the biorthogonality argument). The paper replaces step/unfolding indices with an observation index precisely to obtain this closure. However, it is not shown that the observation index remains well-founded when two observation-indexed processes are placed in parallel and each may perform independent observations; without an explicit lemma establishing that the index decreases or is preserved in a well-founded manner under such composition, the inductive argument for closure does not go through.
  2. [§4.3 (recursive case) and proof of Theorem 5.1] The handling of recursion in the presence of concurrency is central to the claim that the observation-indexed relation is closed under parallel composition. The abstract and introduction assert that the shift to observation indices suffices, but the manuscript provides no concrete derivation or example showing how the index behaves for recursive processes that can perform observations independently before synchronizing.
minor comments (2)
  1. [§3] Notation for the observation index and its interaction with session types could be introduced with a small running example before the full definition.
  2. [§6] The implementation section would benefit from a brief description of how local security theories are represented in the type checker.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed and constructive report. The comments focus on the need for greater explicitness regarding well-foundedness of the observation index under parallel composition and recursion. We address each point below and will revise the manuscript accordingly to strengthen the presentation without altering the core technical development.

read point-by-point responses

  1. Referee: [§4 (logical relation definition and closure lemma)] The soundness and completeness theorems rest on the logical relation being closed under parallel composition (invoked in the biorthogonality argument). The paper replaces step/unfolding indices with an observation index precisely to obtain this closure. However, it is not shown that the observation index remains well-founded when two observation-indexed processes are placed in parallel and each may perform independent observations; without an explicit lemma establishing that the index decreases or is preserved in a well-founded manner under such composition, the inductive argument for closure does not go through.

    Authors: The observation index is defined to decrease precisely on observable actions (independent of internal steps or unfoldings), and the biorthogonality argument in §4 is constructed precisely so that the relation is closed under parallel composition by quantifying over all possible observations of the combined system. Nevertheless, we agree that an auxiliary lemma making the preservation of well-foundedness under parallel composition fully explicit would improve readability and address the concern directly. We will add this lemma (and its proof) in the revised manuscript. revision: yes

  2. Referee: [§4.3 (recursive case) and proof of Theorem 5.1] The handling of recursion in the presence of concurrency is central to the claim that the observation-indexed relation is closed under parallel composition. The abstract and introduction assert that the shift to observation indices suffices, but the manuscript provides no concrete derivation or example showing how the index behaves for recursive processes that can perform observations independently before synchronizing.

    Authors: Because the index is indexed by observations rather than unfoldings, recursive processes may unfold and perform internal computation arbitrarily often without decreasing the index; only actual observations decrease it. This design is what permits independent observations by parallel recursive processes while preserving well-foundedness. We acknowledge that a worked example would make the behavior clearer. We will insert a short concrete derivation (for a pair of recursive processes performing independent observations before a synchronisation) immediately after the statement of the closure property in the revised version. revision: yes

Circularity Check

0 steps flagged

No circularity; logical relation and closure proofs are independent of inputs

full rationale

The paper defines a logical relation for ILLST using an observation-index stratification chosen to support closure under parallel composition, then separately proves (via biorthogonality) that logical equivalence coincides with the closure of weak bisimilarity under parallel composition. The IFC refinement type system is shown to entail self-relatedness by an independent argument. No quoted step reduces a claimed prediction or uniqueness result to a fitted parameter, self-citation, or definitional tautology; all central obligations are stated as external proof goals grounded in standard linear logic and bisimulation. This is the normal non-circular case.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based on abstract only; no free parameters, invented entities, or ad-hoc axioms are identifiable. Relies on standard assumptions of intuitionistic linear logic and weak bisimilarity.

axioms (2)
  • domain assumption Intuitionistic linear logic session types (ILLST) provide the underlying type discipline for concurrency.
    Invoked as the base for the logical relation and refinement types.
  • standard math Biorthogonality argument establishes soundness and completeness of logical equivalence w.r.t. weak bisimilarity closure.
    Used in the proof strategy for the logical relation.

pith-pipeline@v0.9.0 · 5761 in / 1375 out tokens · 17939 ms · 2026-05-24T07:05:41.907995+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

67 extracted references · 67 canonical work pages

  1. [1]

    In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) , Andrew W

    A Core Calculus of Dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) , Andrew W. Appel and Alex Aiken (Eds.). ACM, 147–160. https://doi.org/10.1145/292540.292555 Amal Ahmed

    work page doi:10.1145/292540.292555

  2. [2]

    In15th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol

    Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In15th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 3924). Springer, 69–83. https://doi.org/10.1007/11693024_6 Amal Ahmed, Derek Dreyer, and Andreas Rossberg

    work page doi:10.1007/11693024_6

  3. [3]

    In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    State-Dependent Representation Independence. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 340–353. https://doi.org/10.1145/ 1480881.1480925 Kalev Alpernas, Cormac Flanagan, Sadjad Fouladi, Leonid Ryzhyk, Mooly Sagiv, Thomas Schmitz, and Keith Winstein

    work page arXiv

  4. [4]

    Proceedings of the ACM on Programming Languages 2, OOPSLA (2018), 118:1–118:26

    Secure Serverless Computing using Dynamic Information Flow Control. Proceedings of the ACM on Programming Languages 2, OOPSLA (2018), 118:1–118:26. https://doi.org/10.1145/3276488 Andrew W. Appel and David A. McAllester

    work page doi:10.1145/3276488 2018

  5. [5]

    ACM Transactions on Programming Languages and Systems (TOPLAS) 23, 5 (2001), 657–683

    An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. ACM Transactions on Programming Languages and Systems (TOPLAS) 23, 5 (2001), 657–683. https://doi.org/10. 1145/504709.504712 Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao

    work page arXiv 2001

  6. [6]

    In 28th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol

    Manifest Deadlock-Freedom for Shared Session Types. In 28th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 11423) . Springer, 611–639. https://doi.org/10.1007/978-3-030-17184-1_22 Nick Benton and Chung-Kil Hur

    work page doi:10.1007/978-3-030-17184-1_22

  7. [7]

    In 14th ACM SIGPLAN International Conference on Functional Programming (ICFP)

    Biorthogonality, Step-Indexing and Compiler Correctness. In 14th ACM SIGPLAN International Conference on Functional Programming (ICFP) . ACM, 97–108. https://doi.org/10.1145/1596550.1596567 Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho

    work page doi:10.1145/1596550.1596567

  8. [8]

    Linear logic propositi ons as session types

    Linear Logic Propositions as Session Types. Mathematical Structures in Computer Science 26, 3 (2016), 367–423. https://doi.org/10.1017/S0960129514000218 Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini

    work page doi:10.1017/s0960129514000218 2016

  9. [9]

    Information and Computation 238 (2014), 68–105

    Typing Access Control and Secure Information Flow in Sessions. Information and Computation 238 (2014), 68–105. https://doi.org/10.1016/j.ic.2014.07.005 Sara Capecchi, Ilaria Castellani, and Mariangiola Dezani-Ciancaglini

    work page doi:10.1016/j.ic.2014.07.005 2014

  10. [10]

    Mathematical Structures in Computer Science 26, 8 (2016), 1352–1394

    Information flow safety in multiparty sessions. Mathematical Structures in Computer Science 26, 8 (2016), 1352–1394. https://doi.org/10.1017/S0960129514000619 Sara Capecchi, Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Tamara Rezk

    work page doi:10.1017/s0960129514000619 2016

  11. [11]

    In 21th International Conference on Concurrency Theory (CONCUR)

    Session Types for Access and Information Flow Control. In 21th International Conference on Concurrency Theory (CONCUR) . 237–252. https: //doi.org/10.1007/978-3-642-15375-4_17 Simon Castellan and Nobuko Yoshida

    work page doi:10.1007/978-3-642-15375-4_17

  12. [12]

    Proceedings of the ACM on Programming Languages 3, POPL (2019), 27:1–27:29

    Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. Proceedings of the ACM on Programming Languages 3, POPL (2019), 27:1–27:29. https: //doi.org/10.1145/3290340 Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Jorge A. Pérez

    work page doi:10.1145/3290340 2019

  13. [13]

    Formal Aspects of Computing 28, 4 (2016), 669–696

    Self-Adaptation and Secure Information Flow in Multiparty Communications. Formal Aspects of Computing 28, 4 (2016), 669–696. https://doi.org/10.1007/s00165-016- 0381-3 Iliano Cervesato and Andre Scedrov

    work page doi:10.1007/s00165-016- 2016

  14. [14]

    Information and Computation 207, 10 (2009), 1044–1077

    Relating State-Based and Process-Based Concurrency through Linear Logic. Information and Computation 207, 10 (2009), 1044–1077. https://doi.org/10.1016/j.ic.2008.11.006 Silvia Crafa, Michele Bugliesi, and Giuseppe Castagna

    work page doi:10.1016/j.ic.2008.11.006 2009

  15. [15]

    Electronic Notes in Theoretical Computer Science 66, 3 (2002), 76–97

    Information Flow Security for Boxed Ambients. Electronic Notes in Theoretical Computer Science 66, 3 (2002), 76–97. https://doi.org/10.1016/S1571-0661(04)80417-1 Silvia Crafa and Sabina Rossi

    work page doi:10.1016/s1571-0661(04)80417-1 2002

  16. [16]

    In ACM Workshop on Formal Methods in Security Engineering (FMSE)

    P-Congruences as Non-Interference for the pi-calculus. In ACM Workshop on Formal Methods in Security Engineering (FMSE) . ACM, 13–22. https://doi.org/10.1145/1180337.1180339 Logical Relations for Session-Typed Concurrency 27 Silvia Crafa and Sabina Rossi

    work page doi:10.1145/1180337.1180339

  17. [17]

    Information and Computation 205, 8 (2007), 1235 –

    Controlling information release in the 𝜋-calculus. Information and Computation 205, 8 (2007), 1235 –

    work page 2007

  18. [18]

    https://doi.org/10.1016/j.ic.2007.01.001 Karl Crary, Robert Harper, and Sidd Puri

    work page doi:10.1016/j.ic.2007.01.001 2007

  19. [19]

    In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

    What is a Recursive Module?. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) . ACM, 50–63. https://doi.org/10.1145/301618.301641 Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia

    work page doi:10.1145/301618.301641

  20. [20]

    In: 2021 36th Annual ACM/IEEE Sym- posium on Logic in Computer Science (LICS)

    Session Logical Relations for Noninterference. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . IEEE Computer Society, 1–14. https://doi.org/10.1109/ LICS52264.2021.9470654 Henry DeYoung, Frank Pfenning, and Klaas Pruiksma

    work page arXiv 2021

  21. [21]

    https://doi.org/10.4230/LIPIcs.FSCD.2020.29 Derek Dreyer, Amal Ahmed, and Lars Birkedal

    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 29:1–29:22. https://doi.org/10.4230/LIPIcs.FSCD.2020.29 Derek Dreyer, Amal Ahmed, and Lars Birkedal

    work page doi:10.4230/lipics.fscd.2020.29 2020

  22. [22]

    In24th Annual IEEE Symposium on Logic in Computer Science (LICS)

    Logical Step-Indexed Logical Relations. In24th Annual IEEE Symposium on Logic in Computer Science (LICS) . IEEE Computer Society, 71–80. https://doi.org/10.1109/LICS.2009.34 Derek Dreyer, Georg Neis, and Lars Birkedal

    work page doi:10.1109/lics.2009.34 2009

  23. [23]

    In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP)

    The Impact of Higher-Order State and Control Effects on Local Relational Reasoning. In 15th ACM SIGPLAN International Conference on Functional Programming (ICFP) . ACM, 143–156. https://doi.org/10.1145/1863543.1863566 Derek Dreyer, Georg Neis, and Lars Birkedal

    work page doi:10.1145/1863543.1863566

  24. [24]

    Journal of Functional Programming 22, 4-5 (2012), 477–528

    The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming 22, 4-5 (2012), 477–528. https://doi.org/10.1017/S095679681200024X Simon J. Gay and Malcolm Hole

    work page doi:10.1017/s095679681200024x 2012

  25. [25]

    Subtyping for session types in the pi calcu lus

    Subtyping for Session Types in the Pi Calculus. Acta Informatica 42, 2-3 (2005), 191–225. https://doi.org/10.1007/s00236-005-0177-z Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal

    work page doi:10.1007/s00236-005-0177-z 2005

  26. [26]

    Proceedings of the ACM on Programming Languages 5, POPL (2021), 1–29

    Mechanized Logical Relations for Termination-Insensitive Noninterference. Proceedings of the ACM on Programming Languages 5, POPL (2021), 1–29. https://doi.org/10.1145/3434291 Daniel Heidin and Andrei Sabelfeld

    work page doi:10.1145/3434291 2021

  27. [27]

    The Journal of Logic and Algebraic Programming 63, 1 (2005), 3 –

    The security pi-calculus and non-interference. The Journal of Logic and Algebraic Programming 63, 1 (2005), 3 –

    work page 2005

  28. [28]

    Matthew Hennessy and James Riely

    https://doi.org/10.1016/j.jlap.2004.01.003 Special issue on The pi-calculus. Matthew Hennessy and James Riely

    work page doi:10.1016/j.jlap.2004.01.003 2004

  29. [29]

    Resource Access in the Asynchronous Pi-Calculus

    Information Flow vs. Resource Access in the Asynchronous Pi-Calculus. ACM Trans. Program. Lang. Syst. 24, 5 (Sept. 2002), 566–591. https://doi.org/10.1145/570886.570890 C. A. R. Hoare

    work page doi:10.1145/570886.570890 2002

  30. [30]

    In CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (Lecture Notes in Computer Science, Vol

    Springer, 509–523. https://doi.org/10.1007/3-540-57208-2_35 Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo

    work page doi:10.1007/3-540-57208-2_35

  31. [31]

    Language primitives and type discipline for structured communication-based programming

    Language Primitives and Type Discipline for Structured Communication-Based Programming. In 7th European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 1381). Springer, 122–138. https://doi.org/10.1007/BFb0053567 Kohei Honda, Vasco Thudichum Vasconcelos, and Nobuko Yoshida

    work page doi:10.1007/bfb0053567

  32. [32]

    https://doi.org/10.1007/3-540-46425-5_12 Kohei Honda and Nobuko Yoshida

    Springer, 180–199. https://doi.org/10.1007/3-540-46425-5_12 Kohei Honda and Nobuko Yoshida

    work page doi:10.1007/3-540-46425-5_12

  33. [33]

    In 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    A Uniform Type Structure for Secure Information Flow. In 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 81–92. https://doi.org/10.1145/503272.503281 Kohei Honda and Nobuko Yoshida

    work page doi:10.1145/503272.503281

  34. [34]

    ACM Transactions on Programming Languages and Systems (TOPLAS) 29, 6 (2007),

    A uniform type structure for secure information flow. ACM Transactions on Programming Languages and Systems (TOPLAS) 29, 6 (2007),

    work page 2007

  35. [35]

    https://doi.org/10.1145/1286821.1286822 Chung-Kil Hur and Derek Dreyer

    work page doi:10.1145/1286821.1286822

  36. [36]

    In38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    A Kripke Logical Relation between ML and Assembly. In38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 133–146. https://doi.org/10.1145/1926385.1926402 Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis

    work page doi:10.1145/1926385.1926402

  37. [37]

    In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    The Marriage of Bisimulations and Kripke Logical Relations. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 59–72. https://doi.org/10.1145/2103656.2103666 Atsushi Igarashi and Naoki Kobayashi

    work page doi:10.1145/2103656.2103666

  38. [38]

    In 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    A Generic Type System for the Pi-calculus. In 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . 128–141. https://doi.org/10.1145/360204.360215 Atsushi Igarashi and Naoki Kobayashi

    work page doi:10.1145/360204.360215

  39. [39]

    Theoretical Computer Science 311, 1-3 (2004), 121–163

    A Generic Type System for the Pi-calculus. Theoretical Computer Science 311, 1-3 (2004), 121–163. https://doi.org/10.1016/S0304-3975(03)00325-6 Guilhem Jaber and Davide Sangiorgi

    work page doi:10.1016/s0304-3975(03)00325-6 2004

  40. [40]

    https://doi.org/10.4230/LIPIcs.CSL.2022.25 Naoki Kobayashi

    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 25:1–25:18. https://doi.org/10.4230/LIPIcs.CSL.2022.25 Naoki Kobayashi

    work page doi:10.4230/lipics.csl.2022.25 2022

  41. [41]

    In 12th Annual IEEE Symposium on Logic in Computer Science (LICS)

    A Partially Deadlock-Free Typed Process Calculus. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 128–139. https://doi.org/10.1109/LICS.1997.614941 Naoki Kobayashi

    work page doi:10.1109/lics.1997.614941 1997

  42. [42]

    Information and Computation , author =

    A Type System for Lock-Free Processes. Information and Computation 177, 2 (2002), 122–159. https://doi.org/10.1006/inco.2002.3171 28 Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao Naoki Kobayashi

    work page doi:10.1006/inco.2002.3171 2002

  43. [43]

    doi:10.1007/s00236-005-0179-x

    Type-Based Information Flow Analysis for the Pi-Calculus. Acta Informatica 42, 4-5 (2005), 291–347. https://doi.org/10.1007/s00236-005-0179-x Naoki Kobayashi

    work page doi:10.1007/s00236-005-0179-x 2005

  44. [44]

    https://doi.org/10.1007/11817949_16 Vasileios Koutavas and Mitchell Wand

    233–247. https://doi.org/10.1007/11817949_16 Vasileios Koutavas and Mitchell Wand

    work page doi:10.1007/11817949_16

  45. [45]

    In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    Small Bisimulations for Reasoning about Higher-Order Imperative Programs. In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 141–152. https: //doi.org/10.1145/1111037.1111050 Sam Lindley and J. Garrett Morris

    work page doi:10.1145/1111037.1111050

  46. [46]

    In: Meersman, R., Panetto, H., Dillon, T., Mis- sikoff, M., Liu, L., Pastor, O., Cuzzocrea, A., Sellis, T

    Springer, 560–584. https://doi.org/10.1007/978-3-662- 46669-8_23 Sam Lindley and J. Garrett Morris

    work page doi:10.1007/978-3-662-

  47. [47]

    In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP)

    Talking Bananas: Structural Recursion for Session Types. In 21st ACM SIGPLAN International Conference on Functional Programming (ICFP) . ACM, 434–447. https://doi.org/10.1145/2951913.2951921 Paul-André Melliès and Jerome Vouillon

    work page doi:10.1145/2951913.2951921

  48. [48]

    In 20th Annual IEEE Symposium on Logic in Computer Science (LICS)

    Recursive Polymorphic Types and Parametricity in an Operational Framework. In 20th Annual IEEE Symposium on Logic in Computer Science (LICS) . IEEE Computer Society, 82–91. https://doi.org/10. 1109/LICS.2005.42 Robin Milner

    work page 2005

  49. [49]

    Lecture Notes in Computer Science92, Springer, doi:10.1007/3-540-10235-3

    Springer. https: //doi.org/10.1007/3-540-10235-3 Robin Milner

    work page doi:10.1007/3-540-10235-3

  50. [50]

    Journal of Functional Programming 21, 4-5 (2011), 497–562

    Non-parametric parametricity. Journal of Functional Programming 21, 4-5 (2011), 497–562. https://doi.org/10.1017/S0956796811000165 Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho

    work page doi:10.1017/s0956796811000165 2011

  51. [51]

    https://doi.org/10.1007/978-3-642-28869-2_27 Jorge A

    Springer, 539–558. https://doi.org/10.1007/978-3-642-28869-2_27 Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho

    work page doi:10.1007/978-3-642-28869-2_27

  52. [52]

    Information and Computation 239 (2014), 254–302

    Linear Logical Relations and Observational Equivalences for Session-Based Concurrency. Information and Computation 239 (2014), 254–302. https://doi.org/10.1016/ j.ic.2014.08.001 Andrew M. Pitts

    work page 2014

  53. [53]

    Mathematical Structures in Computer Science 10, 3 (2000), 321–359

    Parametric Polymorphism and Operational Equivalence. Mathematical Structures in Computer Science 10, 3 (2000), 321–359. http://journals.cambridge.org/action/displayAbstract?aid=44651 Andrew M. Pitts and Ian Stark

    work page 2000

  54. [54]

    Higher Order Operational Techniques in Semantics (HOOTS) (1998), 227–273

    Operational Reasoning for Functions with Local State. Higher Order Operational Techniques in Semantics (HOOTS) (1998), 227–273. F. Pottier

    work page 1998

  55. [55]

    In Proceedings 15th IEEE Computer Security Foundations Workshop (CSFW-15)

    A simple view of type-secure information flow in the 𝜋-calculus. In Proceedings 15th IEEE Computer Security Foundations Workshop (CSFW-15). 320–330. https://doi.org/10.1109/CSFW.2002.1021826 Andrei Sabelfeld and Andrew C. Myers

    work page doi:10.1109/csfw.2002.1021826 2002

  56. [56]

    IEEE Journal of Selected Areas in Communications 21, 1 (2003), 5–19

    Language-Based Information-Flow Security. IEEE Journal of Selected Areas in Communications 21, 1 (2003), 5–19. https://doi.org/10.1109/JSAC.2002.806121 Davide Sangiorgi

    work page doi:10.1109/jsac.2002.806121 2003

  57. [57]

    In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS)

    Environmental Bisimulations for Higher-Order Languages. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS) . IEEE Computer Society, 293–302. https://doi.org/10. 1109/LICS.2007.17 Davide Sangiorgi and David Walker

    work page 2007

  58. [58]

    In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    Secure Information Flow in a Multi-Threaded Imperative Language. In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 355–364. https://doi.org/10. 1145/268946.268975 Deian Stefan, Alejandro Russo, Pablo Buiras, Amit Levy, John C. Mitchell, and David Mazières

    work page arXiv

  59. [59]

    In ACM SIGPLAN International Conference on Functional Programming (ICFP)

    Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems. In ACM SIGPLAN International Conference on Functional Programming (ICFP) . ACM, 201–214. https://doi.org/10.1145/2364527.2364557 Kristian Støvring and Søren B. Lassen

    work page doi:10.1145/2364527.2364557

  60. [60]

    In 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)

    A Complete, Co-inductive Syntactic Theory of Sequential Control and State. In 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) . ACM, 161–172. https://doi.org/10.1145/1190216.1190244 Eijiro Sumii and Benjamin C. Pierce

    work page doi:10.1145/1190216.1190244

  61. [61]

    Journal of the ACM 54, 5 (2007),

    A bisimulation for type abstraction and recursion. Journal of the ACM 54, 5 (2007),

    work page 2007

  62. [62]

    https://doi.org/10.1145/1284320.1284325 Jacob Thamsborg and Lars Birkedal

    work page doi:10.1145/1284320.1284325

  63. [63]

    In 16th ACM SIGPLAN International Conference on Functional Programming (ICFP)

    A Kripke Logical Relation for Effect-based Program Transformations. In 16th ACM SIGPLAN International Conference on Functional Programming (ICFP) . ACM, 445–456. https://doi.org/10.1145/ 2034773.2034831 Logical Relations for Session-Typed Concurrency 29 Bernardo Toninho

    work page arXiv

  64. [64]

    https://doi.org/10.1007/978-3-642-37036-6_20 Dennis M

    Springer, 350–369. https://doi.org/10.1007/978-3-642-37036-6_20 Dennis M. Volpano, Cynthia E. Irvine, and Geoffrey Smith

    work page doi:10.1007/978-3-642-37036-6_20

  65. [65]

    Journal of Computer Security 4, 2/3 (1996), 167–188

    A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4, 2/3 (1996), 167–188. https://doi.org/10.3233/JCS-1996-42-304 Philip Wadler

    work page doi:10.3233/jcs-1996-42-304 1996

  66. [66]

    Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming , pages =

    Propositions as Sessions. In ACM SIGPLAN International Conference on Functional Programming (ICFP) . ACM, 273–286. https://doi.org/10.1145/2364527.2364568 S. Zdancewic and A. C. Myers

    work page doi:10.1145/2364527.2364568

  67. [67]

    In 16th IEEE Computer Security Foundations Workshop (CSFW)

    Observational determinism for concurrent program security. In 16th IEEE Computer Security Foundations Workshop (CSFW). 29–43. https://doi.org/10.1109/CSFW.2003.1212703

    work page doi:10.1109/csfw.2003.1212703 2003