Logo

Mechanized semantics:

when machines reason about their languages

Xavier Leroy

Collège de France, chair of software sciences, 2019-2020

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"".

Abstract

"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.

This course presents this mechanized semantics approach on examples of small imperative or functional languages, with many applications ranging from program logics to the verification of compilers and static analyzers. All these concepts are entirely mechanized using the Coq proof assistant. However, a large part of the course remains accessible without prior knowledge of Coq. The companion seminar developed the approach further in several directions, from the mechanization of "big" programming languages such as Javascript and Rust to the use of proof assistants for teaching programming languages foundations.

Lectures

Companion Coq development

The full commented Coq sources are available from the cdf-mech-sem Github project.

Seminar talks

Some talks were given in English, others in French. Video recordings and slides can be found on the main course pages.


Xavier.Leroy@college-de-france.fr