BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Mini Courses in Theoretical Computer Science
SUMMARY:Mechanizing Theories in Twelf: A Tutorial (Part 1)
- Susmit Sarkar
DTSTART;TZID=Europe/London:20070227T100000
DTEND;TZID=Europe/London:20070227T120000
UID:TALK6640AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/6640
DESCRIPTION:As researchers in theory\, and in particular\, pro
gramming language theory\, we are interested in th
eorems and proofs. For high-assurance\, we want th
ese to be checkable automatically. Various proof a
ssistants have been devised and used for mechanizi
ng some realistic proofs\, as well as challenges s
uch as POPLmark. The Twelf tool is such a proof as
sistant\, with support for representation of forma
l systems and inductive proofs over them. It suppo
rts and encourages a method of representation know
n as higher-order abstract syntax\, which simplifi
es reasoning about systems with binding structures
and with hypothetical reasoning.\n\nThis course i
s a tutorial introduction to Twelf\, in its role a
s a system for representing formal systems and che
cking proofs about them. We will look at encodings
of systems\, proofs about them\, and helpful stra
tegies 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 metatheory of programming language
s and type systems.\n\nCourse materials will be pu
t "here":http://www.cl.cam.ac.uk/~ss726/twelf/ .
LOCATION:Computer Laboratory\, Room FW11
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR