Conor has always had a turn of phrase - every paper has at least one gem. * "the engineering of coincidence is replaced by the propagation of consequence" (htt

Conor has always had a turn of phrase - every paper has at least one gem. * "the engineering of coincidence is replaced by the propagation of consequence" (https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf) * "programmers who do not wish the ordering guarantees are entitled not to pay and not to receive", or "We could plough on with proof and, coughing, push this definition through, but tough work ought to make us ponder if we might have thought askew." (https://strathprints.strath.ac.uk/51678/7/McBride_ICFP_2014_How_to_keep_your_neighbours_in_order.pdf https://strathprints.strath.ac.uk/51678/7/McBride_ICFP_2014_...) * "be minimally prescriptive, not maximally descriptive" (https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf) Their papers are also generally presented very well - easy to follow, as these things go (by which I mean it's actually feasible to work through with a pencil and paper and understand the contents within a few hours). I really recommend PolyTest which is particularly edifying; before I learned the "avoid the green slime" principle, dependent types were a battle, but when I read it I was enlightened, and it's super interesting to watch the types evolve as the problem is understood.