Iron: Managing obligations in higher-order concurrent separation logic

Precise management of resources and the obligations they impose, such as the need to dispose of memory, close locks, and release file handles, is hardÐespecially in the presence of concurrency, when some resources are shared, and different threads operate on them concurrently. We present Iron, a novel higher-order concurrent<br/>separation logic...