Based on the cubical-mini and guarded-cm libraries.
References:
- Bertot, [2007] "Theorem proving support in programming language semantics"
- Bertot, [2008] "Structural abstract interpretation, A formal study using Coq"
- https://github.com/coq-community/semantics
- Nipkow, [2012] "Abstract Interpretation of Annotated Commands"
- Nipkow, Klein, [2023] "Concrete Semantics with Isabelle/HOL" (chapter 13)