Abstract

In accordance with the tradition wherein the freshly doctored, once their condition has become merely radioactive as opposed to critical, explain to their erstwhile colleagues what they were up to all that time, I will seek to reassure my sponsors that I accomplished more in my four years than just the removal of my hair.

Type theories such as that implemented in a certain proof assistant(*) allow inductively defined families of types, associating computational behaviour with their elimination rules. In the early 1990s, Thierry Coquand suggested programming with families in a more intuitive pattern matching style: partially implemented in ALF, it gave rise to a number of undecidable problems, and its status with respect to the `elim rule' presentation was never entirely clear. Martin Hofmann and Thomas Streicher showed that pattern matching admits a particular elimination rule for equality (`axiom K') not derivable conventionally. My thesis shows that adding K is sufficient to recover Coquand's system.

This proof has a practical benefit in that it suggests the realistic possibility of a functional language equipped with dependent families. I will attempt to explain what such a thing might be like and why we absolutely positively have to have it, with the aid of examples from my thesis and from more recent work.

(*) My legal adviser advises that mentioning its name might result in litigation from a certain Danish toy manufacturer.