Logical Pinning

Coq formalization of logical pinning for container-internal pointers.

Coq formalization of logical pinning for container-internal (interior) pointers. Covers core libraries and case studies for linked lists and binary trees. Provides automated (make) and manual build paths with explicit dependencies. Accompanies a published research paper.