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: Saskatchewan, Central America change