In the wake of the CompCert C compiler, the field of (mechanized) verified compilation has flourished over the past 15 years. A rich variety of languages, of degrees of optimization, of support for linking, of enforcement of security properties have notably been successfully investigated. Despite the diversity of these works, a powerful duo is (almost) always at their core: propositional, operational small step semantics to model the languages, and elementary (backward) simulation diagrams coinductively stitched together to prove the correctness of program transformations.

In this talk, I will defend the position that alternative semantics approaches are mature enough to be mechanically viable, at scale, for the purpose of compiler verification. More specifically, I will argue in favor of the use of Interaction Trees as a tool to define the semantics of languages as executable definitional interpreters. Interaction trees (itrees) is a rich Coq library that draws from a well established literature in semantics, implementing in a coinductive fashion ideas from the freer monad, iteration theory, and algebraic effects. The resulting semantics offer compositionality, modularity, and executability.

The benefits of these properties are quite commonly understood. The impact this style of semantics has over the proof method used to conduct a refinement proof might be less commonly though of. We will see how in lieu of traditional simulation diagrams, we build a relational and termination sensitive program logic allowing for a combination of asymmetric symbolic stepping and compositional relational reasoning.

Finally, I will overview a strong piece of evidence that this approach goes beyond toy examples. I will present the complete redesign of Vellvm, a project aiming at the formalization in Coq of part of the LLVM compiling infrastructure. Verified IR (VIR), a major sequential subset of LLVM IR whose semantics has been crafted using itrees, will illustrate the semantics side of our story. Our verified front-end from Helix, a Coq formalization of the SPIRAL infrastructure, down to VIR, whose proof follows this equational style, will stand as a testament to this alternate proof method.