PoP Seminar Talk

Concurrent Programming with Sessions and Shared State, in Linear Logic

Luis Caires, Professor of Science and Methodology of Programming at Departamento of Computer Science and Engineering, Técnico Lisboa
Tuesday, 25 October, 2022; 3:30pm
NSH 3305
Host: Frank Pfenning

Abstract

Stateful programming involving sharing and concurrency is common place in modern software development, but getting complex concurrent code right can still be quite challenging, even for skilled developers. In this talk, we introduce CLASS a typed core programming language for higher-order concurrent programming, for which static typing ensures absence of a broad class of “dynamic bugs”: well-typed programs never deadlock, do not leak memory, and always terminate. These properties result from CLASS foundations, based on a conservative extension of Linear Logic with shareable affine state, via a propositions-as-types interpretation of proofs as session processes. The main part of the talk will be a presentation of a suite of challenging code examples, with our type-checker and interpreter implementation, that illustrate the expressiveness and some programming techniques for our language.

Bio

Luís Caires is Full Professor of Computer Science at the Department of Informatics, NOVA University Lisbon, and Director of the NOVA Laboratory for Computer Science and Informatics. His research focuses on programming languages and models, logics and types for concurrency, communication and security. He is an elected member of IFIP WG.2.2, “Formal Description of Programming Concepts” (est. 1964), is chair of the steering committee of ESOP, and served as PC chair of ESOP 2019, Forte 2018 and Concur 2007. He is Scientific Director of the CMU|Portugal Program since 2008 and was a board member of Informatics Europe. (http://ctp.di.fct.unl.pt/~lcaires/)