Next: opening credits
Developing Dependently Typed Programs in LEGO
- opening credits
- natural numbers
- finite set family
- finite set elimination
- and-elim digression
- applying generic elim rules
specifically |
Henry Ford generalisation
- John Major equality
- lifting a finite mapping |
lift that function
- thinning a finite set |
thin at fz |
thin at fs |
thin's code
- thickening a finite set |
through thick and thin
- the tree syntax
- mapping the leaves
- the occur check
- check's elim rule
- proving checkElim |
induction t |
eliminate thick |
apply ind hyps
- it's a knockout
- unification as optimisation |
the Unifier property
- accumulating
- downward closure
- the optimist's theorem |
the optimist's proof
- accumulating a unifier
- idempotent substitutions
- embeddings
- bounded mgu
- base cases
- conclusions
- where now?
Conor McBride
Laboratory for Foundations of Computer Science
Division of Informatics (Vladivostok)
University of Edinburgh
This is the uncut version of the talk I gave (slightly differently
each time) at
- Institute for Representation and Reasoning,
Division of Informatics (Moscow),
University of Edinburgh
- Programming Research Group,
Computer Laboratory,
University of Oxford
- Dependent Types in Programming 1999,
organised by Chalmers University, Goteborg
- Automated Reasoning Group,
Computer Laboratory,
University of Cambridge
Next: opening credits
Conor's Work Page