Message passing-based programming is one of the dominant concurrent 
programming models today in both research and practice. However, we do 
not yet have a mechanized foundation for message passing models to aid both 
research and education. The main contribution of this work is a mechanized core calculus in Coq to aid study of message passing concurrency. Some salient properties of our calculus are the following. First, the novel expression-based calculus supports message-passing expressions such as spawning a process, sending a message to a process, receiving a message along with standard expressions from the familiar simply typed lambda calculus (STLC) that facilitates understanding STLC first, and then understanding message passing abstractions. This is arguably different from prior works that have proposed entirely process-based calculi, but closer to practice where message passing primitives are mixed with computational primitives. Second, the calculus provides statically typed foundations for message passing concurrency by incorporating an intensional design of the receive primitive. Third, the calculus 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. Fourth, the calculus 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. Our innovations are enabled by a novel Coq library for parallel composition that supports structural congruence.