RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.
Title: Fair termination of the binary session
Speaker: Luca Padovani (School of Science and Technology, University of Camerino. )
When: Tuesday, June 18, 2024, 14h
Where: FCUL, room C6.3.27
Abstract: Sessions are private communication channels that enable the compositional static analysis of distributed systems. Well-typed sessions enjoy a number of desirable properties, such as communication safety, protocol fidelity and deadlock freedom. In this talk we’ll see a session type system aimed at ensuring lock freedom, namely that every pending input/output action within a session is eventually performed. The type system is based on the observation that lock freedom is implied by the conjunction of deadlock freedom and of fair termination, the latter being a termination property that holds under a given fairness assumption: in principle, a fairly terminating process may have an infinite execution; in practice, all of its fair (i.e. “realistic”) executions are finite. We’ll focus on one particular formulation of the type system that uses the correspondence between session types and linear logic propositions with fixed points.
Bio: I am an associate professor of Computer Science at the Computer Science Division of the School of Science and Technology of the University of Camerino. My research interests include programming languages, type systems, concurrency theory and formal software verification.
This presentation is supported by FCT through project SafeSessions, ref. PTDC/CCI-CIF/6453/2020.