On Tuesday, October 25th, Professor Luís Caires spoke with the Carnegie Mellon University community during the Principles of Programming Group (PoP) Seminar. The session named “Concurrent Programming with Sessions and Shared State, in Linear Logic” was focused on stateful programming involving sharing and concurrency as is common place in modern software development, and the challenges of getting complex concurrent code right, even for skilled developers. The speakers introduced 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 was a presentation of a suite of challenging code examples, with type-checker and interpreter implementation, that illustrate the expressiveness and some programming techniques for our language.
Luís Caires is a Scientific Director of the CMU Portugal Program, Full Professor of Computer Science at the Department of Informatics, NOVA University Lisbon, and Director of the NOVA Laboratory for Computer Science and Informatics. Caires visited Carnegie Mellon University October 24th – 27th, 2022 to meet with organizers from across the University, including the Project Olympus, the Center for Technology Transfer and Enterprise Creation (CTTEC), Professors and Researchers of the Computer Science Department and the Software and Societal Systems Department.
The Carnegie Mellon Portugal Program strongly supports the mobility of Portuguese academics to be hosted at Carnegie Mellon University to work in research and education, thus building international knowledge networks that allow extended and substantial immersion in world-class learning, teaching, and research.
The Principles of Programming Group (PoP) at Carnegie Mellon aims to understand, develop, and demonstrate the principles, processes, and supporting technologies for the construction of computing systems. A distinguishing characteristic of the PoP group is that it applies formal principles to problems of realistic scale and complexity, for example: automatic verification of large-scale commercial hardware systems; implementation of high-speed network communication software in the ML language; application of type-theoretic principles in the construction of realistic compilers.
