Write a Blog >>
Tue 21 Jan 2020 11:50 - 12:30 at Ile de France III (IDF III) - Morning 2 Chair(s): Robbert Krebbers

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 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

10:30 - 12:30: PLMW 2020 - Morning 2 at Ile de France III (IDF III)
Chair(s): Robbert KrebbersDelft University of Technology
PLMW-POPL-202010:30 - 11:10
Lindsey KuperUniversity of California, Santa Cruz
Media Attached
PLMW-POPL-202011:10 - 11:50
Marco GaboardiBoston University
Media Attached File Attached
PLMW-POPL-202011:50 - 12:30
Xavier LeroyCollège de France
Media Attached File Attached