Abstract

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?’