Pith. sign in

REVIEW 3 major objections 3 minor 40 references

A Language-Agnostic Logical Relation for Message-Passing Protocols

T0 review · 3 major / 3 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper constructs a language-agnostic logical relation, defined over labelled transition systems, that certifies protocol compliance of heterogeneous message-passing systems—covering typed code, untyped code, and physical devices—and…

desk verdict Useful language-agnostic logical relation, but the printed cut rule swaps M1/M2 and omits substitution, so the FTLR and adequacy claims are not supported as written. read the letter →

arxiv 2506.10026 v1 pith:QZZBVRBE submitted 2025-06-10 cs.PL

Tesla Zhang , Sonya Simkin , Rui Li , Yue Yao , Stephanie Balzer This is my paper
classification cs.PL MSC 68Q6003B7068Q85
keywords logicalrelationsmessage-passingprotocolsverificationtypesystemsessiontypesintuitionisticlinearlogiclabelledtransitionsystemsCoqmechanization
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper tries to establish a single verification criterion for protocol compliance that works across heterogeneous message-passing systems: programs written in different languages, untyped code, and physical devices like sensors. It defines a logical relation, entirely in terms of labelled transition systems, whose inhabitants are exactly configurations that behave according to a specified protocol type. Because the definition never mentions syntax, any object that can be given an LTS can be checked, and the paper proves the relation is principled enough that every well-typed term in a session-type calculus inhabits its type. This matters because today's distributed and IoT systems cannot assume a common implementation language or type system, so existing type-based verification does not apply. The entire development is mechanized in the Coq theorem prover, making the proofs machine-checked.

What carries the argument

The load-bearing object is the language-agnostic logical relation defined in Fig. 3, given by two mutually recursive interpretations: $E\llbracket A\rrbracket$ (term interpretation: a configuration that reaches a value after silent internal steps) and $V\llbracket A\rrbracket$ (value interpretation: a configuration ready to perform the external communication prescribed by $A$). Its supporting infrastructure is the process language structure (Definition 6), which packages a set of nameless objects and an LTS transition relation, together with the runtime system of Definition 7 that composes configurations by multiset union and complementary synchronization. The relation is what carries the argument: inhabiting $E\llbracket A\rrbracket$ means complying with protocol $A$, and the fundamental theorem (Theorem 22) transfers type-system correctness into this semantic compliance via complementary configurations. The mechanization uses finite maps and multisets, with configurations represented as multisets of atomic processes.

What would settle it

Build a configuration that the mechanized relation accepts at type $A$, compose it with a complementary configuration of the dual protocol, and check whether the composite can perform an external action that no well-typed session of type $A$ could ever perform; if such a configuration exists, the relation is too permissive and does not actually capture protocol compliance.

Watch

Extended reading notes

Core claim

The paper's central claim is that protocol compliance of a heterogeneous message-passing configuration is captured by the mutually recursive logical relation $E\llbracket A\rrbracket$ and $V\llbracket A\rrbracket$ of Fig. 3: a nameless configuration is in the term interpretation $E\llbracket A\rrbracket$ if it can silently step to a configuration in the value interpretation $V\llbracket A\rrbracket$, and $V\llbracket A\rrbracket$ specifies, by structural induction on the protocol type $A$, the exact send/receive behaviour expected at that type, including sending a channel, receiving a channel, branching on selectors $\pi_1/\pi_2$, and sending the closing signal at type $1$. The relation is defined purely over labelled transition systems, so arbitrary objects—typed or untyped, software or hardware—can be inhabitants as long as they are representable as nameless processes with an LTS. The paper demonstrates this with Theorem 12, showing a bit-flipping automaton inhabits $E\llbracket (1 \oplus 1) \mathbin{\&} (1 \oplus 1) \rrbracket$ (per-instance verification), and Theorem 22, the fundamental theorem, showing every well-typed process term inhabits its type when placed with complementary configurations (once-and-for-all verification), from which Corollary 23 derives adequacy: a closed process of type $1$ eventually sends its closing signal and terminates. All of these results are mechanized in Coq.

Load-bearing premise

The whole approach assumes that every component, including a physical sensor or code written in any language, can be described by a list of possible communication steps using only a fixed set of message kinds—sending or receiving a choice label, a channel name, or a closing signal—and that components interact only by matching a send with a receive.

Editorial extensions

If this is right

  • A specific hardware device can be certified against a protocol specification once, by showing its LTS inhabits $E\llbracket A\rrbracket$, with no need for source code or a type system.
  • For any type system whose well-typed terms can be embedded in this framework, the fundamental theorem makes per-program verification automatic: typechecking suffices, and if typechecking is decidable, verification is fully automatic.
  • Different components written in different languages can be composed safely, since compliance is defined on observable transitions rather than syntax.
  • The framework supports higher-order channels, where a channel name is passed as message content, so dynamically established communication links can be certified.
  • The Coq mechanization means future extensions, such as adding new languages or new protocol types, only require extending the language table and reproving countability rather than redoing the whole framework.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • One testable extension is to take a real device's datasheet, translate its communication spec into an LTS over the paper's action alphabet, and check inhabitance of the promised protocol type; a failure would indicate a spec mismatch.
  • The fixed action alphabet means the framework in its present form cannot certify protocols with payloads beyond booleans, channels, and the closing signal, such as messages carrying numbers or strings; extending the alphabet is a natural next step.
  • The adequacy corollary is a termination guarantee only for closed processes of type $1$, and a similar guarantee for open or larger-typed processes is not derived in the paper.
  • Because the logical relation is unary, it certifies compliance but does not by itself establish relational properties such as noninterference or program equivalence; the paper lists binary logical relations as future work.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

Summary. The paper defines a language-agnostic logical relation for protocol compliance in message-passing systems. Components are modeled as nameless objects with a labelled-transition semantics over a fixed action alphabet; protocols are specified by linear-logic-style behavioral types (1, ⊗, ⊸, &, ⊕); and the logical relation is given as mutually recursive term/value interpretations E⟦A⟧ and V⟦A⟧ over configuration families. The paper presents two verification modes: per-instance certification of a bit-flipping automaton (Theorem 12) and once-and-for-all certification for well-typed terms of a session-type process language (Theorem 22, FTLR, and Corollary 23, adequacy). It claims that the logical relation and both scenarios are mechanized in Coq with the stdpp library.

Significance. If the technical issues identified below are repaired, this is a valuable contribution. The logical relation is defined entirely over LTS behavior rather than syntax, so untyped and foreign objects are potentially in scope; the relation has no fitted parameters; Theorem 12 is a concrete inhabitance proof; and the FTLR/adequacy result would reduce protocol certification to typechecking. The paper is transparent about substitution-related design choices in §5 and gives appropriate credit to related mechanization work. The claimed Coq mechanization is a strength in principle, although it cannot currently be checked from the submission.

major comments (3)
  1. [§3.2.3, Fig. 8 (Cut/let rule)] The stepping rule (let x:A←M1;M2,a) ϵ↦→Obj proc[b'](M2)⊎proc[a](M1) is inconsistent with the typing rule Cut in Fig. 6. In Cut, M1 provides A and M2 provides B using x, so after reduction M1 should reside on the fresh channel (say b') and M2, with x instantiated to b', should reside on the outer channel a. As printed, M2 is placed on b' without the substitution of b' for x, and M1 is placed on a. For the closed term let x:1←send(); recvx();send(), the rule steps to proc[b'](recvx();send())⊎proc[a](send()); after proc[a](send()) fires a!(), the residual process on b' is stuck on the free variable x, so no configuration can reach the transition required by Corollary 23. The correct rule should be of the form (let x:A←M1;M2,a) ϵ↦→Obj proc[a](\widehat{b'/x}(M2))⊎proc[b'](M1), or the paper must explain how the raw terms in Fig. 8 are instantiated. Because Theorem 22 and Corollary 23 are the paper's central once-and-for-all verification results, this rule must be corrected and reconciled with the claimed Coq proofs.
  2. [§3.2.2, Definition 14 / Definition 19] Definition 14 is stated only for two finite maps with the same codomain Y and a relation R:Y×Y→Type, but it is immediately applied to a typing context Γ:Vars⇀Types and a substitution σ:Vars⇀A, which have different codomains. The same problem occurs in Definition 19, where S is valued in NCfg×A while Γ is valued in Types. As written, Lemma 16 and the statement of Theorem 22 are ill-typed. The intended generalization is to maps m1:X⇀Y1 and m2:X⇀Y2 with a heterogeneous relation R:Y1×Y2→Type; please restate Definition 14 in this form and re-verify Lemma 16 accordingly.
  3. [§4, Mechanization artifact] The paper's headline contribution is a Coq mechanization, but the submission contains no pinned artifact: only a bare GitHub URL is given, with no commit hash, Coq/stdpp version, or build instructions. The claims in Theorem 12, Theorem 22, and Corollary 23 therefore cannot be independently checked from the manuscript as submitted. Please bundle the development or provide a stable pointer and environment instructions.
minor comments (3)
  1. [§3.2.3, Fig. 8] The cut rule also should state a freshness side condition for the fresh channel b': writing 'for b'∈A' without a side condition permits b' to coincide with a channel already present in the configuration, which could create spurious communication.
  2. [§5, Discussion and Future Work] The paragraph on substitution says the authors are 'unclear about which approach is favorable' for well-typed terms; since the paper's FTLR is stated for raw terms, this remark should be clarified so that readers know exactly which substitution definition was mechanized and how Fig. 8 is meant to interact with it.
  3. [§3.2.2, after Definition 14] Lemma 13, the composition lemma for substitutions, is stated without freshness or distinctness conditions on the bound variables of M; the mechanization may handle this, but the paper should state the hypotheses needed for the induction to go through.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the logical relation is defined semantically before typing, and the FTLR is a substantive theorem rather than a definitional equivalence.

full rationale

The derivation chain is self-contained in the relevant sense. The logical relation (Fig. 3) is defined semantically over LTS configurations before the typing rules are introduced; E⟦A⟧ and V⟦A⟧ are mutually recursive definitions over the operational model of Definitions 3–7, not over the typing judgment. Theorem 12 is a direct inhabitance proof: the object-level transitions in Fig. 4 are matched against the value-interpretation clauses, so the proof proceeds by unfolding definitions rather than assuming the conclusion. Theorem 22 (FTLR) is stated as a theorem and proved by induction on the typing derivation with supporting substitution lemmas; its conclusion, applyCompl(S,σ(M))∈E⟦A⟧, is not identical to the premise S∈E⟦Γ⟧, since the premise relates variables to complementary configurations while the conclusion adds the substituted term M. Corollary 23 follows from FTLR plus the definition of the term interpretation. No fitted parameters are renamed as predictions, and no uniqueness claim is imported from the authors' prior work. The paper does cite prior work by the same group ([41], and also [2,8,9,13]) for the underlying logical-relations approach and the nameless-object idea, but the definitions and proofs are reproduced in the paper itself (Figs. 3 and 8, Lemma 13, Theorem 22), so those self-citations are contextual rather than load-bearing. Section 5 candidly flags an unresolved design choice about substitution for typed terms, and the printed Fig. 8 cut/let stepping rule appears questionable on correctness grounds, but these are correctness risks, not circularity: the FTLR is not true by construction of the logical relation.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claim rests on the LTS representability of all components and on the finite-depth session type grammar. These are explicit definitions in the paper, not fitted parameters; no numerical constants are fit to data. The Coq proof also assumes standard library infrastructure (stdpp).

assumptions (5)
  • domain assumption Every component, including physical devices, is representable as a nameless object with an LTS over the fixed action alphabet of Definition 3.
    Definition 6 and Fig. 2; the entire language-agnosticism and the logical relation's V cases are defined over this LTS representation.
  • domain assumption Protocols are generated by the finite-depth grammar A,B ::= 1 | A⊗B | A⊕B | A&B | A⊸B (no recursive types).
    Section 2.2; the logical relation and FTLR are by structural induction on this grammar, so recursive or cyclic protocols are outside scope.
  • standard math Channel names form a countably infinite set A, with fresh quantification over all channels in the value interpretation.
    Definition 2 and Fig. 3; needed for the α-renaming and for the ∀b quantifiers in V⟦A⊗B⟧ and V⟦A⊸B⟧.
  • domain assumption Process configurations compose by multiset union, and communication requires complementary actions on the same channel (Step-Comm).
    Fig. 2; the frame and communication rules define how heterogeneous objects form a system.
  • standard math The Coq development relies on Coq's logic and on stdpp's gmap and gmultiset structures.
    Section 4; these libraries supply the finite maps and multisets used for contexts and configurations.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Language-Agnostic Logical Relation for Message-Passing Protocols." pith.science (2026). https://pith.science/paper/QZZBVRBE

@misc{pith2026250610026,
  author       = {Pith},
  title        = {Pith review of: A Language-Agnostic Logical Relation for Message-Passing Protocols},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QZZBVRBE}},
  note         = {Machine review of arXiv:2506.10026}
}
read the original abstract

Today's computing landscape has been gradually shifting to applications targeting distributed and *heterogeneous* systems, such as cloud computing and Internet of Things (IoT) applications. These applications are predominantly *concurrent*, employ *message-passing*, and interface with *foreign objects*, ranging from externally implemented code to actual physical devices such as sensors. Verifying that the resulting systems adhere to the intended protocol of interaction is challenging -- the usual assumption of a common implementation language, let alone a type system, no longer applies, ruling out any verification method based on them. This paper develops a framework for certifying *protocol compliance* of heterogeneous message-passing systems. It contributes the first mechanization of a *language-agnostic logical relation*, asserting that its inhabitants comply with the protocol specified. This definition relies entirely on a labelled transition-based semantics, accommodating arbitrary inhabitants, typed and untyped alike, including foreign objects. As a case study, the paper considers two scenarios: (1) *per-instance verification* of a specific application or hardware device, and (2) *once-and-for-all verification* of well-typed applications for a given type system. The logical relation and both scenarios are mechanized in the Coq theorem prover.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

40 extracted references · 20 canonical work pages

  1. [1]

    Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T

    Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre - Malo Deni \' e lou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming...

    doi:10.1561/2500000031 2016

  2. [2]

    Logical Relations for Session-Typed Concurrency

    Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency. CoRR , abs/2309.00192, 2023. URL: https://doi.org/10.48550/arXiv.2309.00192, https://arxiv.org/abs/2309.00192 arXiv:2309.00192 , https://doi.org/10.48550/ARXIV.2309.00192 doi:10.48550/ARXIV.2309.00192

    work page Pith review arXiv doi:10.48550/arxiv.2309.00192 2023

  3. [3]

    Biorthogonality, step-indexing and compiler correctness

    Nick Benton and Chung - Kil Hur. Biorthogonality, step-indexing and compiler correctness. In 14th ACM SIGPLAN International Conference on Functional Programming ( ICFP ) , pages 97--108. ACM , 2009. https://doi.org/10.1145/1596550.1596567 doi:10.1145/1596550.1596567

    arXiv 2009

  4. [5]

    Session types as intuitionistic linear propositions

    Lu \' s Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In 21th International Conference onf Concurrency Theory ( CONCUR ) , volume 6269 of Lecture Notes in Computer Science , pages 222--236. Springer, 2010. https://doi.org/10.1007/978-3-642-15375-4\_16 doi:10.1007/978-3-642-15375-4\_16

    doi:10.1007/978-3-642-15375-4 2010

  5. [6]

    A certified type-preserving compiler from lambda calculus to assembly language

    Adam Chlipala. A certified type-preserving compiler from lambda calculus to assembly language. In 28th ACM SIGPLAN Conference on Programming Language Design and Implementation ( PLDI ) , pages 54--65. ACM , 2007. https://doi.org/10.1145/1250734.1250742 doi:10.1145/1250734.1250742

    arXiv 2007

  6. [7]

    Constable, Stuart F

    Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Proof Development System . Prentice Hall, 1986. URL: http://dl.acm.org/citation.cfm?id=10510

    work page 1986

  7. [8]

    Session logical relations for noninterference

    Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science ( LICS ) , pages 1--14. IEEE Computer Society, 2021. https://doi.org/10.1109/LICS52264.2021.9470654 doi:10.1109/LICS52264.2021.9470654

    arXiv 2021

  8. [9]

    Regrading policies for flexible information flow control in session-typed concurrency

    Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading policies for flexible information flow control in session-typed concurrency. In 38th European Conference on Object-Oriented Programming (ECOOP) , volume 313 of LIPIcs , pages 11:1--11:29. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ECOOP.202...

    work page doi:10.4230/lipics.ecoop.2024.11 2024

Show all 40 references
  1. [10]

    Semi-axiomatic sequent calculus

    Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-axiomatic sequent calculus. In 5th International Conference on Formal Structures for Computation and Deduction ( FSCD ) , volume 167 of LIPIcs , pages 29:1--29:22. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2...

    2020 doi

  2. [11]

    Gay and Ant \' o nio Ravara

    Simon J. Gay and Ant \' o nio Ravara. Behavioural Types: From Theory to Tools . River Publishers, 2017

    2017

  3. [12]

    Interpr\' e tation fonctionelle et \' e limination des coupures de l'arithm\' e tique d'ordre sup\' e rieur

    Jean-Yves Girard. Interpr\' e tation fonctionelle et \' e limination des coupures de l'arithm\' e tique d'ordre sup\' e rieur . PhD thesis, Universit\' e Paris VII, 1972

    1972

  4. [13]

    A semantic logical relation for termination of intuitionistic linear logic session types

    Tarakaram Gollamudi, Jules Jacobs, Yue Yao, and Stephanie Balzer. A semantic logical relation for termination of intuitionistic linear logic session types. In 11th International Workshop on Coq for Programming Languages ( CoqPL ) , 2025

    2025

  5. [14]

    Types for dyadic interaction

    Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory ( CONCUR ) , volume 715 of Lecture Notes in Computer Science , pages 509--523. Springer, 1993. https://doi.org/10.1007/3-540-57208-2\_35 doi:10.1007/3-540-57208-2\_35

    1993 doi

  6. [15]

    Language primitives and type discipline for structured communication-based programming

    Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In 7th European Symposium on Programming ( ESOP ) , volume 1381 of Lecture Notes in Computer Science , pages 122--138. Springer, 1...

    1998 doi

  7. [16]

    Multiparty asynchronous session types

    Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( POPL ) , pages 273--284. ACM , 2008. https://doi.org/10.1145/1328438.1328472 doi:10.1145/1328438.1328472

    2008

  8. [17]

    Better late than never: A fully-abstract semantics for classical processes

    Wen Kokke, Fabrizio Montesi, and Marco Peressotti. Better late than never: A fully-abstract semantics for classical processes. Proceedings of the ACM on Programming Languages , 3( POPL ):24:1--24:29, 2019. https://doi.org/10.1145/3290337 doi:10.1145/3290337

    2019 doi

  9. [18]

    Efficient, extensional, and generic finite maps in coq-std++

    Robbert Krebbers. Efficient, extensional, and generic finite maps in coq-std++. 2023. URL: https://coq-workshop.gitlab.io/2023/abstracts/coq2023_finmap-stdpp.pdf

    2023

  10. [19]

    Garrett Morris

    Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In 24th European Symposium on Programming ( ESOP ) , volume 9032 of Lecture Notes in Computer Science , pages 560--584. Springer, 2015. https://doi.org/10.1007/978-3-662-46669-8\_23 doi:10.1007/978-3-...

    2015 doi

  11. [20]

    Constructive mathematics and computer programming

    Per Martin - L \" o f. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI , volume 104 of Studies in Logic and the Foundations of Mathematics , pages 153--175. Elsevier, 1982. URL: https://www.sciencedirect.com/science/article...

    1982 doi

  12. [21]

    Intuitionistic Type Theory , volume 1 of Studies in Proof Theory

    Per Martin - L \" o f. Intuitionistic Type Theory , volume 1 of Studies in Proof Theory . Bibliopolis, 1984

    1984

  13. [22]

    A Calculus of Communicating Systems , volume 92 of Lecture Notes in Computer Science

    Robin Milner. A Calculus of Communicating Systems , volume 92 of Lecture Notes in Computer Science . Springer, 1980. https://doi.org/10.1007/3-540-10235-3 doi:10.1007/3-540-10235-3

    1980 doi

  14. [23]

    Communicating and Mobile Systems: the -calculus

    Robin Milner. Communicating and Mobile Systems: the -calculus . Cambridge University Press, 1999

    1999

  15. [24]

    Typed closure conversion

    Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( POPL ) , pages 271--283. ACM , 1996. https://doi.org/10.1145/237721.237791 doi:10.1145/237721.237791

    1996

  16. [25]

    Semantic soundness for language interoperability

    Daniel Patterson, Noble Mushtak, Andrew Wagner, and Amal Ahmed. Semantic soundness for language interoperability. In 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation ( PLDI ) , pages 609--624. ACM , 2022. https://doi.org/10.1145/3519939.3523703 doi...

    2022

  17. [26]

    P \' e rez, Lu \' s Caires, Frank Pfenning, and Bernardo Toninho

    Jorge A. P \' e rez, Lu \' s Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations for session-based concurrency. In 21st European Symposium on Programming ( ESOP ) , volume 7211 of Lecture Notes in Computer Science , pages 539--558. Springer, 2012. https://do...

    2012 doi

  18. [27]

    P \' e rez, Lu \' s Caires, Frank Pfenning, and Bernardo Toninho

    Jorge A. P \' e rez, Lu \' s Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation , 239:254--302, 2014. https://doi.org/10.1016/j.ic.2014.08.001 doi:10.1016/j.ic.2014.08.001

    2014 doi

  19. [28]

    Pitts and Ian Stark

    Andrew M. Pitts and Ian Stark. Operational reasoning for functions with local state. Higher Order Operational Techniques in Semantics (HOOTS) , pages 227--273, 1998

    1998

  20. [29]

    Gordon D. Plotkin. Lambda-definability and logical relations. Technical report, University of Edinburgh, 1973

    1973

  21. [30]

    Safe session-based concurrency with shared linear state

    Pedro Rocha and Lu \' s Caires. Safe session-based concurrency with shared linear state. In 32nd European Symposium on Programming ( ESOP ) , volume 13990 of Lecture Notes in Computer Science , pages 421--450. Springer, 2023. https://doi.org/10.1007/978-3-031-30044-8\_16 doi:1...

    2023 doi

  22. [31]

    Dimsum: A decentralized approach to multi-language semantics and verification

    Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. Dimsum: A decentralized approach to multi-language semantics and verification. Proceedings of the ACM on Programming Languages , 7( POPL ):775--805, 2023. https://d...

    2023 doi

  23. [32]

    The -calculus: a Theory of Mobile Processes

    Davide Sangiorgi and David Walker. The -calculus: a Theory of Mobile Processes . Cambridge University Press, 2001

    2001

  24. [33]

    Logical relations and the typed -calculus

    Richard Statman. Logical relations and the typed -calculus. Information and Control , 65(2/3):85--97, 1985. https://doi.org/10.1016/S0019-9958(85)80001-2 doi:10.1016/S0019-9958(85)80001-2

    1985 doi

  25. [34]

    William W. Tait. Intensional interpretations of functionals of finite type I . The Journal of Symbolic Logic , 32(2):198--212, 1967. URL: http://www.jstor.org/stable/2271658

    1967

  26. [35]

    Standard Library

    The std++ developers and contributors . Rocq-std++: An extended " Standard Library " for Rocq , 2024. URL: https://gitlab.mpi-sws.org/iris/stdpp/

    2024

  27. [36]

    A logical approach to type soundness

    Amin Timany, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. A logical approach to type soundness. Journal of the ACM (JACM) , 2024. To appear

    2024

  28. [37]

    A Logical Foundation for Session-Based Concurrent Computation

    Bernardo Toninho. A Logical Foundation for Session-Based Concurrent Computation . PhD thesis, Carnegie Mellon University and New University of Lisbon, 2015

    2015

  29. [38]

    Higher-order processes, functions, and sessions: A monadic integration

    Bernardo Toninho, Lu \' s Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: A monadic integration. In 22nd European Symposium on Programming ( ESOP ) , volume 7792 of Lecture Notes in Computer Science , pages 350--369. Springer, 2013. https://doi.org...

    2013 doi

  30. [39]

    Information flow control in cyclic process networks

    Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information flow control in cyclic process networks. In 38th European Conference on Object-Oriented Programming (ECOOP) , volume 313 of LIPIcs , pages 40:1--40:30. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Inform...

    2024 doi

  31. [40]

    Propositions as sessions

    Philip Wadler. Propositions as sessions. In ACM SIGPLAN International Conference on Functional Programming ( ICFP ) , pages 273--286. ACM , 2012. https://doi.org/10.1145/2364527.2364568 doi:10.1145/2364527.2364568

    2012

  32. [41]

    Semantic logical relations for timed message-passing protocols

    Yue Yao, Grant Iraci, Cheng-En Chuang, Stephanie Balzer, and Lukasz Ziarek. Semantic logical relations for timed message-passing protocols. Proceedings of the ACM on Programming Languages , 9( POPL ):1750--1781, 2025. https://doi.org/10.1145/3704895 doi:10.1145/3704895

    2025 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.