François Pottier: Verifying a hash table and its iterators in higher-order separation logic. CPP 2017: 3-16