For my thesis I focussed on computer-checked proofs about linearly typed programming languages, or, ways to make software less shit using maths. The inspiration for my foray into type theory was Rust, which is probably now the most popular language to incorporate linear types. Along the way, I wrote computer-checked proofs using the Coq proof assistant, and learnt a bunch about dependently typed programming.
I’d like to thank the ever-stimulating PLS research group, and in particular my supervisors Ben and Gabi.
Full text: A Library Based Approach to the Verification of Languages with Linear Types
Accompanying Coq code: dblib-linear on GitHub