UNIVERSITY OF HERTFORDSHIRE COMPUTER SCIENCE RESEARCH COLLOQUIUM presents "A toolchain for safe development of distributed software" Dr. Raymond Hu (School of Physics, Engineering, and Computer Science, University of Hertfordshire) 26 May 2021 (Wednesday) 13:00 -14:00 Everyone is Welcome to Attend (over Zoom) Abstract: Distributed systems and applications -- built of geographically separate components that communicate via message passing -- are fundamental to our modern computing and social infrastructures. This talk will demonstrate practical tools for safe specification and programming of distributed software. By analogy to the data type safety properties guaranteed by many programming languages, such as interface compliance and compatibility of data and operations, the aim is to develop techniques and tools for safety in the distributed software setting -- protocol compliance and compatibility of component interactions. Specifically, we will demonstrate a framework that combines refinement types and multiparty session types. Refinement types is a technique that allows data types to be refined more precisely with a logical predicate, e.g., `n: int{n >= 0}` describes a variable `n` that ranges over the non-negative integers. Multiparty session types is a technique that describes message passing interactions as types, e.g., `Alex -> Bobbie: int` says Alex sends Bobbie an integer. Our framework combines them to offer a practical toolchain for safe distributed programming in the F* language supported by Microsoft. This is joint work with Fangyi Zhou, Francisco Ferreira, Rumyana Neykova and Nobuko Yoshida, published at OOPSLA '20. --------------------------------------------------- Hertfordshire Computer Science Research Colloquium http://cs-colloq.cs.herts.ac.uk