BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A POPLmark retrospective: Using proof assistants in programming la
 nguage research - Stephanie Weirich - University of Pennsylvania\, USA
DTSTART:20091202T141500Z
DTEND:20091202T151500Z
UID:TALK20742@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:Almost five years ago\, a group of researchers at Penn and Cam
 bridge\nissued the POPLmark challenge: a set of challenge problems designe
 d to\ndemonstrate the effectiveness of proof assistants for programming\nl
 anguage research. Programming language papers often are accompanied\nby lo
 ng technical reports containing the details of the proofs. These\nproofs e
 xist merely to bolster confidence in the results---they are\nrarely read c
 losely. Ideally\, such proofs should be expressed in these\nformal logic o
 f a proof assistant. Our vision was a world where all\nprogramming languag
 e conference papers (such as for POPL) were\naccompanied by machine-checke
 d appendices.\n\nIn this overview talk\, I will revisit the motivation of 
 the POPLmark\nchallenge to reflect on the progress we and others with simi
 lar vision\nhave made since the challenge was issued. I won't assume any p
 rior\nknowledge of language semantics. Instead\, I will focus on the\nques
 tions of 'What is the role of a proof assistant in PL research?'\,\n'Did w
 e get where we wanted to go?' and 'Where do we go from here?'\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR