POPLmark 15 Year Retrospective Panel

This panel will bring together experts in mechanized metatheory with the broader POPL community for a discussion of the POPLmark challenge 15 years later, with an eye toward the future. 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.

Format

• 10 minute background presentation (Benjamin Pierce)
• 70 minutes Q&A (planned and audience questions)
• 10 minutes conclusion

Content

Here are just a few examples of what we hope to discuss:

• What did we learn about different proof assistants and different binding styles from the challenge itself?
• What happened in the years immediately following the POPLmark challenge?
• What about POPLmark led to its impact? What can we learn from that in designing future benchmark suites for mechanized metatheory, and for programming languages in general?
• What has changed since 2005, and what new challenges has this brought with it?
• What problems raised in POPLmark were underaddressed? How can we address them?

You can send us your own questions in advance using this form, and you can ask questions in person during the second half of the Q&A.

Attending

This is completely free if you’re registered for POPL—no need to sign up separately! Just show up on January 21st. Hopefully see you there!

Takeaways from the panel can be found in this SIGPLAN Perspectives blog post. A video of the panel in its entirety can be found on YouTube.