In this report we describe the formalisation of a simple imperative language with concurrent/parallel and atomic execution statements within the Coq theorem prover. Our formalisation includes the specification of a simple imperative programming language with statements for parallel and atomic execution of code, an underlying small-step structural semantics and a proof system that is sound with respect to such semantics. With this formalisation we give a first step towards the certified verification of shared- variable concurrent/parallel programs under the context of Cliff Jones? Rely-Guarantee reasoning and in the logic of Coq.