- Tytuł:
- Type-driven development of concurrent communicating systems
- Autorzy:
- Brady, E.
- Tematy:
-
dependent types
domain specific languages
verification
concurrency - Pokaż więcej
- Wydawca:
- Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie. Wydawnictwo AGH
- Powiązania:
- https://bibliotekanauki.pl/articles/305793.pdf Link otwiera się w nowym oknie
- 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.
- Dostawca treści:
- Biblioteka Nauki
Artykuł