Conor's Publications

Drafts

• 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

.bib

• Eliminating Dependent Pattern Matching with Healfdene Goguen and James McKinna proves the reducibility of dependent pattern matching to old-fashioned eliminators and heterogeneous equality. In particular, we show how to formulate reduction rules which actually make sense, and that the translated programs preserve this computational behaviour.
• Exploring the Regular Tree Types with Peter Morris and Thorsten Altenkirch. Draft.
• A Few Constructions on Constructors with Healf Goguen and James McKinna. Draft.
• Why Dependent Types Matter with Thorsten Altenkirch and James McKinna. Submitted to ICFP 2005.
• my AFP notes on practical dependently typoed programming in Epigram. In colour. Shortly to appear in an LNCS volume.
• I am not a number: I am a free variable with James McKinna. This is the first instalment of how-to-implement-Epigram, but it's generally useful stuff if you're hacking around with syntax. Presented at the Haskell Workshop 2004, in Utah, but not by either of us: thanks to Thomas, no thanks to KLM.
• The view from the left with James McKinna. By accident, this paper is effectively the definition of Epigram Status: in JFP 14(1). Here's our typechecker example, written almost live at MGS this year. And yes, we know about the bug in the ML version of elem to be found in this draft: simple type systems have the property that you can replace any subexpression of a well-typed term by another of the same type!
• The view from the left (as we originally wrote it) This version has much less to say about typechecking and much more to say about interactive programming.
• First-order unification by structural recursion Contains the world's shortest termination proof of unification... Status: in JFP 13(6). Accompanied by online resources (correctness proof, OLEG development).
• Faking It (Simulating Dependent Types in Haskell). Even before the revolution, we can still abuse the class system. With a side order of nested-types-are-not-as-much-fun.
• Inductive Families Need Not Store Their Indices with Edwin Brady and James McKinna. The more static information your compiler has, the better the object code it can spit out. Epigram has more static information than we know what to do with. This paper shoots the first few fish in that barrel. Status: in TYPES 2003.
• With the Container gang: Michael Abbott, Thorsten Altenkirch, and Neil Ghani:
  • Derivatives of Containers I got these guys to differentiate data structures and they gave me a lollipop. Status: in TLCA 2003.
  • $\partial$ for Data is a marmalized version of the above, with more type theory and lots of pictures. In Fundamenta Informaticae.
  • Constructing Polymorphic Programs with Quotient Types That's entertainment. Status: in MPC 2004.
• Generic Programming Within Dependently Typed Programming with Thorsten Altenkirch. Here we give a universe construction for a whole scary bunch of types you'd find in Haskell, and then we write some generic programs using OLEG. It's a pity Epigram wasn't around at the time. Status: in WCGP 2002.
• Elimination with a Motive. A modern convenience no theorem prover should be without. Sez I. Status: in TYPES 2000.
• Dependently Typed Programs and their Proofs. My campaign to burn my thesis has not yet succeeded. It's still the only place where I've written up OLEG, my holey type theory with proof-states-as-valid-contexts, tactics-as-admissible-rules. It's also the place to go for all those gadgets like proofs of Peano axioms. Caution: I was East Ham when I wrote it. Many thanks to my supervisor, Rod Burstall, and to my uncles, James McKinna, Healf Goguen and Martin Hofmann. Apologies to my examiners, Christine Paulin-Mohring and Alex Simpson.
• Inverting Inductively Defined Relations in LEGO. The paper emerging from my MSc, supervised by James McKinna and Alan Smaill. This is where I learned the song I've been singing ever since. Status: in TYPES 1996.
• The Derivative of a Regular Type is its Type of One-Hole Contexts Status: unpublished. My most influential work, some allege.

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...