Periodic Reporting for period 4 - Mathador (Type and Proof Structures for Concurrent Software Verification)

The key goal of the project has been to design a theory of types for fine-grained shared-memory concurrent programs. Such a type theory is a system in which one can write concurrent programs and package them with their correctness proofs into an encapsulated whole, so that the...