Certified Absence of Dangling Pointers in a Language with Explicit Deallocation