Type-driven Development of Concurrent Communicating Systems
DOI:
https://doi.org/10.7494/csci.2017.18.3.1413Abstract
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.Downloads
References
Aldrich J., Sunshine J., Saini D., Sparks Z.: Typestate-oriented programming. In: Proceedings of the 24th ACM SIGPLAN conference on Object Oriented Programming Systems Languages and Applications, pp. 1015—-1012. 2009.
Armstrong J.: Making Reliable Distributed Systems in the Presence of Software Errors. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden, 2003.
Bauer A., Pretnar M.: Programming with Algebraic Effects and Handlers, 2012.
Brady E.: Idris, a general-purpose dependently typed programming language: Design and implementation. In: Journal of Functional Programming, vol. 23, pp. 552–593, 2013.
Brady E.: Programming and Reasoning with Algebraic Effects and Dependent Types. In: ICFP ’13: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. ACM, 2013.
Brady E.: Resource-dependent Algebraic Effects. In: J. Hage, J. McCarthy, eds., Trends in Functional Programming (TFP ’14), LNCS, vol. 8843. Springer, 2014.
Brown C., Hammond K., Danelutto M., Kilpatrick P.: A Language-independent Parallel Refactoring Framework. In: Proceedings of the Fifth Workshop on Refactoring Tools, WRT ’12, pp. 54–58. ACM, New York, NY, USA, 2012.
Christiansen D.: Reflect on Your Mistakes! Lightweight Domain-Specific Error Messages, 2014. URL http://www.itu.dk/people/drc/drafts/error-reflection-submission.pdf. Draft.
Danielsson N.A.: Total Parser Combinators. In: ICFP ’10: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, pp. 285–296. ACM, New York, NY, USA, 2010.
Fournet C., Bhargavan K., Gordon A.D.: Cryptographic verification by typing for a sample protocol implementation. In: Foundations of security analysis and design VI. 2010.
Gordon A., Jeffrey A.: Authenticity by Typing for Security Protocols. In: Journal of computer security, vol. 11(4), pp. 451–520, 2003.
Haller P., Odersky M.: Scala Actors: Unifying thread-based and event-based programming. In: Theoretical Computer Science, vol. 410(23), pp. 202 – 220, 2009. Distributed Computing Techniques.
Honda K., Yoshida N., Carbone M.: Multiparty asynchronous session types. In: ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, pp. 273—-284. 2008.
Kammar O., Lindley S., Oury N.: Handlers in action. In: Proceedings of the 18th International Conference on Functional Programming (ICFP ’13). ACM, 2013.
Krishnaswami N.R., Pradic P., Benton N.: Integrating Linear and Dependent Types. In: Principles of Programming Languages (POPL). 2015.
Larson J.: Erlang for Concurrent Programming. In: Queue, vol. 6(5), pp. 18–23, 2008. ISSN 1542-7730.
Lindley S., Morris J.G.: A semantics for propositions as sessions. In: European Symposium on Programming (ESOP ’15). 2015.
Peyton Jones S., et al.: Haskell 98 Language and Libraries — The Revised Report. Available from http://www.haskell.org/, 2002.
Plotkin G., Pretnar M.: Handlers of Algebraic Effects. In: ESOP 09: Proceedings of the 18th European Symposium on Programming Languages and Systems, pp. 80–94. 2009.
Steiner J.G., Neuman C., Schiller J.I.: Kerberos: An Authentication Service for Open Network Systems. In: USENIX, pp. 191–202. 1988.
The Idris Community: Programming in Idris : a tutorial, 2015. URL http: //idris-lang.org/tutorial.
de Vries E., Plasmeijer R., Abrahamson D.M.: Uniqueness Typing Simplified. In: O. Chitil, Z. Horváth, V. Zsók, eds., Implementation and Application of Functional Languages (IFL ’07), Lecture Notes in Computer Science, vol. 5083, pp. 201–218. Springer, 2007.
Wadler P.: Linear types can change the world! In: M. Broy, C. Jones, eds., IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, pp. 347–359. North Holland, 1990.
Downloads
Published
How to Cite
Issue
Section
