POPL 2020 (series) / PLMW 2020 (series) / PLMW 2020 / Theorem provers are a P.L. researcher's best friend
Theorem provers are a P.L. researcher's best friendMentoring Event
Interactive and automated theorem proving are increasingly used in programming language research. I will discuss why this machine assistance is useful, and how it enables a quantitative jump in the complexity of the P.L. artifacts that can be formalized and in the confidence we can have in these formalizations. The talk will include a short demo of the Coq proof assistant.
| Coq demo (demo.v) | 5KiB |
| Slides (Leroy-PLMW20.pdf) | 674KiB |
Tue 21 JanDisplayed time zone: Saskatchewan, Central America change
Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change
10:30 - 12:30 | Morning 2PLMW at Ile de France III (IDF III) Chair(s): Robbert Krebbers Delft University of Technology | ||
10:30 40mTalk | Making Progress Under Uncertainty in SMT Solving, Research, and LifeMentoring Event PLMW Lindsey Kuper University of California, Santa Cruz Media Attached | ||
11:10 40mTalk | Research as a collaborative effortMentoring Event PLMW Marco Gaboardi Boston University Media Attached File Attached | ||
11:50 40mTalk | Theorem provers are a P.L. researcher's best friendMentoring Event PLMW Xavier Leroy Collège de France Media Attached File Attached | ||
