How do we specify concurrent programs? In the presence of concurrency, programs must be viewed as components that interact with their environment. This intuition has developed into bisimulation, an observational equational theory for reasoning about concurrent programs. Interaction Trees(ITrees) represent impure and recursive programs in Coq. In essence, it is a coinductive variant of a free monad. Its free monadic structure provide a modular method of reasoning about effects. Coinduction allows ITrees to represent recursive programs as infinite data structures and sets ground to a straightforward application of bisimulation. \textit{Weak bisimulation}, a method of encapsulating internal interactions within a component, observes behavioral equivalence of ITrees. This equational theory serves as a clean, modular proof technique for equating impure, recursive programs. A natural extension of Interaction Trees, then, is to use its bisimilarity proof techniques for reasoning about concurrent programs in Coq. In this extended abstract, we present a preliminary model of concurrent, and possibly interleaving Interaction Trees.