Skip to content

Research at St Andrews

Type driven development of concurrent communicating systems

Research output: Contribution to journalArticle


School/Research organisations


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
Issue number3
StatePublished - 7 Jul 2017

    Research areas

  • Dependent types, Domain specific languages, Verification, Concurrency

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Sequential decision problems, dependent types and generic solutions

    Botta, N., Jansson, P., Ionescu, C., Christiansen, D. & Brady, E. C. 17 Mar 2017 In : Logical Methods in Computer Science. 13, 1, 23 p., 7

    Research output: Contribution to journalArticle

  2. Type-driven development with Idris

    Brady, E. C. Mar 2017 Shelter Island: Manning Publications Co.480 p.

    Research output: Book/ReportBook

  3. Automatically proving equivalence by type-safe reflection

    Slama, F. & Brady, E. C. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 40-55 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Elaborator reflection: extending Idris in Idris

    Christiansen, D. & Brady, E. C. 4 Sep 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. New York: ACM, p. 284-297

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. The Idris Programming Language: Implementing Embedded Domain Specific Languages with Dependent Types

    Brady, E. C. 2015 CEFP 2013. Springer, Vol. 8606

    Research output: Chapter in Book/Report/Conference proceedingChapter

Related by journal

  1. Computer Science (Journal)

    Kirby, G. N. C. (Reviewer)
    Apr 2013

    Activity: Publication peer-review and editorial workPeer review of manuscripts

ID: 174257645