“Magic wand” is the somewhat whimsical name for the intuitionistic implication operator “—∗” used in Separation logic and its generalization Permission logic.
I get the impression that magic wands were largely ignored because use of magic wands hit decidability problems. Some more recent papers that changed that are: schwerhoff:ecoop:2015, blom:ijsttt:2015. They get round the decidability problems by introducing witnesses for magic wands.
Magic wands are useful for modelling partial data structures such as all the parts of a tree from the root down except for the bit that is currently being processed.
Magic wands are also used to model borrow semantics in the Rust language by astrauskas:oopsla:2019.
Notes related to Magic wand
Papers related to Magic wand
- Witnessing the elimination of magic wands [blom:ijsttt:2015]
- The ramifications of sharing in data structures [hobor:popl:2013]
- Verifying event-driven programs using ramified frame properties [krishnaswami:tldi:2010]
- Viper: A verification infrastructure for permission-based reasoning [muller:vmcai:2016]
- Lightweight support for magic wands in an automatic verifier [schwerhoff:ecoop:2015]
- Local reasoning about while-loops [tuerk:vstte:2010]