Deadlocks are a common error in programs with lock-based concurrency. Type- and effect-systems are formal systems for statically analyzing programs. This thesis is concerned with one particular such system designed to capture potential deadlocks at compile time.
Despite careful design of the systems and meticulous proof-reading, the
ultimate correctness of mathematical formalizations and corresponding correctness proofs hinges on many subtle details of
the type system, the semantics etc. A machine checked proof, using a
theorem prover, increases the confidence in the formal validity of the
result. So, besides sketching the effect system for statically checking
of absence of deadlock, we report on the a machine-checked formalization
of the system and parts of the proofs, using Coq, a well-known
type-theoretic theorem prover, and OTT, a ``domain-specific language for
semanticists''.
The thesis can be found at the official DUO web page.