Type-driven development of concurrent communicating systems

• Autorzy: Brady E.

Identyfikatory

DOI

10.7494/csci.2017.18.3.1413

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

dependent types; domain specific languages; verification; concurrency

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2017
• Tom: Vol. 18 (3)
• Strony: 219--240
• Opis fizyczny: Bibliogr. 24 poz., rys.

Twórcy

autor

Brady E.

• School of Computer Science, University of St Andrews

Bibliografia

• [1] 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.
• [2] Armstrong J.: Making Reliable Distributed Systems in the Presence of Software Errors. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden, 2003.
• [3] Bauer A., Pretnar M.: Programming with Algebraic Effects and Handlers, Journal of Logical and Algebraic Methods in Programming, vol. 84(1), pp. 108-123, 2015.
• [4] Brady E.: Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol. 23, pp. 552-593, 2013.
• [5] 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.
• [6] Brady E.: Resource-dependent Algebraic Effects. In: Hage J., McCarthy J. (eds.), Trends in Functional Programming (TFP '14), LNCS, vol. 8843, Springer, 2014.
• [7] 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, 2012.
• [8] Christiansen D.: Reect on Your Mistakes! Lightweight Domain-Specific Error Messages, Draft, 2014. http://www.itu.dk/people/drc/drafts/ error-reflection-submission.pdf.
• [9] 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, 2010.
• [10] Fournet C., Bhargavan K., Gordon A.D.: Cryptographic verication by typing for a sample protocol implementation. In: Aldini A., Gorrieri R., Foundations of Security Analysis and Design VI, 2010.
• [11] Gordon A., Jerey A.: Authenticity by Typing for Security Protocols, Journal of Computer Security, vol. 11(4), pp. 451-520, 2003.
• [12] Haller P., Odersky M.: Scala Actors: Unifying thread-based and event-based programming, Theoretical Computer Science, special issue: Distributed Computing Techniques, vol. 410(2-3), pp. 202-220, 2009.
• [13] Honda K., Yoshida N., Carbone M.: Multiparty asynchronous session types. In: ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, pp. 273-284, 2008.
• [14] Kammar O., Lindley S., Oury N.: Handlers in action. In: Proceedings of the 18th International Conference on Functional Programming (ICFP '13), ACM, 2013.
• [15] Krishnaswami N.R., Pradic P., Benton N.: Integrating Linear and Dependent Types. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 17-30, 2015.
• [16] Larson J.: Erlang for Concurrent Programming, Queue, vol. 6(5), pp. 18-23, 2008.
• [17] Lindley S., Morris J.G.: A semantics for propositions as sessions. In: European Symposium on Programming (ESOP '15), 2015.
• [18] McBride C.: I Got Plenty o Nuttin'. In: A List of Successes that can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, LNCS, Springer, 2016.
• [19] Peyton J.S.: Haskell 98 Language and Libraries - The Revised Report, 2002. http://www.haskell.org/.
• [20] Plotkin G., Pretnar M.: Handlers of Algebraic E_ects. In: ESOP 09: Proceedings of the 18th European Symposium on Programming Languages and Systems, pp. 80-94, 2009.
• [21] Steiner J.G., Neuman C., Schiller J.I.: Kerberos: An Authentication Service for Open Network Systems. In: USENIX, pp. 191-202, 1988.
• [22] The Idris Community: The Idris Tutorial, 2017. http://docs.idris-lang.org/ en/latest/tutorial/index.html.
• [23] de Vries E., Plasmeijer R., Abrahamson D.M.: Uniqueness Typing Simplified. In: Chitil O., Horvath Z., Zsok V. (eds.), Implementation and Application of Functional Languages (IFL '07), Lecture Notes in Computer Science, vol. 5083, pp. 201-218, Springer, 2007.
• [24] Wadler P.: Linear types can change the world! In: Broy M., Jones C. (eds.), IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, pp. 347-359, North Holland, 1990.

Uwagi

PL

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).