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 many 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, ...) provide us with a rigorous language to define the semantics, state their properties, write proofs interactively, and check the correctness 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 the foundations of programming languages.

Lectures

• Introduction and course outline [slides]
• Lecture 1: Of expressions and commands: the semantics of an imperative language [slides] [Coq module IMP]
• Lecture 2: Traduttore, traditore: formal verification of a compiler [slides] [Coq module Compil]
• Lecture 3: Advanced compilation: optimizations, static analyses, and their verification [slides] [Coq module Optim]
• Lecture 4: Logics to reason about programs [slides] [Coq modules HoareLogic and SepLogic]
• Lecture 5: Abstract art: static analysis by abstract interpretation [slides] [Coq modules AbstrInterp and AbstrInterp2]
• Lecture 6: Eternity is long... Semantics for divergence: domain theory and coinductive approaches [slides] [Coq modules Divergence and Partiality]
• Lecture 7: Of functions and types: the semantics of a functional language [slides] [Coq module FUN]
• Lecture 8: Coq in Coq? Mechanizing the logic of a proof assistant [slides]
• Concluding remarks [slides]

Companion Coq development

Seminar talks

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

• Philip Wadler: Lambda, the ultimate teaching assistant (Agda version)
• Sylvie Boldo: L’arithmétique des ordinateurs et sa formalisation
• Alan Schmitt: Sémantique formelle de JavaScript
• Arthur Charguéraud: Logique de séparation en Coq : théorie et pratique
• David Pichardie: Interpréteurs abstraits mécanisés
• Derek Dreyer: Understanding and evolving the Rust language
• Xavier Leroy: What’s in a name? Représenter les variables et leurs liaisons