These slides were first shown at the Dagstuhl Seminar Dependent Type Theory Meets Practical Programming in August 2001.
If your browser doesn't do frames (or does them by hanging), you've had it, I'm afraid. You see, in the pages which follow, the pictures appear in a frame on the left of the window, whilst the commentary, such as it is, appears on the right, together with the navigation links. Links within the main body of the commentary advance the accompanying image appropriately. Any supplementary references can be found at the end.
While you're reading this, your browser, unless it's too clever by half, has started loading the images for the first few slides. In fact, it should be loading the images for the whole talk. That's what the dots at the bottom lead to. If you're on a fast line, don't bother waiting. Otherwise, it might be a good idea to have a cup of tea, or whatever takes just over half a meg, and let your cache fill up with entertainment.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.