Type-directed concurrency

Abstract. We introduce a novel way to integrate functional and con-current programming based on intuitionistic linear logic. The functional core arises from interpreting proof reduction as computation. The concur-rent core arises from interpreting proof search as computation. The two are tightly integrated via a monad that permits both sides to share the same logical meaning for the linear connectives while preserving their dif-ferent computational paradigms. For example, concurrent computation synthesizes proofs which can be evaluated as functional programs. We illustrate our design with some small examples, including an encoding of the pi-calculus.