- Tytuł:
- Type-driven development of concurrent communicating systems
- Autorzy:
- Brady, E.
- Powiązania:
- https://bibliotekanauki.pl/articles/305793.pdf
- Data publikacji:
- 2017
- Wydawca:
- Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
- Tematy:
-
dependent types
domain specific languages
verification
concurrency - Opis:
- 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.
- Źródło:
-
Computer Science; 2017, 18 (3); 219-240
1508-2806
2300-7036 - Pojawia się w:
- Computer Science
- Dostawca treści:
- Biblioteka Nauki
Artykuł