University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > A POPLmark retrospective: Using proof assistants in programming language research

A POPLmark retrospective: Using proof assistants in programming language research

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

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 Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity