2nd (as of Fall 2006) year PhD student at CMU. More info at my homepage. I'm lucky enough that my research heavily involves formalization and metatheorem proving in Twelf. Among other things, I try to contribute interesting/advanced examples to the Twelf wiki. With the help of the other wiki elves, these examples become informative and human consumable. I've seen and fought a number of strange and challenging Twelf metatheorem proving related beasts in my travels, so if you've got questions or requests make a note in User talk:DanielKLee or The Twelf Project: To do.