March 12th: Jake Donham on Twelf (UPDATED)

UPDATE: This meeting has been relocated and the talk postponed. We’ll meet for pizza instead at Amici’s, 216 King St. @ 3rd street in San Francisco.

Thanks to the nice folks at Twitter, we have a home for our next Bay FP meeting on Wednesday March 12th @
7:30pm.  Jake Donham will be speaking about Twelf:

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.

Twitter: 164 South Park St, San Francisco, CA 94107

View Larger Map

It’s a building with a dark green door.  People can just come on in and walk to their right to a large conference room.