The POPLmark 15 Year Retrospective Panel will bring together experts in mechanized metatheory with the broader POPL community for a discussion of the POPLmark challenge 15 years later. The POPLmark challenge is a benchmark suite for mechanized metatheory that drew solutions in many different proof assistants using many different techniques, inspired discussion within the community, and influenced hundreds of papers in mechanized metatheory. Since POPLmark, mechanization of metatheory in POPL papers has gone from a rare occurrence to a norm.
For a paper with that much influence, it is important to answer as a community what we can learn going forward. Discussions with those involved, however, suggests that there is still no consensus on the answer to this question. This panel will bring that discussion into the spotlight and aim, when possible, to reach consensus. It will discuss lessons from POPLmark and the evolution of mechanized metatheory since POPLmark as relevant to the field of mechanized metatheory, to the design of future benchmark suites and challenges, and to the POPL community more broadly.
Notes from the panel will be published here following the event.