• Outrageous but Meaningful Coincidences, being my attempt to get my own show in Baltimore by implementing a small dependent type theory in Agda.
  • Ornamental Algebras, Algebraic Ornaments, tout seul. This paper explains how to formalize an overlay from my millenial propaganda talk, or it would do if it was in any shape. The code does the business, though. The idea is to encode how one datatype can be built from another by a combination of refinement and annotation. By doing so, we expose coincidences as the consequences of design choices and gain the coresponding functionality for free.
  • Why walk when you can take the tube?, with Lucas Dixon and Peter Hancock. Lucas said we should compress open terms, speeding up access to the variables. I said a tube is what you get when you line up holes in a sequence, so Tube F = List (∂F 0). Hank said you can explore a structure by collecting the ways to move the cursor down : F → F ⋅ (∂F × I). This draft is very drafty: code one wet Sunday in Aberystwyth, 2006; formatting, section headings, and chat on the train back to Nottingham.

What this page used to say


Old slides live in the Colour Supplement. Newer slides live in my filing cabinet (sorry!), but my APPSEM 2003 gig Sense and Sensibility has been scanned recently (ta!). Thatcher's children and inquisitive non-Brits may find this helpful...