Ao longo dos anos, muitas linguagens de programação foram propostas com o objetivo de prevenir condições de corrida para acessos à memória. O conceito de monitores, em particular, foi concebido justamente para evitar condições de corrida com acessos à memória. Nesta tese, nós descrevemos uma linguagem de programação inspirada por monitores e livre desse tipo de condição de corrida. Nossa linguagem possui threads, memória compartilhada com ponteiros, laços não limitados, e uma construção nova que emula as capacidades de monitores. Essa nova construção é interessante porque é mais simples e, ao mesmo tempo, mais flexível do que monitores. Nós prevenimos condições de corrida na linguagem por meio de um sistema de tipos que permite apenas o compartilhamento entre threads de dados imutáveis ou protegidos. Nós definimos a semântica operacional em passo pequeno da nossa linguagem por meio de três operações distintas e hierarquicamente organizadas: grosseiramente, a primeira camada representa núcleos individuais, a segunda camada gerencia a memória compartilhada e a terceira camada gerencia o conjunto de threads. Sobre essas relações, nós definimos uma relação de múltiplos passos que produz um traço da execução do programa. Nós usamos esse traço para provar a ausência de condições de corrida. Todos esses resultados foram formalmente definidos e provados em Coq.