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’’.
| supervisors | Martin Steffen |
| Duo link | thesis text |