Foundations of session types

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Foundations of session types

Full text

Pdf (515 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Coimbra, Portugal

SESSION: Concurrency table of contents

Pages 219-230

Year of Publication: 2009

ISBN:978-1-60558-568-0

Authors

Giuseppe Castagna	Université Denis Diderot, Paris, France
Mariangiola Dezani-Ciancaglini	Università degli Studi di Torino, Torino, Italy
Elena Giachino	Università degli Studi di Torino, Torino, Italy
Luca Padovani	Università degli Studi di Urbino, Urbino, Italy

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 13, Downloads (12 Months): 13, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599437 What is a DOI?

ABSTRACT

We present a streamlined theory of session types based on a simple yet general and expressive formalism whose main eatures are semantically characterized and where each design choice is semantically justified. We formally define the semantics of session types and use it to devise the subsessioning relation. We give a coinductive characterization of subsessioning and describe algorithms to decide all the key relations defined in the article. We demonstrate the generality and expressive power of our framework by providing a session-based type system for a pi-calculus variant that does not rely on any specialized construct for session-based communication. The type system is shown to guarantee absence of communication errors and global progress.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	L. Acciai and M. Boreale. A type system for client progress in a service-oriented calculus. In Concurrency, Graphs and Models, volume 5065 of LNCS, pages 642--658. Springer, 2008.
	2	M. Boreale, R. Bruni, R. De Nicola, and M. Loreti. Sessions and pipelines for structured service programming. In FMOODS'08, volume 5051 of LNCS, pages 19--38. Springer, 2008.
	3	L. Caires and H.T. Vieira. Conversation types. In ESOP'09, LNCS 5502, pages 285--300. Springer, 2009.
	4	G. Castagna, R. De Nicola, and D. Varacca. Semantic subtyping for the π-calculus. Theor. Comput. Sci., 398(1-3):217--242, 2008.
	5	G. Castagna and A. Frisch. A gentle introduction to semantic subtyping. In PPDP '05, pages 198--208, ACM Press (full version) and ICALP '05, LNCS n. 3580, pages 30--34, Springer (summary), 2005. Joint ICALP-PPDP keynote talk.
	6	G. Castagna, N. Gesbert, and L. Padovani. A theory of contracts for web services. ACM Transactions on Programming Languages and Systems, 2009. Extended version of the article in POPL '08. To appear.
	7	I. Castellani and M. Hennessy. Testing theories for asynchronous languages. In FST&TCS '98, volume 1350 of LNCS, pages 90--101. Springer, 1998.
	8	R. De Nicola and M. Hennessy. Testing equivalences for processes. Theor. Comput. Sci, 34:83--133, 1984.
	9	R. De Nicola and M. Hennessy. CCS without τ's. In TAPSOFT/CAAP'87, volume 249 of LNCS, pages 138--152. Springer, 1987.
	10	M. Dezani-Ciancaglini, U. de'Liguoro, and N. Yoshida. On progress for structured communications. In TGC'07, volume 4912 of LNCS, pages 257--275. Springer, 2008.
	11	M. Dezani-Ciancaglini, E. Giachino, S. Drossopoulou, and N. Yoshida. Bounded session types for object-oriented languages. In FMCO'06, volume 4709 of LNCS, pages 207--245. Springer, 2007.
	12	M. Dezani-Ciancaglini, N. Yoshida, A. Ahern, and S. Drossopoulou. A distributed object oriented language with session types. In TGC'05, volume 3705 of LNCS, pages 299--318. Springer, 2005.
	13	A. Frisch. Regular tree language recognition with static information. In IFIP TCS'04, pages 661--674. Kluwer, 2004.
	14	A. Frisch, G. Castagna, and V. Benzaken. Semantic subtyping: dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM, 55(4):1--64, 2008.
	15	S. Gay. Bounded polymorphism in session types. MSCS, 18(5):895--930, 2008.
	16	S. Gay and M. Hole. Subtyping for session types in the pi-calculus. Acta Informatica, 42(2/3):191--225, 2005.
	17	S. Gay and V.T. Vasconcelos. Linear type theory for asynchronous session types. Available online, 2008.
	18	M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes with value-passing. In ICALP'90, volume 443 of LNCS. Springer, 1990.
	19	K. Honda. Types for dyadic interaction. In CONCUR'93, volume 715 of LNCS, pages 509--523. Springer, 1993.
	20	K. Honda, D. Mostrous, and N. Yoshida. Global principal typing in partially commutative asynchronous sessions. In ESOP'09, LNCS 5502, pages 316--332. Springer, 2009.
	21	K. Honda, V.T. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP'98, volume 1381 of LNCS. Springer, 1998.
	22	K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In POPL'08, pages 273--284. ACM, 2008.
	23	A. Igarashi and N. Kobayashi. A generic type system for the pi-calculus. Theor. Comput. Sci, 311(1-3):121--163, 2004.
	24	N. Kobayashi. Type systems for concurrent programs. In FMC'03, LNCS 2757. Springer, 2003.
	25	N. Kobayashi. Type systems for concurrent programs. Extended version of [24], Tohoku University, 2007.
	26	L.G. Mezzina. How to infer finite session types in a calculus of services and sessions. In COORDINATION'08, volume 5052 of LNCS, pages 216--231. Springer, 2008.
	27	R. Milner, J. Parrow, and D. Walker. Modal logics for mobile processes. Theor. Comput. Sci., 114(1):149--171, 1993.
	28	B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Math. Struct. in Comp. Science, 6(5):409--454, 1996.
	29	A. Vallecillo, V.T. Vasconcelos, and A. Ravara. Typing the behavior of objects and components using session types. In FOCLASA'02, volume 68(3) of ENTCS, pages 439--456. Elsevier, 2002.
	30	V. T. Vasconcelos. Fundamentals of session types. In SFM'09, volume 5569 of LNCS, pages 158--186. Springer, 2009.
	31	N. Yoshida and V. T. Vasconcelos. Language primitives and type disciplines for structured communication--based programming revisited. In SecRet'06, volume 171(4) of ENTCS, pages 73---93. Elsevier, 2007.