Forked from
Iris / stdpp
Source project has a limited visibility.
-
Robbert Krebbers authored
The refinement relation on addresses allows union references to be refined: (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2 The result is that frozen values are below their unfrozen variant, which made it possible to prove that constant propagation (see constant_propagation.v) can be performed on the level of the memory model.
Robbert Krebbers authoredThe refinement relation on addresses allows union references to be refined: (β2 → β1) → RUnion i s β1 ⊆ RUnion i s β2 The result is that frozen values are below their unfrozen variant, which made it possible to prove that constant propagation (see constant_propagation.v) can be performed on the level of the memory model.
