All done! After spending quite some time on writing the thesis, I have successfully completed my PhD studies in June 2015. The thesis, a lengthy 386 pages of PDF, contains a lot of ideas, descriptions and justifications on capturing interactive proof process to facilitate extraction of reusable proof strategies as well as for other uses.
The thesis is titled Capturing Proof Process and is available in the publications list. The tools described in this thesis — the ProofProcess framework — are available on GitHub. Time permitting, I am hoping to continue improving the tools and update them to the most recent versions of the supported theorem provers.
As my first post-doctoral position, I have started working on the Taming Concurrency project together with Prof. Cliff Jones. The project tries to unpick the popular approaches to concurrency reasoning, namely the Rely/Guarantee thinking and Separation Logic to get to the underlying issues, ideas and strengths in order to improve the overall approach to reasoning about concurrency in software.