This talk starts with a brief overview of contemporary research in programming languages, emphasizing the growing importance of software verification in this field. Automatic and interactive theorem provers play an important role in this area. I give a short introduction to the Coq proof assistant, then emphasize how Coq and other interactive theorem provers are changing the way the programming languages community conducts and publishes research.
Xavier.Leroy@inria.fr