Protocol engineering for communicating actors | Laura Bocchi & Laura Voinea | Code Mesh V 2020

This video was recorded at Code Mesh V 2020 - Protocol engineering for communicating actors | Laura Bocchi & Laura Voinea ABSTRACT In systems of communicating processes or actors, data types can be used to discipline the sorts of sent and received messages. Session types, in addition, can describe specific causalities and patterns among different send/receive actions (like application-level protocols). I will give an overview on recent and ongoing research about writing “good protocols” using session types and session types to yield correct implementations. I will then focus on modular composition of protocols. Real-world communication protocols are often built out of simpler protocols that cater for some specific functionality (e.g., banking, authentication) or operate at different levels of abstraction (e.g., HTTP, POP). However much of the work used for program verification (e.g., session types) treat protocols as monolithic units. I will show an