" What exactly does this program do ? " To answer this question with the precision of mathematics, we need a formal semantics of the language in which this program is written. Several approaches to formal semantics are well established today : denotational semantics, which interpret the program as an element of a mathematical structure ; operational semantics, which describe the successive stages of program execution ; axiomatic semantics, which describe the logical assertions satisfied by these executions. These formal semantics have numerous applications : not only do they define programming languages with far greater precision than a reference manual written in French or English, but they also verify the correctness of algorithms and tools that operate on programs, such as compilers, static analyses and program logics.
The semantics of a programming language can be voluminous and complex, making " on paper " demonstrations using these semantics tedious and unreliable. But we can enlist the help of the computer ! Demonstration assistants (Coq, HOL, Isabelle, etc.) provide a rigorous language for defining semantics, stating their properties, writing demonstrations and automatically checking the consistency of these demonstrations. This mechanization is a powerful lever for scaling semantic approaches to realistic programming languages and tools.
The lecture presented this mechanized semantics approach on the example of small imperative or functional languages, with applications to program logic and the verification of compilers and static analyzers. All these notions have been fully mechanized with the Coq wizard. Coq development is available at https://github.com/xavierleroy/cdf-sem-meca.
The seminar took the approach further in several directions, from the mechanization of " real-world languages " such as Javascript and Rust, to the use of demonstration wizards to teach the fundamentals of programming languages.