[TYPES/announce] POPLmark Retrospective Panel at POPL: Come, and send us your questions!

[Talia Ringer]

Hi all,

As many of you book your tickets to New Orleans for POPL, I*’d like to
encourage you to be there on* Tuesday, January 21st (the day before POPL,
or the last day of CPP) for the POPLmark 15 Year Retrospective Panel
<https://popl20.sigplan.org/track/POPL-2020-poplmark-15-year-retrospective-panel>.
This panel will take a look back at the influential POPLmark Challenge
<https://www.seas.upenn.edu/~plclub/poplmark/> for mechanized metatheory 15
years later, with an eye toward the future. It should be an exciting panel
for anyone who is interested in proof assistants, mechanized metatheory,
and in benchmark suites and challenges to help the POPL community more
broadly. .

We have some stellar panelists:


   -

   Benjamin Pierce (Penn)
   -

   Peter Sewell (Cambridge)
   -

   Xavier Leroy (Collège de France)
   -

   Robby Findler (Northwestern)
   -

   Scott Owens (Kent)
   -

   Brigitte Pientka (McGill)


We want to make sure this is a fun and engaging panel, so if you have
anything you’d like to hear the panelists discuss, we’d love your questions
ahead of time (we’ll of course also take questions in person at the panel). You
can send questions using this form
<https://docs.google.com/forms/d/e/1FAIpQLSe-svhT0wbY5uXNggGYJQGTdt5DNvA9ZY30A_MAQmbzetXO-Q/viewform?usp=sf_link>.
No need to shy away from controversy (we have a great moderator), and don’t
worry if you aren’t sure if your question is worth asking. Just send us
anything you’d like to hear about related to the POPLmark challenge,
mechanized metatheory, and benchmark suites and challenges.

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?

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!

Talia Ringer (UW)

http://tlringer.github.io/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20191227/d9793445/attachment.html>