This is an English translation of Xavier Leroy's 2019-2020 lectures at Collège de France, "Sémantiques mécanisées : quand la machine raisonne sur ses langages"".
"What does this program do, exactly?" To answer this question with mathematical precision, we need a formal semantics for the language in which this program is written. Several approaches to formal semantics are well understood today: denotational semantics, which interpret the program as an element of a mathematical structure; operational semantics, which describe the successive steps in program execution; axiomatic semantics, which describe the logical assertions satisfied by all the executions. These formal semantics have man applications: not just defining programming languages with much higher precision than English prose in a reference manual, but also verifying the correctness of the algorithms and the tools that operate over programs, such as compilers, static analyzers, and program logics.
The semantics of a programming language can be bulky and complicated, making "pencil-and-paper" proofs based on these semantics painful and unreliable. However, we can get help from the computer! Proof assistants (Coq, HOL, Isabelle, etc.) provide us with a rigorous language to define the semantics, state their properties, write proofs interactively, and check the soundness of these proofs automatically. This mechanization acts as a powerful lever to scale semantic-based approaches up, all the way to realistic programming languages and tools.
Some talks were given in English, others in French. Video recordings and slides can be found on the main course pages.