Twelf is a proof assistant and programming language based on typed logic programming.It is full of interesting and beautiful ideas. I’m going to use Twelf as a jumping-off point to talk about some of those ideas: judgments and inference rules; proof search and logic programming; proofs as programs; dependent types; higher-order abstract syntax. I won’t go too deep into the technicalities of Twelf but I’ll try to explain why Twelf is interesting in comparison with other proof assistants like Coq.Slides are available at http://docs.google.com/Presentation?id=dgqkzd94_0d5svjkgrAbout Bay Area Functional Programmers: BayFP meets monthly with talks on functional programming. Slides and videos from previous talks are available at http://bayfp.org/blog/. The group mailing list is http://groups.google.com/group/bayfp/. Less