• Robbert Krebbers's avatar
    Various changes. · bb9d75d9
    Robbert Krebbers authored
    * Parametrize refinements with memories. This way, refinements imply typing,
      for example [w1 ⊑{Γ,f@m1↦m2} w2 : τ → (Γ,m1) ⊢ w1 : τ]. This relieves us from
      various hacks.
    * Use addresses instead of index/references pairs for lookup and alter
      operations on memories.
    * Prove various disjointness properties.
decidable.v 8.46 KB