Typing Composite Subjects

Daniele Gorla; Luca Aceto; Stian Lybech

REVIEW 2 major objections 5 minor 38 references

Typing Composite Subjects

T0 review · 2 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read Tree-shaped types for composite channel names exactly match object-oriented interface types.

desk verdict The tree-shaped type system for eπ is solid, but the WC correspondence theorem is broken as printed: the interface translation and the [T-VEC] rules don't line up. read the letter →

arxiv 2411.13732 v1 pith:7X4BKNDZ submitted 2024-11-20 cs.PL

Luca Aceto , Daniele Gorla , Stian Lybech This is my paper · ORCID

classification cs.PL

keywords polyadicsynchronisationcompositesubjectseπ-calculustree-shapedtypestypecorrespondenceobject-orientedlanguagessubjectreductionsafety

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 proposes a type system for the eπ-calculus, a variant of the π-calculus in which channel names, called subjects, can be vectors of names that are composed at runtime. The central claim is that composite subjects can be typed by giving each individual name a tree-shaped type that records both whether the name can be used as a channel and which names it may be composed with. The system is shown to satisfy subject reduction and a safety property, and an encoding of a minimal class-based language, WC, into eπ establishes an exact correspondence: a WC program is well-typed if and only if its encoding is well-typed under the tree types. If correct, this means tree-shaped types are the process-calculus counterpart of interfaces in object-oriented languages.

What carries the argument

The central object is the tree-shaped type (C, Δ), consisting of a channel capability C (either ch(~B) or nil) and a composition environment Δ mapping type names to further tree nodes. A name x is assigned a base type name I, whose entry in Γ is such a pair; typing a subject vector x1·...·xn proceeds by starting at x1's entry, extracting the composition environment to look up the next name, and finally extracting the channel capability at the last step. This structure is what makes runtime composition typeable without placing channel names inside types. The encoding of WC uses the reference-cell technique, where a local variable is represented as an asynchronous output on a private channel, a field as an output on the composite name A·p, and a method as an input-guarded replication on A·f; the exact type correspondence then follows from a chain of lemmas showing well-typedness of values, expressions, statements, and environments is preserved in both directions.

What would settle it

Exhibit an operator op with declared signature $int, int \to int$ whose evaluation on two integers yields a boolean; then the well-typed process $(\nu z : I_{bool})(z<op(1,2)> \mid z(y).\mathbf{0})$ would reduce to a state where the value received on $z$ has type $bool$ rather than $int$, violating Lemma 4 and breaking subject reduction.

Watch

Extended reading notes

Core claim

The paper's central discovery is that the two capabilities of a name in eπ — acting as a channel and participating in compositions — are orthogonal and can be organised into a tree. Each node of the tree is a type name I paired with a capability type (C, Δ), where C is either ch(~B) or nil and Δ is a type environment giving the types of names that may follow the current prefix. Because types are named rather than containing names directly, recursive types such as x<x> are expressible without explicit recursive type constructors, and α-conversion does not cause problems. The main theorem states that the eπ type system exactly corresponds to the 'expectable' type system for WC via the encoding, so a program is well-typed in WC precisely when its image is well-typed in eπ.

Load-bearing premise

The soundness results rely on Lemma 4, which asserts that expression evaluation preserves types, but the paper does not specify the operational semantics of the operators and states the lemma without proof, so the soundness argument is only as strong as the unstated assumption that operator evaluation respects declared type signatures.

Editorial extensions

If this is right

Well-typed WC programs are mapped to well-typed eπ processes, and ill-typed programs to ill-typed ones, so the eπ type system is a faithful host for typed object-oriented languages.
The tree-type discipline can type known encodings such as the encoding of the distributed π-calculus Dπ without the α-conversion problems and capability collapse of earlier location-based types.
The encoding of WC uses only subject vectors of length at most two, so extending WC with nested class declarations would naturally require longer vectors and would still be covered by the same type discipline.
Subtyping can be added to the channel-capability component without difficulty, and the composition component suggests a subtyping rule in which a subtype offers at least the same compositions, with pointwise subtypes on each entry.
The exact correspondence provides a clear baseline for future work on operational correspondence and full abstraction between WC and eπ by proving the encoding's quality properties.

Reading between the lines

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

The paper leaves the encoding's operational correspondence unproven; proving divergence reflection and bisimilarity for the while-loop and method-call encodings would turn the static type correspondence into a full abstraction result, and the big-step versus small-step semantics gap is the main obstacle.
The tree-type view is not tied to eπ specifically: any name space with hierarchical structure, such as typed URI paths or nested namespaces in distributed systems, could be typed by the same tree discipline.
The open subtyping question suggests a concrete program: define subtyping on the composition environment as structural subtyping on trees, and check whether subject reduction survives; this would give a process-calculus analogue of nominal subtyping in OO languages.
Because the reference encoding uses private channels for variables, the type correspondence indicates that eπ's simple types already enforce a form of capability discipline; testing whether session types would additionally enforce encapsulation would be a natural next step.

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.

Desk Editor's Note

read the letter

Dear [name],

You should know two things about arXiv:2411.13732. The tree-shaped type system for eπ is a clean re-presentation of Carbone's nominal types, and the Safety/Subject Reduction proofs are fine. But the main new result, the exact type correspondence with the WC language (Theorem 4), is not supported by the rules as printed: the encoding of WC interface types is inconsistent with the [T-VEC] typing rules.

Here is the concrete issue. The [T-VEC] rules type a name x by first looking up Γ(x), a type name I, and then consulting the current composition environment ∆ on I: [T-VEC 2] is (fst ∘ ∆ ∘ Γ)(x). In the encoding on page 23, the interface entry for I_A is translated as I_A:(nil,(p:I_B,...)), putting the member name p directly in the second component. But that component is supposed to be a map from type names to capability types, not from names to type names. So to type A·p, [T-VEC 1] on A gives the second component (p:I_B,...), and then [T-VEC 2] on p needs Γ(p) — which is undefined. The proofs in Section 6 compute instead fst(Γ(∆(p))), i.e., they look up p in ∆, then I_B in Γ. That is the reverse composition order. Unless the rules are misprinted, the correspondence theorem does not go through.

The fix is straightforward: swap the roles of ⟦·⟧_2 and ⟦·⟧_3 for interfaces, so the second component maps I_B and I_~B to their capability types, and the top-level environment maps p and f to those type names. With that change, the proofs should work, but they need to be redone.

What the paper does well: the presentation of the tree types is genuinely more intuitive than Carbone's, and the WC encoding is a good idea. The authors are honest that the core type system is equivalent to Carbone's, so novelty rests on the encoding and correspondence. The unproven Lemma 4 (expression safety) is a minor gap, standard in this line of work; the deferred operational correspondence is a reasonable scope choice.

Bottom line: worth a serious referee, but not acceptable as is. A revision that fixes the translation and rechecks Lemma 19, 16, and Theorem 4 should be evaluated. I'd bring it to reading group for the discussion of the flaw.

Referee Report

2 major / 5 minor

Summary. This paper proposes a type system for the eπ-calculus, where subjects of synchronisation are vectors of names. The system assigns to each name a tree-shaped type built from a communication capability and a composition environment, and it types composite subjects by traversing this tree according to the order of names in the vector. The authors prove safety and subject reduction for the resulting system (Theorems 1 and 2, Corollary 1). They then introduce WC, a minimal class-based imperative language, define an encoding of WC into eπ, translate WC interface types into eπ type environments, and claim that well-typedness of a WC program is equivalent to well-typedness of its encoding (Theorem 4).

Significance. The main conceptual contribution is a clean separation between channel capabilities and composition capabilities, represented as named trees, which makes composite-subject typing syntax-directed and avoids the α-conversion problems of earlier solutions such as the Dπ typing of Hüttel. The core type system is presented carefully, and the safety and subject-reduction proofs are detailed inductive arguments. The WC correspondence is an ambitious validation of the design: if Theorem 4 were established, it would show that tree-shaped types are essentially a notational variant of conventional OO interface types under a natural encoding. The paper is also honest about what it does not prove: operational correspondence and divergence properties of the encoding are explicitly left as future work. However, as detailed below, the proof of the main correspondence theorem currently contains a load-bearing technical error in the type translation.

major comments (2)

[§4.3, Lemma 4] The type translation on p. 23 is inconsistent with the rules [T-VEC 1] and [T-VEC 2] in Figure 2, and this prevents the proof of Theorem 4 from going through as written. In Figure 2, a composite subject is typed by first applying Γ to the head name and then applying the current composition environment ∆ to the resulting type name: for example, [T-VEC 1] requires (snd ∘ ∆ ∘ Γ)(x). However, the translation of an interface, /llbracketI : ∆, Γ/rrbracket = I : (nil, (/llbracket∆/rrbracket2)), /llbracket∆/rrbracket3, ..., places the field and method names p, f themselves in the second component (/llbracket∆/rrbracket2 = p : IB, ...), while the corresponding type names IB are placed at top level via /llbracket∆/rrbracket3. Consequently, to type the field output A·p<v>, [T-VEC 1] on A yields ∆ = (p : IB, ...), and [T-VEC 2] on p requires (fst ∘ ∆ ∘ Γ)(p) = fst(∆(Γ(p))); but Γ(p) is undefined, and even if ∆(p) = IB, fst(IB) is not defined because IB is a base type, not a tuple. The derivations in Lemma 19 and in the method-call and field-assignment cases of Lemma 16 instead compute fst(Γ(∆(p))) = fst(Γ(IB)) = ch(B), which is not a use of [T-VEC 2]. The same problem affects A·f. Thus the typings of field and method accesses claimed in Section 6 do not follow from the stated rules, and Theorem 4 is not established. The construction appears repairable, for example by making the second component of an interface map the type names IB/I~B to their capability tuples and adding top-level entries p : IB and f : I~B, but the translation and the proofs of Lemmas 16–21 would need to be reworked.
[§4.3, Lemma 4] Lemma 4, called 'Safety for expressions', is asserted without proof and is stated relative to an expression semantics →e that is never defined. Since Lemma 4 is used in Lemma 5 and in the [E-OUT] and [E-COM] cases of Theorem 2, Theorems 1 and 2 and Corollary 1 are conditional on an unformalized and unproven preservation property of expression evaluation. The authors should either state the missing hypothesis explicitly, e.g. 'assume evaluation preserves typing', or give a proof of Lemma 4 under a minimal formal axiomatisation of →e; as it stands, the soundness claims of Section 4 are not fully self-contained.

minor comments (5)

[§4.2, text before Figure 2] The text says to start with rule [T-VEC 2] for a vector of length n>1, but [T-VEC 2] types a single name, while the rule for x·~x is [T-VEC 1]; this naming mix-up is confusing and should be corrected.
[Lemma 19] The displayed chain of equalities purporting to derive A·p : ch(B) by [T-VEC 1] and [T-VEC 2] omits the crucial step where Γ and ∆ are applied to p; please expand the derivation so that the order of Γ and ∆ is visible, since that is exactly where the current proof goes wrong.
[Lemma 21] The hypothesis 'Assume /llbracketΓ/rrbracket⊢ P for some process P' quantifies over an arbitrary P, but the reverse direction of the lemma is used with a specific P constructed from /llbracketS/rrbracket^Γ_r and r().0; the statement should spell out the freshness and typing conditions needed for that plugging.
[Definition 1 and §4.2] There are small typos: 'unrodered' should be 'unordered' in Definition 1, and 'preceeded' should be 'preceded' in Section 4.2; these should be corrected.
[§6.1] The paper explicitly says that operational correspondence and divergence reflection for the encoding are not proven; this is an honest limitation, but the abstract and introduction should make equally clear that Theorem 4 is only a type-correspondence result and not a full correctness statement for the encoding.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the WC type-correspondence theorem is a proved encoding result, not a fitted prediction or self-citation chain.

full rationale

The derivation chain contains no circular step. The eπ type system (Section 4, Figure 2) and the WC type system (Section 5, Figures 8–10) are defined independently, and no parameter is fitted from one to the other; Theorem 4 is an explicit encoding theorem proved by induction over the encodings of types, expressions, statements and environments (Lemmas 14–21). The translation of WC types into eπ tree types is a construction whose adequacy is exactly what the theorem asserts, not an assumption of it. The admitted equivalence with Carbone's nominal type system is a novelty statement, and the self-citations [18] and [21] are used only as background on ρ-calculi and higher-order Ψ-calculi; neither is load-bearing for the safety, subject-reduction, or correspondence proofs. The paper does flag real limitations: Lemma 4 (and the analogous WC Lemma 8) is asserted without a formal proof and depends on an unspecified operator semantics, and Section 6.1 explicitly leaves operational correspondence and divergence sensitiveness of the encoding as conjectures for future work; these are proof gaps and correctness risks, not circular reductions of the main results to their own inputs. A possible mismatch between the printed encoding of interface members and the composition order in [T-VEC] would likewise be a correctness defect, not a circularity. Score 1 reflects only the presence of harmless self-citations.

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

The central results rest on standard syntactic typing assumptions plus an abstract, unspecified expression semantics. No numerical parameters are fitted. The auxiliary type names I_B and I_ret are definitions in the encoding, not fitted constants.

assumptions (5)

domain assumption Well-formed type environments: every type name occurring in Γ has an entry in Γ.
Section 4.1 states 'We shall only consider well-formed type environments', and the rules [T-VEC 1]/[T-VEC 2] rely on Γ(I) being defined. The condition is not formalized or shown to hold for environments arising in typing derivations.
domain assumption Expression evaluation respects typing (Lemma 4).
The semantics of operators op is left unspecified (Section 3), and Lemma 4 is stated without proof. The safety and subject reduction results depend on this lemma.
domain assumption No operation yields a name as a value.
Stated in Section 3. This ensures that the type of a value is either a base type or determined by Γ for names, and prevents names from being generated by expression evaluation.
standard math Terms are well-sorted with matching arities.
Section 3 assumes well-sortedness so that substitutions in [E-IN] are arity-matched. This is a standard background assumption for polyadic calculi.
standard math Correctness of the reference/cell encoding from Hirschkoff et al. [13].
The encoding of WC variables and fields in Section 6 uses the representation of references as asynchronous outputs from [13]. The paper does not re-prove this prior result.

invented entities (3)

Type names I (atomic type names distinct from channel names) independent evidence
purpose: Named types allow compositional types without embedding channel names, avoiding α-conversion problems for restricted names.
The type system is proved sound (Theorems 1, 2) and the type correspondence (Theorem 4) holds, providing internal evidence for the adequacy of type names.
Tree-shaped types (C, ∆) with capability and composition components independent evidence
purpose: Give each name a compositional type distinguishing channel capability from composition capability, and support different behaviours in different vector positions.
Subject reduction and the exact correspondence with OO interfaces (Theorem 4) support this type structure.
Container types I_B and return type I_ret independent evidence
purpose: In the WC encoding, I_B represents a variable or field of base type B as a channel, and I_ret is a channel for return signals.
These are part of the encoding that satisfies Theorem 4, which is proved in the paper.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Typing Composite Subjects." pith.science (2026). https://pith.science/paper/7X4BKNDZ

@misc{pith2026241113732,
  author       = {Pith},
  title        = {Pith review of: Typing Composite Subjects},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7X4BKNDZ}},
  note         = {Machine review of arXiv:2411.13732}
}

read the original abstract

Many type systems have been presented in the literature for variants of the pi-calculus, but none of them are able to handle composite subjects such as those found in the language epi, which features polyadic synchronisation. The purpose of this paper is to address the question of how to type composite subjects in a general fashion. We assess the validity of our proposal by first proving the standard correctness results for a type system (i.e., subject reduction and type safety). Then, we follow the path opened by Sangiorgi in 1998 and show an encoding in epi of a minimal OO language called WC (While with \Classes) whose ``expectable'' type system exactly corresponds to the one induced by ours via the encoding. This comparison contributes to understanding the relationship between our types and conventional types for OO languages.

Figures

Figures reproduced from arXiv: 2411.13732 by the authors.

**Figure 1.** Early labelled semantics for the eπ-calculus. polyadic π-calculus [23], and polyadic subjects, as in [4]. As usual, polyadicity (i.e. polyadic objects) leads to have a bound output label both in the premise and in the conclusion of the [E-OPEN] rule. In the rule [E-COM1], the list of bound names ye in xe!(νye)ve can be empty; thus, it can act both as an ordinary communication rule and as a close rule. Finally, as us… view at source ↗

**Figure 2.** Type rules for values, subject vectors, and proces [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗

**Figure 3.** Error-predicate for processes. τ-labelled transitions: NSafeΓ(P) ∆= ¬WrongΓ (P) SafeΓ(P) ∆= ∀P ′ . (P τ−→* P ′ =⇒ NSafeΓ [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗

Figures from the paper (8 more)

**Figure 4.** Figure 4: The syntax of WC. the λ-calculus [22], and also from Pierce and Turner’s work on the PICT language [32, 37]. Also, the encoding of object-oriented (OO) languages into (variants of the) π-calculus is by now well established [19, 35, 39]; hence, it is not surprising that…

**Figure 5.** Figure 5: Semantics of WC declarations. semantics of declarations concern the initial construction of the field and method environments, envF and envM, and the state and method table envS and envT . We give the semantics in classic big-step style. Transitions are thus on the for…

**Figure 6.** Figure 6: Semantics of WC expressions. 5.2 Typed WC There are also textbook examples of type systems for While-like languages; for example the language BUMP given in [14, pp. 185-198], which also includes procedure calls. We can define a similar type system for WC as follows: De…

**Figure 10.** Figure 10: Note that we continue to use the abbreviated notat [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]

**Figure 7.** Figure 7: Semantics of WC statements. Lemma 6 (Weakening for envV ). If Γ ⊢ envV and x ∈/ dom(envV ), then Γ,x : B ⊢ envV . Lemma 7 (Strengthening for envV ). If Γ,x : B ⊢ envV and x ∈/ dom(envV ), then Γ ⊢ envV . The next lemma expresses that, if an expression e is judged to ha…

**Figure 8.** Figure 8: Type rules for WC-environment agreement. [T-VAR] Γ(x) = B Γ ⊢ x : B [T-FIELD] Γ ⊢ e : I Γ(I)(p) = B Γ ⊢ e.p : B [T-OP] Γ ⊢ ee: Be op : Be→ B Γ ⊢ op(ee) : B [T-VAL] Γ ⊢ v : B   B =    int if v ∈ Z bool if v ∈ B Γ(v) if v ∈ N   [PITH_FULL_IMAGE:figures/full_f…

**Figure 9.** Figure 9: Type rules for WC-expressions Lemma 10 (Extension of envV ). If Γ,x : B ⊢ envV and x ∈/ dom(envV ) and Γ,x : B ⊢ v : B, then Γ,x : B ⊢ (x,v),envV . We shall need almost the same lemmata for envS, except extension, since new fields cannot be declared at runtime. As env…

**Figure 10.** Figure 10: Type rules for WC-statements. • Suppose [WC-ASSV] was used. Then we know that S = x := e, and the transition is of the form envT ⊢ hx := e,envSV i → envS,envV[x 7→ v] From the premise of that rule we have that envSV ⊢ e →e v. Now, Γ ⊢ x := e must have been concluded b…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

38 extracted references · 29 canonical work pages

[2]

Logical Methods in Computer Science V olume 7, Issue 1, doi:10.2168/LMCS-7(1:11)2011

Jesper Bengtson, Magnus Johansson, Joachim Parrow & Bjö rn Victor (2011): Psi-calculi: a framework for mobile processes with nominal data and logic . Logical Methods in Computer Science V olume 7, Issue 1, doi:10.2168/LMCS-7(1:11)2011. Available at https://lmcs.episciences.org/696

work page doi:10.2168/lmcs-7(1:11)2011 2011
[3]

Marco Carbone (2005): Trust and Mobility . Ph.D. thesis, University of Aarhus. BRICS Dissertation Se ries Number DS-05-3

work page 2005
[4]

Nordic Journal of Computing 10(2), pp

Marco Carbone & Sergio Maffeis (2003): On the Expressive Power of Polyadic Synchronisation in Pi- Calculus. Nordic Journal of Computing 10(2), pp. 70–98, doi:10.1016/S1571-0661(05)80361-5

work page doi:10.1016/s1571-0661(05)80361-5 2003
[5]

In: Proc

Arthur Charguéraud (2013): Pretty-Big-Step Semantics. In: Proc. of ESOP, LNCS 7792, Springer, pp. 41–60, doi:10.1007/978-3-642-37036-6_3

work page doi:10.1007/978-3-642-37036-6_3 2013
[6]

In: Proc

Francesco Dagnino, Viviana Bono, Elena Zucca & Mariangi ola Dezani-Ciancaglini (2020): Sound- ness Conditions for Big-Step Semantics . In: Proc. of ESOP , LNCS 12075, Springer, pp. 169–196, doi:10.1007/978-3-030-44914-8_7

work page doi:10.1007/978-3-030-44914-8_7 2020
[7]

Formal Asp

Murdoch Gabbay & Andrew Pitts (2002): A New Approach to Abstract Syntax with V ariable Binding. Formal Asp. Comput. 13, pp. 341–363, doi:10.1007/s001650200016

doi:10.1007/s001650200016 2002
[8]

In: Proc

Rob van Glabbeek (2012): Musings on Encodings and Expressiveness . In: Proc. of EXPRESS/SOS , EPTCS 89, pp. 81–98, doi:10.4204/EPTCS.89.7

work page doi:10.4204/eptcs.89.7 2012
[9]

In: Proc

Rob van Glabbeek (2018): A Theory of Encodings and Expressiveness (Extended Abstrac t). In: Proc. of FoSSaCS, LNCS 10803, Springer, pp. 183–202, doi:10.1007/978-3-319-893 66-2_10

work page doi:10.1007/978-3-319-893 2018

Show all 38 references

[10]

Information and Computation 208(9), pp

Daniele Gorla (2010): T owards a uniﬁed approach to encodability and separation results for process calculi. Information and Computation 208(9), pp. 1031–1053, doi:10.1016/j.ic.2010.05.002

2010 doi
[11]

Math- ematical Structures in Computer Science 26, pp

Daniele Gorla & Uwe Nestmann (2016): Full abstraction for expressiveness: history, myths and fa cts. Math- ematical Structures in Computer Science 26, pp. 639 – 654, doi:10.1017/S0960129514000279

2016 doi
[12]

Information and Computation 173(1), pp

Matthew Hennessy & James Riely (2002): Resource Access Control in Systems of Mobile Agents. Information and Computation 173(1), pp. 82–120, doi:10.1006/inco.2001.3089

2002
[13]

Daniel Hirschkoff, Enguerrand Prebet & Davide Sangior gi (2020): On the Representation of References in the Pi-Calculus . In Igor Konnov & Laura Kovács, editors: 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria ( Virtual Co...

2020 doi
[14]

Cambridge University Press, doi:10.1017/CBO9780511840449

Hans Hüttel (2010): Transitions and Trees - An Introduction to Structural Operational Semantics. Cambridge University Press, doi:10.1017/CBO9780511840449

2010 doi
[15]

In: International Conference on Concurrency Theory , Springer, pp

Hans Hüttel (2011): Typed ψ -calculi. In: International Conference on Concurrency Theory , Springer, pp. 265–279, doi:10.1007/978-3-642-23217-6_18

2011 doi
[16]

In Martín Abadi & Alberto Lluch La- fuente, editors: Trustworthy Global Computing , Springer International Publishing, Cham, pp

Hans Hüttel (2014): Types for Resources in ψ -calculi. In Martín Abadi & Alberto Lluch La- fuente, editors: Trustworthy Global Computing , Springer International Publishing, Cham, pp. 83–102, doi:10.1007/978-3-319-05119-2_6

2014 doi
[17]

In Atsushi Igarashi, editor: Programming Languages and Systems , Springer International Publishing, Cham, pp

Hans Hüttel (2016): Binary Session Types for Psi-Calculi . In Atsushi Igarashi, editor: Programming Languages and Systems , Springer International Publishing, Cham, pp. 96–115, doi:10.1007/978-3-319-47958-3_6

2016 doi
[18]

Bendixen & Bjarke B

Hans Hüttel, Stian Lybech, Alex R. Bendixen & Bjarke B. B ojesen (2024): A Generic Type System for Higher-Order Ψ -calculi. Information and Com- putation, p. 105190, doi:https://doi.org/10.1016/j.ic.2024.105 190. Available at https://www.sciencedirect.com/science/article/pii/S...

2024 doi
[19]

Josva Kleist & Davide Sangiorgi (2002): Imperative objects as mobile processes . Sci. Comput. Program. 44(3), pp. 293–342, doi:10.1016/S0167-6423(02)00034-5

2002 doi
[20]

Xavier Leroy & Hervé Grall (2009): Coinductive big-step operational semantics . Inf. Comput. 207(2), pp. 284–304, doi:10.1016/J.IC.2007.12.004

2009 doi
[21]

Informa- tion and Computation 297, p

Stian Lybech (2024): The reﬂective higher-order calculus: Encodability, typab ility and separation. Informa- tion and Computation 297, p. 105138, doi:10.1016/j.ic.2024.105138

2024
[22]

Mathematical structures in computer science 2(2), pp

Robin Milner (1992): Functions as processes . Mathematical structures in computer science 2(2), pp. 119– 141

1992
[23]

In: Logic and Algebra of Speciﬁcation , Springer Berlin Heidelberg, pp

Robin Milner (1993): The Polyadic π -Calculus: a Tutorial. In: Logic and Algebra of Speciﬁcation , Springer Berlin Heidelberg, pp. 203–246, doi:10.1007/978-3-642-5 8041-3_6

1993 doi
[24]

Information and Computation 100(1), pp

Robin Milner, Joachim Parrow & David Walker (1992): A calculus of mobile processes, I . Information and Computation 100(1), pp. 1–40, doi:10.1016/0890-5401(92)90008-4

1992 doi
[25]

In: ECOOP’99 Workshops, LNCS 1743, Springer, pp

Uwe Nestmann & António Ravara (1999): Semantics of Objects as Processes (SOAP) . In: ECOOP’99 Workshops, LNCS 1743, Springer, pp. 314–325

1999
[26]

Springer- V erlag London, doi:10.1007/978-1-84628-692-6

Hanne Riis Nielson & Flemming Nielson (2007): Semantics with Applications: An Appetizer . Springer- V erlag London, doi:10.1007/978-1-84628-692-6

2007 doi
[27]

In: Handbook of Process Algebra , Elsevier, pp

Joachim Parrow (2001): An introduction to the π -calculus. In: Handbook of Process Algebra , Elsevier, pp. 479–543, doi:10.1016/B978-044482830-9/50026-6

2001 doi
[28]

In: Emerging Trends in Concurrency Theory , ENTCS 209, Elsevier, pp

Joachim Parrow (2006): Expressiveness of Process Algebras . In: Emerging Trends in Concurrency Theory , ENTCS 209, Elsevier, pp. 173–186, doi:10.1016/J.ENTCS.2008.04 .011

2006 doi
[29]

Mathematical Structures in Computer Science 24(2), doi:10.1017/S0960129513000170

Joachim Parrow, Johannes Borgström, Palle Raabjerg & J ohannes Åman Pohjola (2014): Higher-order psi- calculi. Mathematical Structures in Computer Science 24(2), doi:10.1017/S0960129513000170

2014 doi
[30]

van Glabbeek (2015): Analysing and Comparing Encodability Criteria

Kirstin Peters & Rob J. van Glabbeek (2015): Analysing and Comparing Encodability Criteria . In: Proc. of EXPRESS/SOS, EPTCS 190, pp. 46–60, doi:10.4204/EPTCS.190.4

2015 doi
[31]

In: [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Comput er Science , IEEE, pp

Benjamin Pierce & Davide Sangiorgi (1993): Typing and subtyping for mobile processes . In: [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Comput er Science , IEEE, pp. 376–385, doi:10.1109/LICS.1993.287570

1993
[32]

Pierce & David N

Benjamin C. Pierce & David N. Turner (2000): Pict: a programming language based on the Pi-Calculus . In Gordon D. Plotkin, Colin Stirling & Mads Tofte, editors: Proof, Language, and Interaction, Essays in Honour of Robin Milner , The MIT Press, pp. 455–494

2000
[33]

Mosses (2014): Deriving Pretty-Big-Step Semantics from Small-Step Se- mantics

Casper Bach Poulsen & Peter D. Mosses (2014): Deriving Pretty-Big-Step Semantics from Small-Step Se- mantics. In: Proc. of ESOP , LNCS 8410, Springer, pp. 270–289, doi:10.1007/978-3-642-5483 3-8_15. L. Aceto et al. 49

2014 doi
[34]

Technical Report, 17-96, Dep

António Ravara & V asco Thudichum V asconcelos (1996): An Operational Semantics and a Type System for GNOME Based on a Typed Calculus of Objects . Technical Report, 17-96, Dep. of Mathematics, Tech. Univ. of Lisbon

1996
[35]

Davide Sangiorgi (1998): An Interpretation of Typed Objects into Typed pi-Calculus . Inf. Comput. 143(1), pp. 34–73, doi:10.1006/INCO.1998.2711

1998
[36]

Cambridge university press

Davide Sangiorgi & David Walker (2003): The pi-calculus: a Theory of Mobile Processes . Cambridge university press

2003
[37]

Turner (1996): The Polymorphic Pi-calculus: Theory and Implementation

David N. Turner (1996): The Polymorphic Pi-calculus: Theory and Implementation . Ph.D. thesis, University of Edinburgh, UK. Available at https://hdl.handle.net/1842/395

1996
[38]

In: Object-Oriented Computing III, Lecture Notes , Kindai Kagaku Sha

V asco Thudichum V asconcelos (1995): An Operational Semantics and a Type System for ABCL/1 Based o n a Calculus of Objects . In: Object-Oriented Computing III, Lecture Notes , Kindai Kagaku Sha

1995
[39]

Information and Computation 116(2), pp

David Walker (1995): Objects in the π -Calculus. Information and Computation 116(2), pp. 253–271, doi:10.1006/inco.1995.1018

1995

Pith tools

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

[1] [2]

Logical Methods in Computer Science V olume 7, Issue 1, doi:10.2168/LMCS-7(1:11)2011

Jesper Bengtson, Magnus Johansson, Joachim Parrow & Bjö rn Victor (2011): Psi-calculi: a framework for mobile processes with nominal data and logic . Logical Methods in Computer Science V olume 7, Issue 1, doi:10.2168/LMCS-7(1:11)2011. Available at https://lmcs.episciences.org/696

work page doi:10.2168/lmcs-7(1:11)2011 2011

[2] [3]

Marco Carbone (2005): Trust and Mobility . Ph.D. thesis, University of Aarhus. BRICS Dissertation Se ries Number DS-05-3

work page 2005

[3] [4]

Nordic Journal of Computing 10(2), pp

Marco Carbone & Sergio Maffeis (2003): On the Expressive Power of Polyadic Synchronisation in Pi- Calculus. Nordic Journal of Computing 10(2), pp. 70–98, doi:10.1016/S1571-0661(05)80361-5

work page doi:10.1016/s1571-0661(05)80361-5 2003

[4] [5]

In: Proc

Arthur Charguéraud (2013): Pretty-Big-Step Semantics. In: Proc. of ESOP, LNCS 7792, Springer, pp. 41–60, doi:10.1007/978-3-642-37036-6_3

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

[5] [6]

In: Proc

Francesco Dagnino, Viviana Bono, Elena Zucca & Mariangi ola Dezani-Ciancaglini (2020): Sound- ness Conditions for Big-Step Semantics . In: Proc. of ESOP , LNCS 12075, Springer, pp. 169–196, doi:10.1007/978-3-030-44914-8_7

work page doi:10.1007/978-3-030-44914-8_7 2020

[6] [7]

Formal Asp

Murdoch Gabbay & Andrew Pitts (2002): A New Approach to Abstract Syntax with V ariable Binding. Formal Asp. Comput. 13, pp. 341–363, doi:10.1007/s001650200016

doi:10.1007/s001650200016 2002

[7] [8]

In: Proc

Rob van Glabbeek (2012): Musings on Encodings and Expressiveness . In: Proc. of EXPRESS/SOS , EPTCS 89, pp. 81–98, doi:10.4204/EPTCS.89.7

work page doi:10.4204/eptcs.89.7 2012

[8] [9]

In: Proc

Rob van Glabbeek (2018): A Theory of Encodings and Expressiveness (Extended Abstrac t). In: Proc. of FoSSaCS, LNCS 10803, Springer, pp. 183–202, doi:10.1007/978-3-319-893 66-2_10

work page doi:10.1007/978-3-319-893 2018