March BayFP Meeting
March 7, 2008 | Be the first to comment
The next BayFP meeting is Wednesday, March 12th. Something a little different this time (although with some connections to Burak Emir’s talk last month about pattern matching in Scala); I’ll 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.
Posted by: Jake
Categories: Technology, Programming
