TY - JOUR AU - Brady, Edwin Charles PY - 2017/07/07 Y2 - 2024/03/29 TI - Type-driven Development of Concurrent Communicating Systems JF - Computer Science JA - csci VL - 18 IS - 3 SE - Articles DO - 10.7494/csci.2017.18.3.1413 UR - https://journals.agh.edu.pl/csci/article/view/1413 SP - AB - Modern software systems rely on communication, for example mobile applcations communicating with a central server, distributed systems coordinaing a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent prgrams is hard, since we must reason about each process and the order in which communication might happen between processes. In this paper, I describe a type-driven approach to implementing communicating concurrent programs, using the dependently typed programming language Idris. I show how the type system can be used to describe resource access protocols (such as controlling access to a file handle) and verify that programs correctly follow those prtools. Finally, I show how to use the type system to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol. ER -