### Honours Thesis

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