First-order Hybrid Separation Logic
摘要
The basic set-theoretic interpretation of the separating connectives of first-order separation logic allows for an effective, sound and complete axiomatization in a hybrid extension.