Message passing-based programming is one of the dominant concurrent programming models today in both research and practice. The major challenge in message passing concurrency is to reason about the type of message received by any process and its effect. We present λir, a message passing-based language that incorporates an intensional design of the receive expression to solve this problem. Intensional design of receive expression integrates static and dynamic type checking and allows the effect of the message received to be intensionally inspected through a notion of dynamic typing. This enables reasoning about the effect of the message received from the head of the mailbox while retaining static type safety. We demonstrate the applications of intensional design of receive expression in various programming patterns like multiplexing, safe pipelining, encoding state machines and supporting the chain of responsibility pattern. In each of these applications, intensional receive helps in providing better safety. We have also formalized λir using the Coq proof assistant and prove its soundness. λir provides built-in proofs for guaranteed delivery of messages and encodes actions as an integral part that makes it possible to describe and prove properties about happens-before relations. λir comes with a range of extensions like broadcasting, multicasting, guarded receive, non-blocking receive, and synchronization primitive "wait" that not only provide insights into the extensibility

of the calculus, but also provide pedagogical examples of how it can be extended.