Abstract
As software tends to be increasingly concurrent, the paradigm ofmessage passing is becoming more prominent in computing. The language Erlang offers an intuitive and industry-testedimplementation of process-oriented programming, combining pattern-matching with message mailboxes, resulting in concise, elegant programs. However, it lacks a successful static verification mechanism that ensures safety and determinism of communications with respect to well-defined specifications. We present a session typing system for a featherweight Erlang calculus that encompasses the main communication abilities of the language. In this system, structured types are used to govern the interaction of Erlang processes, ensuring that their behaviour is safe with respect to a defined protocol. The expected properties of subject reduction and type safety are established.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amadio, R.M., Boudol, G., Lhoussaine, C.: On message deliverability and non-uniform receptivity. Fundam. Inf. 53, 105–129 (2002)
Armstrong, J., Virding, R., Wikström, C., Williams, M.: Concurrent Programming in Erlang, 2nd edn. Prentice-Hall, Englewood Cliffs (1996)
Business process execution language for web services, http://public.dhe.ibm.com/software/dw/specs/ws-bpel/ws-bpel.pdf
Carlsson, R.: An introduction to Core Erlang. In: PLI 2001 Erlang Workshop (2001)
Christakis, M., Sagonas, K.: Detection of asynchronous message passing errors using static analysis. In: Rocha, R., Launchbury, J. (eds.) PADL 2011. LNCS, vol. 6539, pp. 5–18. Springer, Heidelberg (2011)
Gay, S.J., Hole, M.J.: Subtyping for session types in the pi calculus. Acta Informatica 42(2/3), 191–225 (2005)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998), http://www.di.fc.ul.pt/~vv/papers/honda.vasconcelos.kubo_language-primitives.pdf
Hu, R., Yoshida, N., Honda, K.: Session-based distributed programming in java. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 516–541. Springer, Heidelberg (2008)
Lindahl, T., Sagonas, K.: Practical type inference based on success typings. In: 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP 2006, pp. 167–178. ACM, New York (2006)
Viroli, M.: Towards a formal foundation to orchestration languages. Electronic Notes in Theoretical Computer Science 105, 51–71 (2004); Proceedings of the First International Workshop on Web Services and Formal Methods (WSFM 2004)
Walker, D.: Substructural Type Systems. In: Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)
Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. In: 1st International Workshop on Security and Rewriting Techniques. ENTCS, vol. 171(4), pp. 73–93. Elsevier, Amsterdam (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 IFIP International Federation for Information Processing
About this paper
Cite this paper
Mostrous, D., Vasconcelos, V.T. (2011). Session Typing for a Featherweight Erlang. In: De Meuter, W., Roman, GC. (eds) Coordination Models and Languages. COORDINATION 2011. Lecture Notes in Computer Science, vol 6721. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21464-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-21464-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21463-9
Online ISBN: 978-3-642-21464-6
eBook Packages: Computer ScienceComputer Science (R0)