Abstract
In 2010, Luis Caires and Frank Pfenning developed a propositions-as-types correspondence for concurrent computation, along the lines of the standard Curry-Howard correspondence between simply typed lambda-calculus and intuitionistic logic. Their correspondence connects a form of linear logic, and the pi-calculus equipped with session types (type-theoretic formulations of communication protocols). As well as guaranteeing correct communication in the sense that messages follow the specified protocol, the type system guarantees deadlock-free execution of concurrent processes by imposing a rather severe prohibition on cyclic interconnections. Earlier work by Naoki Kobayashi developed a more liberal type system for deadlock-freedom in the pi-calculus, which allows the formation of cyclic interconnections if there is no actual cyclic dependency between communication operations. Kobayashi's system was developed from computational intuitions, but it is natural to wonder whether it can be given a logical foundation. In this talk we explore a reformulation of Kobayashi's deadlock-freedom proof as a cut-elimination result, and assess its consequences on the computational and logical sides of the Curry-Howard correspondence.