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 3)
- Susmit Sarkar
DTSTART;TZID=Europe/London:20070305T100000
DTEND;TZID=Europe/London:20070305T120000
UID:TALK6642AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/6642
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 POP Lmark. The Twelf tool is such a proof a
ssistant\, with support for representation of form
al systems and inductive proofs over them. It supp
orts and encourages a method of representation kno
wn as higher-order abstract syntax\, which simplif
ies reasoning about systems with binding structure
s and with hypothetical reasoning.\n\nThis course
is a tutorial introduction to Twelf\, in its role
as a system for representing formal systems and ch
ecking proofs about them. We will look at encoding
s of systems\, proofs about them\, and helpful str
ategies 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 b
e drawn from the metatheory of programming languag
es and type systems.\n\nCourse materials will be p
ut "here":http://www.cl.cam.ac.uk/~ss726/twelf/ .
LOCATION:Computer Laboratory\, Room FW11
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR