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 1) - Susmit Sarkar
DTSTART:20070227T100000Z
DTEND:20070227T120000Z
UID:TALK6640@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 POPLmark. The Twelf tool is such a proof assistant\
 , with support for representation of formal systems and inductive proofs o
 ver them. It supports and encourages a method of representation known as h
 igher-order abstract syntax\, which simplifies reasoning about systems wit
 h 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 o
 f systems\, proofs about them\, and helpful strategies to convince Twelf w
 e 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 metatheo
 ry 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