A POPLmark retrospective: Using proof assistants in programming language research

Add to your list(s) Download to your calendar using vCal

• Stephanie Weirich - University of Pennsylvania, USA
• Wednesday 02 December 2009, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Mateja Jamnik.

Note change of speaker!

Almost five years ago, a group of researchers at Penn and Cambridge issued the POP Lmark challenge: a set of challenge problems designed to demonstrate the effectiveness of proof assistants for programming language research. Programming language papers often are accompanied by long technical reports containing the details of the proofs. These proofs exist merely to bolster confidence in the results—-they are rarely read closely. Ideally, such proofs should be expressed in these formal logic of a proof assistant. Our vision was a world where all programming language conference papers (such as for POPL ) were accompanied by machine-checked appendices.

In this overview talk, I will revisit the motivation of the POP Lmark challenge to reflect on the progress we and others with similar vision have made since the challenge was issued. I won’t assume any prior knowledge of language semantics. Instead, I will focus on the questions of ‘What is the role of a proof assistant in PL research?’, ‘Did we get where we wanted to go?’ and ‘Where do we go from here?’

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.