Scaling Up Mechanized Proof Automation for Small-step Semantics
Sandrine Blazy, Alain Delaët, Denis Merigoux · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
Verifying the correctness of a program using an interactive proof assistant involves first defining in the proof assistant the semantics of the programming language used to write the program. Once mechanized, the semantics of the programming language serves as the basis for the whole proof development, as it is referred by all subsequent theorems. Traditionally, the semantic judgments are mechanized using recursive inductive predicates, matching the pen-and-paper inference rules of operational semantics. However, the shape of these judgments may make proof engineering and maintenance tedious, requiring complex proof automation frameworks.In this paper, we highlight a different style of writing and mechanizing semantics, based on continuations. We show that continuation-based small-step semantics interacts better with basic proof automation tactics than the traditional operational style, and as such allows for scaling up more efficiently the mechanized proof development. After detailing the inner workings of the interactions between the semantic style and proof automation of common theorems, we perform a case study for the medium-sized Catala domain-specific programming language. All of our examples and case studies are mechanized using the Rocq proof assistant, and our development is available as a supplementary material.