Over the years, many programming languages were proposed with the goal of being free from data races. The concept of monitors, in particular, was envisioned precisely to prevent data races. In this thesis, we describe a data-race-free programming language inspired by monitors. Our languages features threads, shared memory with referential semantics, unbounded loops, and a novel construct that emulates monitor capabilities. This new construct is interesting because it is simpler and at the same time more flexible than monitors. We prevent data races in the language by using a type system that allows only immutable or protected data to be shared among threads. We defined the small-step operational semantics of this language through three distinct and hierarchically layered single-step operations: roughly, the first layer represents individual cores, the second layer manages the shared memory, and the third layer manages the thread pool. Over these relations, we defined a multistep relation that produces a trace of program execution. We use this trace to prove the absence of data races. All these results were formally defined and proved in Coq.