David Knothe and Oliver Bringmann - Combining Big and Small-Step Semantics to Verify Loop Optimizations
See the paper at https://arxiv.org/abs/2602.19868 : See Patrick Cousot & Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2--3):103--179, 1992 , and also Coinductive big-step operational semantics by Xavier Leroy and Hervé Grall and Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment by David M. Kahn, Jan Hoffmann and Runming Li. Starts at around 3 hours . See also Patrick Bahr - Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations . Subscribe to ACM SIGPLAN .