Type driven development of concurrent communicating systems

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)
3 Downloads (Pure)

Abstract

Modern software systems rely on communication, for example mobile applications communicating with a central server, distributed systems coordinating a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent programs 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 protocols. 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.
Original languageEnglish
Article number1413
Number of pages22
JournalComputer Science
Volume18
Issue number3
DOIs
Publication statusPublished - 7 Jul 2017

Keywords

  • Dependent types
  • Domain specific languages
  • Verification
  • Concurrency

Fingerprint

Dive into the research topics of 'Type driven development of concurrent communicating systems'. Together they form a unique fingerprint.

Cite this