BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Mechanizing Theories in Twelf: A Tutorial (Part 3) - Susmit Sarkar
DTSTART:20070305T100000Z
DTEND:20070305T120000Z
UID:TALK6642@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:As researchers in theory\, and in particular\, programming lan
 guage theory\, we are interested in theorems and proofs. For high-assuranc
 e\, we want these to be checkable automatically. Various proof assistants 
 have been devised and used for mechanizing some realistic proofs\, as well
  as challenges such as POP Lmark. The Twelf tool is such a proof assistant
 \, with support for representation of formal systems and inductive proofs 
 over them. It supports and encourages a method of representation known as 
 higher-order abstract syntax\, which simplifies reasoning about systems wi
 th binding structures and with hypothetical reasoning.\n\nThis course is a
  tutorial introduction to Twelf\, in its role as a system for representing
  formal systems and checking proofs about them. We will look at encodings 
 of systems\, proofs about them\, and helpful strategies to convince Twelf 
 we have a good proof. We will also learn how to understand a proof we get\
 , and believe in these proofs. Our examples will be drawn from the metathe
 ory of programming languages and type systems.\n\nCourse materials will be
  put "here":http://www.cl.cam.ac.uk/~ss726/twelf/ .
LOCATION:Computer Laboratory\, Room FW11
END:VEVENT
END:VCALENDAR