pith. sign in

arxiv: 2306.12935 · v4 · pith:AO6RMH4Snew · submitted 2023-06-22 · 💻 cs.PL

Special Delivery: Programming with Mailbox Types (Extended Version)

Simon Fowler , Duncan Paul Attard , Danielle Marshall , Simon J. Gay , Phil Trinder This is my paper

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

classification 💻 cs.PL
keywords mailbox typesactor languagesbehavioural typestype systemscommunication errorsquasi-linear typingbidirectional typingconcurrency
0
0 comments X

The pith

Pat is the first programming language to incorporate mailbox types for detecting actor communication errors.

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

The paper presents Pat, a higher-order functional language with sums, products and lists that adds mailbox types to model actor mailboxes as commutative regular expressions. An algorithmic type system based on quasi-linear typing and backwards bidirectional typing checks programs for protocol violations, unexpected messages, forgotten replies, self-deadlocks and ordinary data errors. The system is proved sound and complete with respect to a declarative version, and is demonstrated on a factory automation example plus benchmarks from the Savina suite. This work moves mailbox types from process calculi into a practical language setting while handling aliasing and nested evaluation contexts.

Core claim

Mailbox types, which capture mailbox contents as commutative regular expressions and are augmented with interfaces for finer-grained control, can be embedded in a full programming language Pat together with an algorithmic type checker that detects four specific classes of behavioural error in addition to data-type mistakes.

What carries the argument

Mailbox types that represent mailbox contents via commutative regular expressions, together with quasi-linear typing to manage aliasing and a co-contextual algorithmic system obtained via backwards bidirectional typing.

If this is right

  • Type checking in Pat catches protocol violations, unexpected messages, forgotten replies and self-deadlocks before execution.
  • The algorithmic type system is sound and complete with respect to the declarative system.
  • Quasi-linear typing combined with backwards bidirectional typing suffices to handle aliasing and nested contexts.
  • The language supports higher-order functions, sums, products and lists while still enforcing mailbox protocols.

Where Pith is reading between the lines

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

  • The same mailbox-type discipline could be retrofitted to existing actor runtimes such as Erlang or Akka.
  • Interfaces for finer-grained mailbox reasoning may generalise to other message-passing calculi.
  • The co-contextual approach may simplify type inference for other behavioural type systems that must cope with aliasing.

Load-bearing premise

The difficulties created by aliasing and nested evaluation contexts when moving mailbox types from a process calculus into a programming language can be solved by quasi-linear typing plus a co-contextual algorithmic checker.

What would settle it

An actor program that performs a protocol violation, sends an unexpected message, omits a required reply, or deadlocks on itself yet is accepted by the Pat type checker (or a well-behaved program that the checker rejects).

Figures

Figures reproduced from arXiv: 2306.12935 by Danielle Marshall, Duncan Paul Attard, Phil Trinder, Simon Fowler, Simon J. Gay.

Figure 1
Figure 1. Figure 1: Channel- and actor-based languages [Fowler et al. 2017] [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Send and receive uses of future Session typing was originally studied in the context of pro￾cess calculi (e.g., [Honda et al. 1998; Vasconcelos 2012]), but later work [Fowler et al. 2021; Gay and Vasconcelos 2010; Wadler 2014] introduced session types for languages based on the linear 𝜆-calculus. The more relaxed view of linearity in the mailbox calculus makes language integration far more challenging. A m… view at source ↗
Figure 3
Figure 3. Figure 3: Use-after-free via aliasing situation, use-after-free errors are not an issue with a fully linear type system, since we cannot use a resource after it has been consumed. We could require that a name cannot be used after it has been guarded upon by insisting that the subject and body of a guard expression are typable under disjoint type environments. Indeed, such an approach correctly rules out the error in… view at source ↗
Figure 4
Figure 4. Figure 4: The syntax of Pat, a core language with mailbox types [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Pat declarative term typing m. The mailbox only needs to be second-class, but subtyping means that we can also send to a first-class name. All payloads −→𝑉 must be subtypes of the types defined by the signature for message m, and payloads must be typable under separate environments to avoid aliasing when receiving a message. Unlike in session-typed functional programming languages, sending is a side-effect… view at source ↗
Figure 6
Figure 6. Figure 6: Pat operational semantics Here f is used to send a Put and then a Get with s of type !Reply◦ as payload. As the two sends to the f message are sequentially composed, the type of f at the root of the subderivation is !(Put ⊙ Get) • . Since s is used at type ?(Reply ⊙ 1) • in D1, the send and receive patterns balance out to the empty mailbox type ?1 • . Finally, we can construct the derivation for the entire… view at source ↗
Figure 7
Figure 7. Figure 7: Pat runtime typing second-class lifting of a disjoint runtime type environment. Rule TC-Subs allows subtyping on runtime type environments; the subtyping relation Δ ≤ Δ ′ is analogous to subtyping on Γ. Thread and frame stack typing. Rule TC-Thread types a thread, which is a pair of a currently￾evaluating term, typable under an environment Γ1, and a stack frame, typable under an environment Γ2. The combina… view at source ↗
Figure 8
Figure 8. Figure 8: Pat syntax extended for algorithmic typing [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Pat algorithmic type operations during typechecking. We can then generate and solve inclusion constraints 𝜙 on patterns [PITH_FULL_IMAGE:figures/full_fig_p018_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Pat algorithmic typing (programs, definitions, and terms) [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Pat algorithmic typing (guards) Un-annotated let expressions. Although our core calculus assumes an annotation on let expres￾sions, this is unnecessary if the let-bound variable is used in the continuation 𝑁, or 𝑀 has a synthesisable type. Specifically, TC-LetNoAnn1 allows us to check the type of the continuation and inspect the produced environment for the type of 𝑥, which can be used to check 𝑀. Similar… view at source ↗
Figure 12
Figure 12. Figure 12: Examples motivating extensions 5 EXTENSIONS It is straightforward to extend Pat with product and sum types, and by using contextual typing information prior to constraint generation, we can add higher-order functions and interfaces that allow finer-grained alias analysis. The formalisation can be found in Appendix B. 5.1 Product and Sum Types Product and sum constructors are checking cases, and must conta… view at source ↗
Figure 13
Figure 13. Figure 13: Factory use case 6.2.1 Benchmarks. Tbl. 1 shows that all but one of the mailbox calculus examples from [de’Liguoro and Padovani 2018] can be checked in strict mode. The Savina examples capture typical concurrent programming patterns, namely, master-worker (K￾Fork, Fibonacci, Log Map), client-server (Ping Pong, Counter), and peer-to-peer (Big), and common network topologies such as star (Philosopher, Smoke… view at source ↗
Figure 13
Figure 13. Figure 13: In its initial state, empty, the Warehouse expects a Prepare message (if there are Robots in the system), or none (if no Robot requests access), expressed as the guard Prepare + 1 on line 2. When a part is requested, the Warehouse transitions to the state engaged, where it awaits a Deliver message from the Door and notifies the Robot via a Delivered message (lines 9–15). Subsequent interactions that the W… view at source ↗
Figure 14
Figure 14. Figure 14: Pat type checking pipeline C SUPPLEMENTARY IMPLEMENTATION AND EVALUATION MATERIAL Our typechecking tool processes Pat programs specified in plain text files that are structured in three segments: (1) Interface definitions that establish the set of messages that a mailbox can receive; (2) Function definitions that specify processes that are instantiable using spawn; (3) Body an invocation of a function def… view at source ↗
read the original abstract

The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Behavioural types make it possible to detect communication errors early in the development process, but most work has addressed channel-based languages rather than actor languages. Mailbox types are a novel behavioural type system for actors first introduced for a process calculus, and capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language incorporating mailbox types, and describes an algorithmic type system. Pat is a higher-order functional language with sums, products, and lists, along with interfaces that allow finer-grained reasoning about mailbox contents. Typechecking in Pat detects four classes of behavioural error: protocol violation, unexpected message, forgotten reply and self-deadlock, as well as the usual data type errors. The Pat type system makes essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. We make use of a co-contextual algorithmic type system, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite. This establishes a foundation for applying mailbox typing to practical actor languages.

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 / 3 minor

Summary. The paper introduces Pat, the first programming language to incorporate mailbox types (commutative regular expressions over mailbox contents). Pat is a higher-order functional language with sums, products, and lists, plus interfaces for finer-grained mailbox reasoning. It defines a declarative type system and an algorithmic variant (via quasi-linear typing and backwards-bidirectional co-contextual typing) that is proved sound and complete w.r.t. the declarative system; the implementation detects protocol violations, unexpected messages, forgotten replies, self-deadlocks, and ordinary data-type errors. The system is evaluated on a factory-automation case study and Savina actor benchmarks.

Significance. If the soundness/completeness claims and the handling of aliasing via quasi-linear types hold, the work supplies the first practical bridge from mailbox-type process calculi to a full programming language, enabling early detection of four classes of actor communication errors. The claimed machine-checked or detailed proofs, the implemented checker, and the concrete case-study evaluation are explicit strengths that would make the contribution self-contained and reproducible.

major comments (2)
  1. [§4] §4 (algorithmic type system) and the associated soundness/completeness theorem: the central claim that the co-contextual backwards-bidirectional algorithm is sound and complete rests on the quasi-linear discipline; without an explicit statement of the quasi-linearity invariant preserved by the algorithmic rules (or a machine-checked proof artifact), it is difficult to verify that aliasing and nested evaluation contexts are fully tamed.
  2. [§3] §3 (quasi-linear typing) and the transition from the prior process calculus: the manuscript states that quasi-linear typing suffices to address aliasing, yet the load-bearing step—how the type rules prevent duplication of mailbox references inside higher-order functions or nested contexts—is only sketched; a small counter-example showing what would go wrong without quasi-linearity would make the design choice falsifiable.
minor comments (3)
  1. The abstract and introduction repeatedly cite the four error classes; a single running example that illustrates each class (with the corresponding mailbox-type error message) would improve readability.
  2. Notation for commutative regular expressions and interfaces is introduced without an early concrete example; adding one before the formal rules would help readers unfamiliar with the prior calculus paper.
  3. [Evaluation] The Savina evaluation reports successful type-checking but does not tabulate type-checking times or the size of the generated constraints; these metrics would strengthen the practicality claim.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive review and the recommendation of minor revision. The comments highlight opportunities to improve clarity around the quasi-linear discipline and its role in the algorithmic type system. We address each point below and will incorporate the suggested clarifications.

read point-by-point responses

  1. Referee: [§4] §4 (algorithmic type system) and the associated soundness/completeness theorem: the central claim that the co-contextual backwards-bidirectional algorithm is sound and complete rests on the quasi-linear discipline; without an explicit statement of the quasi-linearity invariant preserved by the algorithmic rules (or a machine-checked proof artifact), it is difficult to verify that aliasing and nested evaluation contexts are fully tamed.

    Authors: We agree that an explicit statement of the invariant would aid verification. In the revised manuscript we will add a concise paragraph in §4 that states the quasi-linearity invariant (mailbox references may not be duplicated except through the controlled mechanisms of interfaces and the co-contextual rules) and indicates how each algorithmic rule preserves it. The existing soundness and completeness proofs in the appendix already rely on this invariant via the correspondence with the declarative system; we will add a short lemma linking the invariant to the algorithmic judgements. We do not currently provide a machine-checked artifact, as the proofs were developed by detailed hand-written case analysis. revision: yes

  2. Referee: [§3] §3 (quasi-linear typing) and the transition from the prior process calculus: the manuscript states that quasi-linear typing suffices to address aliasing, yet the load-bearing step—how the type rules prevent duplication of mailbox references inside higher-order functions or nested contexts—is only sketched; a small counter-example showing what would go wrong without quasi-linearity would make the design choice falsifiable.

    Authors: We accept that a concrete counter-example would strengthen the exposition. In the revision we will insert a short example in §3 that shows a higher-order function receiving a mailbox reference; without the quasi-linear restriction the reference could be duplicated and passed to two distinct actor creations, violating the mailbox-type invariant. The example will be accompanied by the corresponding typing derivation that fails under the quasi-linear rules. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's core contributions consist of the design of the new language Pat, its declarative type system, an algorithmic version with explicit soundness and completeness proofs relative to the declarative system, and an implementation evaluated on case studies. These elements are developed directly to address aliasing and nested contexts via quasi-linear typing and backwards-bidirectional typing. Prior process-calculus work is cited only as background for the mailbox-type concept; the extension to a full programming language with interfaces, sums/products/lists, and error detection classes is presented as an independent step with its own formal development and implementation. No derivation step reduces by construction to a fitted parameter, self-definition, or load-bearing self-citation chain. The claims remain self-contained against external benchmarks and case studies.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard mathematical properties of regular expressions and the actor communication model, plus the domain-specific assumption that quasi-linear typing suffices to handle aliasing. No free parameters are introduced. Mailbox types are an extension of a prior construct rather than a wholly new invented entity.

axioms (2)
  • domain assumption Mailbox contents can be modeled by commutative regular expressions
    Stated as the basis for mailbox types in the abstract.
  • ad hoc to paper Quasi-linear typing tames aliasing and nested evaluation contexts sufficiently for a practical language
    The abstract states that the type system makes essential use of quasi-linear typing to address these challenges.

pith-pipeline@v0.9.0 · 5835 in / 1506 out tokens · 28458 ms · 2026-05-24T08:43:50.252940+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

29 extracted references · 29 canonical work pages

  1. [1]

    L 3: A Linear Language with Locations. Fundam. Informaticae 77, 4 (2007), 397–449. 27 , , Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos

    work page 2007

  2. [2]

    Polymorphic lambda calculus with context-free session types. Inf. Comput. 289, Part (2022), 104948. Roberto M. Amadio, Ilaria Castellani, and Davide Sangiorgi

    work page 2022

  3. [3]

    On Bisimulations for the Asynchronous pi-Calculus. Theor. Comput. Sci. 195, 2 (1998), 291–324. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, ...

    work page 1998

  4. [4]

    Behavioral Types in Programming Languages. Found. Trends Program. Lang. 3, 2-3 (2016), 95–230. https://doi.org/10.1561/2500000031 Mehdi Bagherzadeh and Hridesh Rajan

    work page doi:10.1561/2500000031 2016

  5. [5]

    Journal of the ACM (JACM) 11, 4 (1964), 481–494

    Derivatives of regular expressions. Journal of the ACM (JACM) 11, 4 (1964), 481–494. Avik Chaudhuri

    work page 1964

  6. [6]

    Fair termination of binary sessions. Proc. ACM Program. Lang. 6, POPL (2022), 1–30. Silvia Crafa and Luca Padovani

    work page 2022

  7. [7]

    ACM Trans

    The Chemical Approach to Typestate-Oriented Programming. ACM Trans. Program. Lang. Syst. 39, 3 (2017), 13:1–13:45. Frank S. de Boer, Dave Clarke, and Einar Broch Johnsen

    work page 2017

  8. [8]

    ACM Comput

    Bidirectional Typing. ACM Comput. Surv. 54, 5 (2022), 98:1–98:38. Robert Ennals, Richard Sharp, and Alan Mycroft

    work page 2022

  9. [9]

    Linear Types for Packet Processing. In Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings (Lecture Notes in Computer Science, Vol. 2986), David A. Schmidt (Ed.). Springer,...

    work page doi:10.1007/978-3-540-24725-8_15 2004

  10. [10]

    Linear type theory for asynchronous session types.J. Funct. Program. 20, 1 (2010), 19–50. Rosita Gerbo and Luca Padovani

    work page 2010

  11. [11]

    Joseph R

    Semigroups, Presburger formulas, and languages.Pacific journal of Mathematics 16, 2 (1966), 285–296. Joseph R. Harrison

    work page 1966

  12. [12]

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

    Types for Dyadic Interaction. In CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings (Lecture Notes in Computer Science, Vol. 715), Eike Best (Ed.). 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 1993

  13. [13]

    Multiparty Asynchronous Session Types. J. ACM 63, 1 (2016), 9:1–9:67. Mark W. Hopkins and Dexter Kozen

    work page 2016

  14. [14]

    ACM Comput

    Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49, 1 (2016), 3:1–3:36. https://doi.org/10.1145/2873052 Shams Mahmood Imam and Vivek Sarkar

    work page doi:10.1145/2873052 2016

  15. [15]

    Information and Computation 185, 2 (2003), 182–210

    Modelling environments in call-by-value programming languages. Information and Computation 185, 2 (2003), 182–210. Sam Lindley and J. Garrett Morris

    work page 2003

  16. [16]

    Rumyana Neykova and Nobuko Yoshida

    Springer, 95–109. Rumyana Neykova and Nobuko Yoshida. 2017a. Let it recover: multiparty protocol-induced recovery. In CC. ACM, 98–108. Rumyana Neykova and Nobuko Yoshida. 2017b. Multiparty Session Actors. Log. Methods Comput. Sci. 13, 1 (2017). Leo Osvald, Grégory M. Essertel, Xilun Wu, Lilliam I. González Alayón, and Tiark Rompf

    work page 2017

  17. [17]

    Luca Padovani

    Springer, 88–102. Luca Padovani. 2018a. Deadlock-Free Typestate-Oriented Programming. Art Sci. Eng. Program. 2, 3 (2018),

    work page 2018

  18. [18]

    Luca Padovani. 2018b. Mailbox Calculus Checker. https://boystrange.github.io/mcc/ Luca Padovani. 2018c. A type checking algorithm for concurrent object protocols. Journal of Logical and Algebraic Methods in Programming 100 (2018), 16–35. https://doi.org/10.1016/j.jlamp.2018.06.001 Luca Padovani

    work page doi:10.1016/j.jlamp.2018.06.001 2018

  19. [19]

    ACM Trans

    Context-Free Session Type Inference. ACM Trans. Program. Lang. Syst. 41, 2 (2019), 9:1–9:37. Rohit Parikh

    work page 2019

  20. [20]

    On Context-Free Languages. J. ACM 13, 4 (1966), 570–581. Benjamin C. Pierce and David N. Turner

    work page 1966

  21. [21]

    ACM Trans

    Local type inference. ACM Trans. Program. Lang. Syst. 22, 1 (2000), 1–44. Andrew M. Pitts

    work page 2000

  22. [22]

    Intrinsically typed compilation with nameless labels. Proc. ACM Program. Lang. 5, POPL (2021), 1–28. Alceste Scalas, Nobuko Yoshida, and Elias Benussi

    work page 2021

  23. [23]

    In PARLE ’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings (Lecture Notes in Computer Science, Vol

    An Interaction-based Language and its Typing System. In PARLE ’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings (Lecture Notes in Computer Science, Vol

    work page 1994

  24. [24]

    Maritsas, George Philokyprou, and Sergios Theodoridis (Eds.)

    , Constantine Halatsis, Dimitris G. Maritsas, George Philokyprou, and Sergios Theodoridis (Eds.). Springer, 398–413. https://doi.org/10.1007/3-540-58184-7_118 Samira Tasharofi, Peter Dinges, and Ralph E. Johnson

    work page doi:10.1007/3-540-58184-7_118

  25. [25]

    ACM Transactions on Programming Languages and Systems (TOPLAS) 39, 4 (2017), 1–46

    Scaling reliably: Improving the scalability of the Erlang distributed actor platform. ACM Transactions on Programming Languages and Systems (TOPLAS) 39, 4 (2017), 1–46. 29 , , Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder Vasco T. Vasconcelos

    work page 2017

  26. [26]

    Fundamentals of session types. Inf. Comput. 217 (2012), 52–70. Philip Wadler

    work page 2012

  27. [27]

    Propositions as sessions. J. Funct. Program. 24, 2-3 (2014), 384–418. Noam Zeilberger

    work page 2014

  28. [28]

    Pat programs are type checked following the six-stage pipeline of Fig

    Pat type checking pipeline C SUPPLEMENTARY IMPLEMENTATION AND EVALUATION MATERIAL Our typechecking tool processes Pat programs specified in plain text files that are structured in three segments: (1) Interface definitions that establish the set of messages that a mailbox can receive; (2) Function definitions that specify processes that are instantiable us...

    work page 2012

  29. [29]

    The Robot 39 , , Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J

    When a part is requested, the Warehouse transitions to theengaged state and awaits a Deliver message from the Door, notifying the Robot collecting the part via a Delivered message (lines 86–92). The Robot 39 , , Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder acknowledges the delivery by sending PartTaken, as the guard o...

    work page 2018