April 17th Meeting: Jake Donham on Twelf

The April meeting of BayFP is Thursday the 17th at 7:30pm at Citizen Space, 425 2nd Street, #300, San Francisco:

View Larger Map

Jake Donham will be giving his talk on Twelf that was postponed from last month.

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.

As always, the talk is free and open to all