Functional programming has been revolutionized by our understanding of its connection to intuitionistic logic and type theory. In this tutorial we report on the progress of a long-term effort to provide a similar logical underpinning for message-passing concurrent programming. We show how substructural logics give rise to session types characterizing communication, and how substructural proofs can be interpreted as processes. Program examples will focus on recent progress on incorporating sharing of resources, such as shared queues, the classic dining philosophers problem, and a representation of the untyped asynchronous pi-calculus.

Frank Pfenning is Joseph F. Traub Professor and Head of the Computer Science Department at Carnegie Mellon University. He obtained his PhD in Mathematics at Carnegie Mellon University in 1987. He served as trustee and president of CADE, chaired several conferences and program committees including FoSSaCS 2013, LICS 2008, CADE 2007, and RTA 2006, and served on the editorial board of TCS, JAR, and JSC, and was named Fellow of the ACM in 2015. His current research interests include expressive type systems for functional, concurrent, and logic programming languages, computer security, logical frameworks, and automated deduction.