This paper investigates an approach for statically preventing race conditions in an object-oriented language. The setting
of this work is a variant of Gordon and Hankin’s concurrent object calculus. We enrich that calculus with a form of dependent
object types that enables us to verify that threads invoke and update methods only after acquiring appropriate locks. We establish
that well-typed programs do not have race conditions.