Stuttering for Free - A New Approach to Simulation Proofs

Explore a groundbreaking 17-minute video presentation from OOPSLA2 2023 that introduces FreeSim, a novel simulation technique for proving behavioral refinements between transition systems. Delve into the limitations of traditional stuttering simulations and discover how FreeSim overcomes these constraints by allowing for asynchronous progress. Learn about the technique's implementation in Coq and its practical applications, including simplifying CompCert's meta-theory and enhancing the ITrees library with dual non-determinism. Gain insights from the research team's findings and access supplementary materials, including the full article and artifact archive. Ideal for computer scientists, formal verification experts, and those interested in advanced simulation methods in programming language theory.

[OOPSLA23] Stuttering for Free