Developing Dependently Typed Programs in LEGO

1. opening credits
2. natural numbers
3. finite set family
4. finite set elimination
5. and-elim digression
6. applying generic elim rules specifically | Henry Ford generalisation
7. John Major equality
8. lifting a finite mapping | lift that function
9. thinning a finite set | thin at fz | thin at fs | thin's code
10. thickening a finite set | through thick and thin
11. the tree syntax
12. mapping the leaves
13. the occur check
14. check's elim rule
15. proving checkElim | induction t | eliminate thick | apply ind hyps
16. it's a knockout
17. unification as optimisation | the Unifier property
18. accumulating
19. downward closure
20. the optimist's theorem | the optimist's proof
21. accumulating a unifier
22. idempotent substitutions
23. embeddings
24. bounded mgu
25. base cases
26. conclusions
27. where now?

Conor McBride

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