No.050 Software Contracts for Communication, Monitoring, and Security

Deadlock freedom is for concurrent programs what progress is for sequential ones: it indicates the absence of stable (i.e., irreducible) states in which some pending operations cannot be completed. In the particular case of communicating processes, operations are inputs and outputs on channels and deadlocks may be caused by mutual dependencies between communications. In this talk we see how to define an effect system ensuring deadlock freedom of higher-order programs and discuss some of its properties.