Write a Blog >>

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.

No schedule or scheduled events are not visible yet, check back later

Not scheduled yet

POPL-2020-poplmark-15-year-retrospective-panelNot scheduled yet



Notes from the panel will be published here following the event.