Video and Slides from Jake Donham’s Talk
Here are the video and slides from the April 17th meeting.
This work is licensed under a Creative Commons Attribution 3.0 Unported License.
{ Monthly Archives }
April 2008
This work is licensed under a Creative Commons Attribution 3.0 Unported License.
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:
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