If you want to play with the system, I uploaded a hacked-up version of twelf 1.5R1 to
http://www.cs.cmu.edu/~jcreed/transfer/nettwelf.tar.gz
and the current version of the swf file is at
http://www.cs.cmu.edu/~jcreed/transfer/twelftut.swf
it is bound to change a lot, though; I'm still reconsidering how to explain dependent types, even though my intended audience here (some of the kids taking HOT) probably knows about them pretty well, since we've covered them at the kind level, for giving functors types.
You can still look at the slides without running the server; just use CTRL-LEFT and -RIGHT to move between slides.
To run the server, unpack twelf, and compile nettwelf/src/netserver/sources.cm, and then evaluate NetServer.server 1066 at the toplevel.
Download the swf file somewhere, open it in the Flash viewer, hit the "connect" button on the first slide. Later when you get to one of the gray boxes with the little twelf logo in it, you can click on the logo or hit ENTER to submit the current text to the server.