Locks are a classic data structure for concurrent programming. We introduce a type system to ensure that names of the asynchronous pi-calculus are used as locks. Our calculus also features a construct to deallocate a lock once we know that it will never be acquired again. Typability guarantees two properties: deadlock-freedom, that is, no acquire operation on a lock waits forever; and leak-freedom, that is, all locks are eventually deallocated. We leverage the simplicity of our typing discipline to study the induced typed behavioural equivalence. After defining barbed equivalence, we introduce a sound labelled bisimulation, which makes it possible to establish equivalence between programs that manipulate and deallocate locks.

翻译：锁是并发编程中一种经典的数据结构。我们引入了一个类型系统，以确保异步π-演算中的名称被用作锁。我们的演算还包含一个构造，用于在确定锁永远不会再被获取时将其释放。可类型化性保证了两个性质：无死锁，即对锁的获取操作永远不会无限等待；以及无泄漏，即所有锁最终都会被释放。我们利用类型规则的简洁性来研究由此诱导的类型化行为等价性。在定义了柱状等价性后，我们引入了一种可靠的标记互模拟，这使得能够建立对操作和释放锁的程序之间的等价性。