Compiling concurrency correctly : verifying software transactional memory

This thesis considers the problem of formally verifying an implementation of STM, and outlines a new approach to concurrent compiler correctness using the notion of bisimulation, implemented using the Agda theorem prover.