survey

Open access

Foundations of Session Types and Behavioural Contracts

Authors:

Hans Hüttel,

Ivan Lanese,

Vasco T. Vasconcelos,

Luís Caires,

Marco Carbone,

Pierre-Malo Deniélou,

Gianluigi ZavattaroAuthors Info & Claims

ACM Computing Surveys (CSUR), Volume 49, Issue 1

Article No.: 3, Pages 1 - 36

https://doi.org/10.1145/2873052

Published: 05 April 2016 Publication History

PDF eReader

Abstract

Behavioural type systems, usually associated to concurrent or distributed computations, encompass concepts such as interfaces, communication protocols, and contracts, in addition to the traditional input/output operations. The behavioural type of a software component specifies its expected patterns of interaction using expressive type languages, so types can be used to determine automatically whether the component interacts correctly with other components. Two related important notions of behavioural types are those of session types and behavioural contracts. This article surveys the main accomplishments of the last 20 years within these two approaches.

References

[1]

Martín Abadi and Luca Cardelli. 1996. A Theory of Objects. Springer, Berlin.

Google Scholar

[2]

Lucia Acciai and Michele Boreale. 2008. Responsiveness in process calculi. Theor. Comput. Sci. 409, 1 (2008), 59--93.

Digital Library

Google Scholar

[3]

Lucia Acciai and Michele Boreale. 2010. Spatial and behavioral types in the pi-calculus. Inform. Comput. 208, 10 (2010), 1118--1153.

Digital Library

Google Scholar

[4]

Lucia Acciai, Michele Boreale, and Gianluigi Zavattaro. 2010. On the relationship between spatial logics and behavioral simulations. In FOSSACS (LNCS), Vol. 6014. Springer, Berlin, 146--160.

Google Scholar

[5]

Pedro Baltazar, Luís Caires, Vasco Thudichum Vasconcelos, and Hugo Torres Vieira. 2012a. A type system for flexible role assignment in multiparty communicating systems. In TGC (LNCS), Vol. 8191. Springer, Berlin, 82--96.

Google Scholar

[6]

Pedro Baltazar, Dimitris Mostrous, and Vasco Thudichum Vasconcelos. 2012b. Linearly refined session types. In LINEARITY (EPTCS), Vol. 101. Open Publishing Association, Sydney, 38--49.

Google Scholar

[7]

Franco Barbanera and Ugo de’Liguoro. 2010. Two notions of sub-behaviour for session-based client/server systems. In PPDP. ACM, New York, NY, 155--164.

Google Scholar

[8]

Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. Intersection and union types: Syntax and semantics. Inform. Comput. 119, 2 (1995), 202--230.

Digital Library

Google Scholar

[9]

Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A filter lambda model and the completeness of type assignment. J. Symb. Log. 48, 4 (1983), 931--940.

Crossref

Google Scholar

[10]

Henk Barendregt, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus With Types. Cambridge University Press, Cambridge.

Digital Library

Google Scholar

[11]

Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari, and Roberto Zunino. 2008. Semantics-based design for secure web services. IEEE Trans. Software Eng. 34, 1 (2008), 33--49.

Digital Library

Google Scholar

[12]

Massimo Bartoletti, Julien Lange, Alceste Scalas, and Roberto Zunino. 2015. Choreographies in the wild. Sci. Comput. Program. 109 (2015), 36--60.

Digital Library

Google Scholar

[13]

Massimo Bartoletti, Alceste Scalas, Emilio Tuosto, and Roberto Zunino. 2013. Honesty by typing. In FMOODS/FORTE (LNCS), Vol. 7892. Springer, Berlin, 305--320.

Google Scholar

[14]

Massimo Bartoletti, Emilio Tuosto, and Roberto Zunino. 2012a. Contract-oriented computing in CO2. Sci. Ann. Comp. Sci. 22, 1 (2012), 5--60.

Google Scholar

[15]

Massimo Bartoletti, Emilio Tuosto, and Roberto Zunino. 2012b. On the realizability of contracts in dishonest systems. In COORDINATION (LNCS), Vol. 7274. Springer, Berlin, 245--260.

Google Scholar

[16]

Martin Berger, Kohei Honda, and Nobuko Yoshida. 2005. Genericity and the pi-calculus. Acta Inf. 42, 2--3 (2005), 83--141.

Crossref

Google Scholar

[17]

Giovanni Bernardi. 2013. Behavioural Equivalences for Web Services. Ph.D. Dissertation. Trinity College Dublin.

Google Scholar

[18]

Giovanni Bernardi and Matthew Hennessy. 2012. Modelling session types using contracts. In SAC. ACM, New York, NY, 1941--1946.

Digital Library

Google Scholar

[19]

Giovanni Bernardi and Matthew Hennessy. 2013. Compliance and testing preorders differ. In SEFM Workshops (LNCS), Vol. 8368. Springer, Berlin, 69--81.

Google Scholar

[20]

Giovanni Bernardi and Matthew Hennessy. 2014. Using higher-order contracts to model session types (extended abstract). In CONCUR (LNCS), Vol. 8704. Springer, Berlin, 387--401.

Google Scholar

[21]

Lorenzo Bettini, Sara Capecchi, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Betti Venneri. 2008. Session and union types for object oriented programming. In Concurrency, Graphs and Models (LNCS), Vol. 5065. Springer, Berlin, 659--680.

Google Scholar

[22]

Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A theory of design-by-contract for distributed multiparty interactions. In CONCUR (LNCS), Vol. 6269. Springer, Berlin, 162--176.

Google Scholar

[23]

Laura Bocchi, Julien Lange, and Emilio Tuosto. 2012. Three algorithms and a methodology for amending contracts for choreographies. Sci. Ann. Comp. Sci. 22, 1 (2012), 61--104.

Google Scholar

[24]

Eduardo Bonelli, Adriana B. Compagnoni, and Elsa L. Gunter. 2005. Typechecking safe process synchronization. In FGUC (ENTCS), Vol. 138. Elsevier, Amsterdam, 3--22.

Google Scholar

[25]

Michele Boreale, Roberto Bruni, Luís Caires, Rocco De Nicola, Ivan Lanese, Michele Loreti, Francisco Martins, Ugo Montanari, António Ravara, Davide Sangiorgi, Vasco Thudichum Vasconcelos, and Gianluigi Zavattaro. 2006. SCC: A service centered calculus. In WS-FM (LNCS), Vol. 4184. Springer, Berlin, 38--57.

Google Scholar

[26]

Michele Boreale, Roberto Bruni, Rocco De Nicola, and Michele Loreti. 2008. Sessions and pipelines for structured service programming. In FMOODS (LNCS), Vol. 5051. Springer, Berlin, 19--38.

Google Scholar

[27]

Gérard Boudol. 1997. Typing the use of resources in a concurrent calculus. In ASIAN (LNCS), Vol. 1345. Springer, Berlin, 239--253.

Google Scholar

[28]

Mario Bravetti and Gianluigi Zavattaro. 2007. Towards a unifying theory for choreography conformance and contract compliance. In Software Composition (LNCS), Vol. 4829. Springer, Berlin, 34--50.

Google Scholar

[29]

Mario Bravetti and Gianluigi Zavattaro. 2008a. Contract compliance and choreography conformance in the presence of message queues. In WS-FM (LNCS), Vol. 5387. Springer, Berlin, 37--54.

Google Scholar

[30]

Mario Bravetti and Gianluigi Zavattaro. 2008b. A foundational theory of contracts for multi-party service composition. Fundam. Inform. 89, 4 (2008), 451--478.

Digital Library

Google Scholar

[31]

Mario Bravetti and Gianluigi Zavattaro. 2009a. Contract-based discovery and composition of web services. In SFM (LNCS), Vol. 5569. Springer, Berlin, 261--295.

Google Scholar

[32]

Mario Bravetti and Gianluigi Zavattaro. 2009b. A theory of contracts for strong service compliance. Math. Struct. Comput. Sci. 19, 3 (2009), 601--638.

Digital Library

Google Scholar

[33]

Ed Brinksma, Giuseppe Scollo, and Chris Steenbergen. 1995. Lotos specifications, their implementations and their tests. In Conformance Testing Methodologies and Architectures for OSI Protocols. IEEE Computer Society, Washington, DC, 468--479.

Google Scholar

[34]

Antonio Brogi, Carlos Canal, and Ernesto Pimentel. 2004. Behavioural types and component adaptation. In AMAST (LNCS), Vol. 3116. Springer, Berlin, 42--56.

Google Scholar

[35]

Roberto Bruni and Leonardo Gaetano Mezzina. 2008. Types and deadlock freedom in a calculus of services, sessions and pipelines. In AMAST (LNCS), Vol. 5140. Springer, Berlin, 100--115.

Google Scholar

[36]

Tevfik Bultan and Xiang Fu. 2007. Specification of realizable service conversations using collaboration diagrams. In SOCA. IEEE Computer Society, Washington, DC, 122--132.

Google Scholar

[37]

Nadia Busi, Roberto Gorrieri, Claudio Guidi, Roberto Lucchi, and Gianluigi Zavattaro. 2005. Choreography and orchestration: A synergic approach for system design. In ICSOC (LNCS), Vol. 3826. Springer, Berlin, 228--240.

Google Scholar

[38]

Luís Caires. 2008. Spatial-behavioral types for concurrency and resource control in distributed systems. Theor. Comput. Sci. 402, 2--3 (2008), 120--141.

Digital Library

Google Scholar

[39]

Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. 2013. Behavioral polymorphism and parametricity in session-based communication. In ESOP (LNCS), Vol. 7792. Springer, Berlin, 330--349.

Google Scholar

[40]

Luís Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. In CONCUR (LNCS), Vol. 6269. Springer, Berlin, 222--236.

Google Scholar

[41]

Luís Caires, Frank Pfenning, and Bernardo Toninho. 2015. Linear logic propositions as session types. (unpublished).

Google Scholar

[42]

Luís Caires and João Costa Seco. 2013. The type discipline of behavioral separation. In POPL. ACM, New York, NY, 275--286.

Google Scholar

[43]

Luís Caires and Hugo Torres Vieira. 2010. Conversation types. Theor. Comput. Sci. 411, 51--52 (2010), 4399--4440.

Digital Library

Google Scholar

[44]

Sara Capecchi, Elena Giachino, and Nobuko Yoshida. 2010. Global escape in multiparty sessions. In FSTTCS (LIPIcs), Vol. 8. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 338--351.

Google Scholar

[45]

Marco Carbone. 2009. Session-based choreography with exceptions. In PLACES (ENTCS). Elsevier, Amsterdam, 35--55.

Google Scholar

[46]

Marco Carbone, Kohei Honda, and Nobuko Yoshida. 2008. Structured interactional exceptions in session types. In CONCUR (LNCS), Vol. 5201. Springer, Berlin, 402--417.

Google Scholar

[47]

Marco Carbone and Fabrizio Montesi. 2013. Deadlock-freedom-by-design: Multiparty asynchronous global programming. In POPL. ACM, New York, NY, 263--274.

Digital Library

Google Scholar

[48]

Samuele Carpineti, Giuseppe Castagna, Cosimo Laneve, and Luca Padovani. 2006. A formal account of contracts for web services. In WS-FM (LNCS), Vol. 4184. Springer, Berlin, 148--162.

Google Scholar

[49]

Cyril Carrez, Alessandro Fantechi, and Elie Najm. 2003. Behavioural contracts for a sound assembly of components. In FORTE (LNCS), Vol. 2767. Springer, Berlin, 111--126.

Google Scholar

[50]

Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. 2009a. Foundations of session types. In PPDP. ACM, Berlin, 219--230.

Google Scholar

[51]

Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, and Luca Padovani. 2012. On global types and multi-party sessions. Logical Methods Comput. Sci. 8, 1, Article 24, 45 pages.

Google Scholar

[52]

Giuseppe Castagna, Nils Gesbert, and Luca Padovani. 2009b. A theory of contracts for Web services. ACM Trans. Program. Lang. Syst. 31, 5, Article 19, 61 pages.

Digital Library

Google Scholar

[53]

Giuseppe Castagna and Luca Padovani. 2009. Contracts for mobile processes. In CONCUR (LNCS), Vol. 5710. Springer, Berlin, 211--228.

Google Scholar

[54]

Samir Chouali and Ahmed Hammad. 2011. Formal verification of components assembly based on SysML and interface automata. ISSE 7, 4 (2011), 265--274.

Google Scholar

[55]

Samir Chouali, Sebti Mouelhi, and Hassan Mountassir. 2010. Adapting component behaviours using interface automata. In EUROMICRO-SEAA. IEEE Computer Society, Washington, DC, 119--122.

Google Scholar

[56]

Rance Cleaveland and Matthew Hennessy. 1993. Testing equivalence as a bisimulation equivalence. Formal Asp. Comput. 5, 1 (1993), 1--20.

Digital Library

Google Scholar

[57]

Jean-Louis Colaço, Marc Pantel, Fabien Dagnat, and Patrick Sallé. 1999. Static safety analysis for non-uniform service availability in actors. In FMOODS (IFIP Conference Proceedings), Vol. 139. Kluwer, Amsterdam, 371--386.

Crossref

Google Scholar

[58]

Jean-Louis Colaço, Mark Pantel, and Patrick Sallé. 1997. A set-constraint-based analysis of actors. In FMOODS. Chapman & Hall, London, 1--16.

Google Scholar

[59]

Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. 2013. Inference of global progress properties for dynamically interleaved multiparty sessions. In COORDINATION (LNCS), Vol. 7890. Springer, Berlin, 45--59.

Google Scholar

[60]

Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2016. Global progress for dynamically interleaved multiparty sessions. Math. Struct. Comput. Sci. 26 (2016), 238--302.

Crossref

Google Scholar

[61]

Mario Coppo and Alberto Ferrari. 1993. Type inference, abstract interpretation and strictness analysis. Theor. Comput. Sci. 121, 1&2 (1993), 113--143.

Digital Library

Google Scholar

[62]

Luís Cruz-Filipe, Ivan Lanese, Francisco Martins, António Ravara, and Vasco Thudichum Vasconcelos. 2008. Behavioural theory at work: Program transformations in a service-centred calculus. In FMOODS (LNCS), Vol. 5051. Springer, Berlin, 59--77.

Google Scholar

[63]

Luís Cruz-Filipe, Ivan Lanese, Francisco Martins, António Ravara, and Vasco Thudichum Vasconcelos. 2014. The stream-based service-centered calculus: A foundation for service-oriented programming. Formal Aspects Comput. 26, 5 (2014), 865--918.

Crossref

Google Scholar

[64]

Ornela Dardha, Elena Giachino, and Davide Sangiorgi. 2012. Session types revisited. In PPDP. ACM, New York, NY, 139--150.

Google Scholar

[65]

Luca de Alfaro and Thomas A. Henzinger. 2001. Interface automata. In ESEC-FSE. ACM, New York, NY, 109--120.

Google Scholar

[66]

Rocco De Nicola and Matthew Hennessy. 1984. Testing equivalences for processes. Theor. Comput. Sci. 34 (1984), 83--133.

Crossref

Google Scholar

[67]

Robert DeLine and Manuel Fähndrich. 2004. Typestates for objects. In ECOOP (LNCS), Vol. 3086. Springer, Berlin, 465--490.

Google Scholar

[68]

Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. 2010. Termination in impure concurrent languages. In CONCUR (LNCS), Vol. 6269. Springer, Berlin, 328--342.

Google Scholar

[69]

Romain Demangeon and Kohei Honda. 2011. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR (LNCS), Vol. 6901. Springer, Berlin, 280--296.

Google Scholar

[70]

Pierre-Malo Deniélou and Nobuko Yoshida. 2011. Dynamic multirole session types. In POPL. ACM, 435--446.

Google Scholar

[71]

Pierre-Malo Deniélou and Nobuko Yoshida. 2013. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP (2) (LNCS), Vol. 7966. Springer, Berlin, 174--186.

Google Scholar

[72]

Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. 2012. Cut reduction in linear logic as asynchronous session-typed communication. In CSL (LIPIcs), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 228--242.

Google Scholar

[73]

Mariangiola Dezani-Ciancaglini, Ugo de’Liguoro, and Nobuko Yoshida. 2007. On progress for structured communications. In TGC (LNCS), Vol. 4912. Springer, Berlin, 257--275.

Google Scholar

[74]

Mariangiola Dezani-Ciancaglini, Elena Giachino, Sophia Drossopoulou, and Nobuko Yoshida. 2006. Bounded session types for object oriented languages. In FMCO (LNCS), Vol. 4709. Springer, Berlin, 207--245.

Google Scholar

[75]

Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. 2005. Compositional characterisations of lambda-terms using intersection types. Theor. Comput. Sci. 340, 3 (2005), 459--495.

Digital Library

Google Scholar

[76]

Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, Alexander Ahern, and Sophia Drossopoulou. 2005. L-doos: A distributed object-oriented language with session types. In TGC (LNCS), Vol. 3705. Springer, Berlin, 299--318.

Google Scholar

[77]

Joshua Dunfield. 2012. Elaborating intersection and union types. In ICFP. ACM, New York, NY, 17--28.

Google Scholar

[78]

Joshua Dunfield and Frank Pfenning. 2003. Type assignment for intersections and unions in call-by-value languages. In FoSSaCS (LNCS), Vol. 2620. Springer, Berlin, 250--266.

Google Scholar

[79]

Cédric Fournet, C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof. 2004. Stuck-free conformance. In CAV (LNCS), Vol. 3114. Springer, Berlin, 242--254.

Google Scholar

[80]

Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In PLDI. ACM, New York, NY, 268--277.

Google Scholar

[81]

Maxime Gamboni. 2010. Statically Proving Behavioural Properties in the π-Calculus via Dependency Analysis. Ph.D. Dissertation. Instituto Superior Técnico, Technical University of Lisbon.

Google Scholar

[82]

Maxime Gamboni and António Ravara. 2010. Responsive choice in mobile processes. In TGC (LNCS), Vol. 6084. Springer, Berlin, 135--152.

Google Scholar

[83]

Simon J. Gay. 2008. Bounded polymorphism in session types. Math. Struct. Comput. Sci. 18, 5 (2008), 895--930.

Crossref

Google Scholar

[84]

Simon J. Gay, Nils Gesbert, and António Ravara. 2014. Session types as generic process types. In EXPRESS/SOS (EPTCS), Vol. 160. 94--110.

Google Scholar

[85]

Simon J. Gay and Malcolm Hole. 1999. Types and subtypes for client-server interactions. In ESOP (LNCS), Vol. 1576. Springer, Berlin, 74--90.

Google Scholar

[86]

Simon J. Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. Acta Inf. 42, 2--3 (2005), 191--225.

Crossref

Google Scholar

[87]

Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear type theory for asynchronous session types. J. Funct. Program. 20, 1 (2010), 19--50.

Digital Library

Google Scholar

[88]

Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. 2010. Modular session types for distributed object-oriented programming. In POPL. ACM, New York, NY, 299--312.

Google Scholar

[89]

Jean-Yves Girard. 1987. Linear logic. Theor. Comput. Sci. 50 (1987), 1--102.

Digital Library

Google Scholar

[90]

Jean-Yves Girard and Yves Lafont. 1987. Linear logic and lazy computation. In TAPSOFT(2) (LNCS), Vol. 250. Springer, Berlin, 52--66.

Google Scholar

[91]

Marco Giunti. 2011. A type checking algorithm for qualified session types. In WWV (EPTCS), Vol. 61. Open Publishing Association, 96--114.

Google Scholar

[92]

Marco Giunti and Vasco Thudichum Vasconcelos. 2016. Linearity, session types and the Pi calculus. Math. Struct. Comput. Sci. 26 (2016), 206--237.

Crossref

Google Scholar

[93]

Andrew D. Gordon and Alan Jeffrey. 2003. Typing Correspondence Assertions for Communication Protocols. Theor. Comput Sci. 300, 1--3 (2003), 379--409.

Digital Library

Google Scholar

[94]

Matthew Goto, Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, and James Riely. 2016. An extensible approach to session polymorphism. Mathematical Structures in Computer Science 26, 465--509.

Crossref

Google Scholar

[95]

Mohamed G. Gouda, Eric G. Manning, and Yao-Tin Yu. 1984. On the progress of communications between two finite state machines. Inform. Control 63, 3 (1984), 200--216.

Digital Library

Google Scholar

[96]

Christian Haack and Alan Jeffrey. 2005. Timed spi-calculus with types for secrecy and authenticity. In CONCUR (LNCS), Vol. 3653. Springer, Berlin, 202--216.

Google Scholar

[97]

Carl Hewitt, Peter Bishop, and Richard Steiger. 1973. A universal modular actor formalism for artificial intelligence. In IJCAI. William Kaufmann, 235--245.

Google Scholar

[98]

C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall, Upper Saddle River, NJ.

Digital Library

Google Scholar

[99]

Kohei Honda. 1993. Types for dyadic interaction. In CONCUR (LNCS), Vol. 715. Springer, Berlin, 509--523.

Google Scholar

[100]

Kohei Honda, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2012. Verification of MPI programs using session types. In EuroMPI (LNCS), Vol. 7490. Springer, Berlin, 291--293.

Google Scholar

[101]

Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language primitives and type discipline for structured communication-based programming. In ESOP (LNCS), Vol. 1381. Springer, Berlin, 122--138.

Digital Library

Google Scholar

[102]

Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL. ACM, New York, NY, 273--284.

Google Scholar

[103]

Hans Hüttel. 2011. Typed ψ-calculi. In CONCUR (LNCS), Vol. 6901. Springer, Berlin, 265--279.

Google Scholar

[104]

Hans Hüttel. 2013. Types for resources in ψ-calculi. In TGC (LNCS), Vol. 8358. Springer, Berlin, 83--102.

Google Scholar

[105]

Hans Hüttel, Naoki Kobayashi, and Takashi Suto. 2009. Undecidable equivalences for basic parallel processes. Inform. Comput. 207, 7 (2009), 812--829.

Digital Library

Google Scholar

[106]

Atsushi Igarashi and Naoki Kobayashi. 2000. Type reconstruction for linear pi-calculus with I/O subtyping. Inform. Comput. 161, 1 (2000), 1--44.

Digital Library

Google Scholar

[107]

Atsushi Igarashi and Naoki Kobayashi. 2004. A generic type system for the pi-calculus. Theor. Comput. Sci. 311, 1--3 (2004), 121--163.

Digital Library

Google Scholar

[108]

Atsushi Igarashi and Hideshi Nagira. 2007. Union types for object-oriented programming. J. Object Technol. 6, 2 (2007), 47--68.

Crossref

Google Scholar

[109]

Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. 2010. Session type inference in Haskell. In PLACES (EPTCS), Vol. 69. Open Publishing Association, 74--91.

Google Scholar

[110]

Nickolas Kavantzas, David Burdett, Gregory Ritzinger, Tony Fletcher, Yves Lafon, and Charlton Barreto. 2005. Web Services Choreography Description Language Version 1.0. Technical Report. W3C. Retrieved from http://www.w3.org/TR/ws-cdl-10/.

Google Scholar

[111]

Naoki Kobayashi. 1998. A partially deadlock-free typed process calculus. ACM Trans. Program. Lang. Syst. 20, 2 (1998), 436--482.

Digital Library

Google Scholar

[112]

Naoki Kobayashi. 2000. Type systems for concurrent processes: From deadlock-freedom to livelock-freedom, time-boundedness. In IFIP TCS (LNCS), Vol. 1872. Springer, Berlin, 365--389.

Crossref

Google Scholar

[113]

Naoki Kobayashi. 2002. A type system for lock-free processes. Inform. Comput. 177, 2 (2002), 122--159.

Digital Library

Google Scholar

[114]

Naoki Kobayashi. 2003. Type systems for concurrent programs. In Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, Vol. 2757. Springer, Berlin, 439--453. Extended version available at http://www-kb.is.s.u-tokyo.ac.jp/&sim;koba/papers/tutorial-type-extended.pdf.

Google Scholar

[115]

Naoki Kobayashi. 2005. Type-based information flow analysis for the pi-calculus. Acta Inf. 42, 4--5 (2005), 291--347.

Crossref

Google Scholar

[116]

Naoki Kobayashi and C.-H. Luke Ong. 2009. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS. IEEE Computer Society, Washington, DC, 179--188.

Google Scholar

[117]

Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. 1996. Linearity and the pi-calculus. In POPL. ACM, New York, NY, 358--371.

Google Scholar

[118]

Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. 1999. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21, 5 (1999), 914--947.

Digital Library

Google Scholar

[119]

Naoki Kobayashi, Shin Saito, and Eijiro Sumii. 2000. An implicitly-typed deadlock-free process calculus. In CONCUR (LNCS), Vol. 1877. Springer, Berlin, 489--503.

Crossref

Google Scholar

[120]

Naoki Kobayashi and Davide Sangiorgi. 2010. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32, 5, Article 16 (2010), 49 pages.

Digital Library

Google Scholar

[121]

Dimitrios Kouzapas, Raymond Hu, Nobuko Yoshida, and Kohei Honda. 2016. On asynchronous eventful session semantics. Math. Struct. Comput. Sci. 26 (2016), 303--364.

Crossref

Google Scholar

[122]

Ivan Lanese, Claudio Guidi, Fabrizio Montesi, and Gianluigi Zavattaro. 2008. Bridging the gap between interaction- and process-oriented choreographies. In SEFM. IEEE Computer Society, Washington, DC, 323--332.

Google Scholar

[123]

Ivan Lanese, Francisco Martins, Vasco Thudichum Vasconcelos, and António Ravara. 2007. Disciplining orchestration and conversation in service-oriented computing. In SEFM. IEEE Computer Society, Washington, DC, 305--314.

Google Scholar

[124]

Ivan Lanese, Fabrizio Montesi, and Gianluigi Zavattaro. 2013. Amending choreographies. In WWV (EPTCS), Vol. 123. Open Publishing Association, 34--48.

Google Scholar

[125]

Cosimo Laneve and Luca Padovani. 2007. The must preorder revisited. In CONCUR (LNCS), Vol. 4703. Springer, Berlin, 212--225.

Google Scholar

[126]

Cosimo Laneve and Luca Padovani. 2013. An algebraic theory for web service contracts. In IFM (LNCS), Vol. 7940. Springer, Berlin, 301--315.

Google Scholar

[127]

Julien Lange and Emilio Tuosto. 2012. Synthesising choreographies from local session types. In CONCUR (LNCS), Vol. 7454. Springer, 225--239.

Google Scholar

[128]

Edward A. Lee and Yuhong Xiong. 2004. A behavioral type system and its application in Ptolemy II. Formal Asp. Comput. 16, 3 (2004), 210--237.

Crossref

Google Scholar

[129]

Barbara Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16, 6 (1994), 1811--1841.

Digital Library

Google Scholar

[130]

Hugo A. López, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, César Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2015. Protocol-based verification of message-passing parallel programs. In OOPSLA. ACM, New York, NY, 280--298.

Google Scholar

[131]

Leonardo Gaetano Mezzina. 2008. How to infer finite session types in a calculus of services and sessions. In COORDINATION (LNCS), Vol. 5052. Springer, Berlin, 216--231.

Google Scholar

[132]

Robin Milner. 1992. Funtions as processes. Math. Struct. Comput. Sci. 2, 2 (1992), 119--141.

Crossref

Google Scholar

[133]

Robin Milner. 1993. The polyadic π-calculus: A tutorial. In Logic and Algebra of Specification. NATO ASI Series, Vol. 94. Springer, Berlin, 203--246.

Google Scholar

[134]

Robin Milner, Joachim Parrow, and David Walker. 1992. A calculus of mobile processes, I. Inform. Comput. 100, 1 (1992), 1--40.

Digital Library

Google Scholar

[135]

Fabrizio Montesi and Nobuko Yoshida. 2013. Compositional choreographies. In CONCUR (LNCS), Vol. 8052. Springer, Berlin, 425--439.

Google Scholar

[136]

Dimitris Mostrous and Nobuko Yoshida. 2009. Session-based communication optimisation for higher-order mobile processes. In TLCA (LNCS), Vol. 5608. Springer, Berlin, 203--218.

Google Scholar

[137]

Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. 2009. Global principal typing in partially commutative asynchronous sessions. In ESOP (LNCS), Vol. 5502. Springer, Berlin, 316--332.

Google Scholar

[138]

Mayur Naik and Jens Palsberg. 2005. A type system equivalent to a model checker. In ESOP (LNCS), Vol. 3444. Springer, Berlin, 374--388.

Google Scholar

[139]

Elie Najm and Abdelkrim Nimour. 1997. A calculus of object bindings. In FMOODS. Chapman & Hall, London.

Google Scholar

[140]

Elie Najm, Abdelkrim Nimour, and Jean-Bernard Stefani. 1999a. Guaranteeing liveness in an object calculus through behavioural typing. In FORTE (IFIP Conference Proceedings), Vol. 156. Kluwer, Amsterdam, 203--221.

Google Scholar

[141]

Elie Najm, Abdelkrim Nimour, and Jean-Bernard Stefani. 1999b. Infinite types for distributed object interfaces. In FMOODS (IFIP Conference Proceedings), Vol. 139. Kluwer, Amsterdam, 353--369.

Crossref

Google Scholar

[142]

Nicholas Ng and Nobuko Yoshida. 2014. Pabble: Parameterised scribble for parallel programming. In PDP. IEEE Computer Society, 707--714.

Google Scholar

[143]

Flemming Nielson and Hanne Riis Nielson. 1993. From CML to process algebras. In CONCUR (LNCS), Vol. 715. Springer, Berlin, 493--508.

Google Scholar

[144]

Flemming Nielson and Hanne Riis Nielson. 1996. From CML to its process algebra. Theor. Comput. Sci. 155, 1 (1996), 179--219.

Digital Library

Google Scholar

[145]

Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer, Berlin.

Digital Library

Google Scholar

[146]

Oscar Nierstrasz. 1995. Regular types for active objects. In Object-Oriented Software Composition. Prentice Hall International, Upper Saddle River, NJ, 99--121.

Google Scholar

[147]

Luca Padovani. 2010a. Contract-based discovery of web services modulo simple orchestrators. Theor. Comput. Sci. 411, 37 (2010), 3328--3347.

Digital Library

Google Scholar

[148]

Luca Padovani. 2010b. Session types = intersection types + union types. In ITRS (EPTCS), Vol. 45. Open Publishing Association, 71--89.

Google Scholar

[149]

Luca Padovani. 2011. Fair subtyping for multi-party session types. In COORDINATION (LNCS), Vol. 6721. Springer, Berlin, 127--141.

Google Scholar

[150]

Luca Padovani. 2013a. Fair subtyping for open session types. In ICALP (2) (LNCS), Vol. 7966. Springer, Berlin, 373--384.

Google Scholar

[151]

Luca Padovani. 2013b. From lock freedom to progress using session types. In PLACES (EPTCS), Vol. 137. Open Publishing Association, 3--19.

Google Scholar

[152]

Luca Padovani. 2014. Deadlock and lock freedom in the linear π-calculus. In CSL-LICS. ACM, New York, NY, 72:1--72:10.

Google Scholar

[153]

Frank Pfenning, Luís Caires, and Bernardo Toninho. 2011. Proof-carrying code in a session-typed process calculus. In CPP (LNCS), Vol. 7086. Springer, Berlin, 21--36.

Google Scholar

[154]

Benjamin C. Pierce. 1991. Programming with Intersection Types, Union Types, and Polymorphism. Technical Report CMU-CS-91-106. CMU.

Google Scholar

[155]

Benjamin C. Pierce and Davide Sangiorgi. 1996. Typing and subtyping for mobile processes. Mathematical Struc. Comput. Sci. 6, 5 (1996), 409--453.

Crossref

Google Scholar

[156]

Garrel Pottinger. 1980. A type assignment for the strongly normalizable lambda-terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, NY, 561--577.

Google Scholar

[157]

Franz Puntigam. 2001a. State inference for dynamically changing interfaces. Comput. Lang. 27, 4 (2001), 163--202.

Digital Library

Google Scholar

[158]

Franz Puntigam. 2001b. Strong types for coordinating active objects. Concurr. Comput.: Practice Exp. 13, 4 (2001), 293--326.

Crossref

Google Scholar

[159]

Franz Puntigam and Christof Peter. 2001. Types for active objects with static deadlock prevention. Fundam. Inform. 48, 4 (2001), 315--341.

Digital Library

Google Scholar

[160]

António Ravara, Pedro Resende, and Vasco Thudichum Vasconcelos. 2012. An algebra of behavioural types. Inform. Comput. 212 (2012), 64--91.

Digital Library

Google Scholar

[161]

António Ravara and Vasco Thudichum Vasconcelos. 2000. Typing non-uniform concurrent objects. In CONCUR (LNCS), Vol. 1877. Springer, Berlin, 474--488.

Crossref

Google Scholar

[162]

Jakob Rehof. 2013. Towards combinatory logic synthesis. In BEAT, Online Proceedings. 47--58.

Google Scholar

[163]

Arend Rensink and Walter Vogler. 2007. Fair testing. Inform. Comput. 205, 2 (2007), 125--198.

Digital Library

Google Scholar

[164]

John C. Reynolds. 1997. Design of the programming language Forsythe. In Algol-like Languages. Birkhäuser, Basel, 173--233.

Google Scholar

[165]

Davide Sangiorgi. 1996. Pi-calculus, internal mobility, and agent-passing calculi. Theor. Comput. Sci. 167, 1&2 (1996), 235--274.

Digital Library

Google Scholar

[166]

Davide Sangiorgi. 1998. An interpretation of typed objects into typed pi-calculus. Inform. Comput. 143, 1 (1998), 34--73.

Digital Library

Google Scholar

[167]

Davide Sangiorgi. 1999. The name discipline of uniform receptiveness. Theor. Comput. Sci. 221, 1--2 (1999), 457--493.

Digital Library

Google Scholar

[168]

Davide Sangiorgi. 2006. Termination of processes. Math. Struct. Comput. Sci. 16, 1 (2006), 1--39.

Digital Library

Google Scholar

[169]

Robert E. Strom and Shaula Yemini. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng. 12, 1 (1986), 157--171.

Digital Library

Google Scholar

[170]

Joshua Sunshine, Karl Naden, Sven Stork, Jonathan Aldrich, and Éric Tanter. 2011. First-class state change in Plaid. In OOPSLA. ACM, New York, NY, 713--732.

Google Scholar

[171]

Alvaro Tasistro, Ernesto Copello, and Nora Szasz. 2012. Principal type scheme for session types. Int. J. Logic Comput. 3, 1 (2012), 34--43.

Google Scholar

[172]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In PPDP. ACM, New York, NY, 161--172.

Google Scholar

[173]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2012. Functions as session-typed processes. In FoSSaCS (LNCS), Vol. 7213. Springer, Berlin, 346--360.

Google Scholar

[174]

Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-order processes, functions, and sessions: A monadic integration. In ESOP (LNCS), Vol. 7792. Springer, Berlin, 350--369.

Google Scholar

[175]

Antonio Vallecillo, Vasco Thudichum Vasconcelos, and António Ravara. 2006. Typing the behavior of software components using session types. Fundam. Inform. 73, 4 (2006), 583--598.

Digital Library

Google Scholar

[176]

Vasco Thudichum Vasconcelos. 1994. Typed concurrent objects. In ECOOP (LNCS), Vol. 821. Springer, Berlin, 100--117.

Google Scholar

[177]

Vasco Thudichum Vasconcelos. 2012. Fundamentals of session types. Inform. Comput. 217 (2012), 52--70.

Digital Library

Google Scholar

[178]

Vasco Thudichum Vasconcelos, Simon Gay, and António Ravara. 2006. Typechecking a multithreaded functional language with session types. Theor. Comput. Sci. 368, 1--2 (2006), 64--87.

Digital Library

Google Scholar

[179]

Hugo Torres Vieira, Luís Caires, and João Costa Seco. 2008. The conversation calculus: A model of service-oriented computation. In ESOP (LNCS), Vol. 4960. Springer, Berlin, 269--283.

Google Scholar

[180]

Hugo Torres Vieira and Vasco Thudichum Vasconcelos. 2013. Typing progress in communication-centred systems. In COORDINATION (LNCS), Vol. 7890. Springer, Berlin, 236--250.

Google Scholar

[181]

Jules Villard. 2011. Heaps and Hops. Ph.D. Dissertation. ENS Cachan.

Google Scholar

[182]

Philip Wadler. 2012. Propositions as sessions. In ICFP. ACM, New York, NY, 273--286.

Google Scholar

[183]

Nobuko Yoshida, Martin Berger, and Kohei Honda. 2004. Strong normalisation in the pi-calculus. Inform. Comput. 191, 2 (2004), 145--202.

Digital Library

Google Scholar

[184]

Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, and Raymond Hu. 2010. Parameterised multiparty session types. In FOSSACS (LNCS), Vol. 6014. Springer, Berlin, 128--145.

Google Scholar

[185]

Nobuko Yoshida and Vasco Thudichum Vasconcelos. 2007. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. In SecReT (ENTCS), Vol. 171(4). Elsevier, Amsterdam, 73--93.

Digital Library

Google Scholar

Cited By

View all

Saffrich HNishida YThiemann P(2024)Law and Order for Typestate with BorrowingProceedings of the ACM on Programming Languages10.1145/36897638:OOPSLA2(1475-1503)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689763
Castellani I(2024)A simple view of multiparty session typesProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678252(1-3)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678252
Dal Lago UPadovani L(2024)On the Almost-Sure Termination of Binary SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678239(1-12)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678239
Show More Cited By

Recommendations

Verifying message-passing programs with dependent behavioural types
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Concurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler ...
Gradual session types

Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type ...
Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types
ICALP '09: Proceedings of the 36th Internatilonal Collogquium on Automata, Languages and Programming: Part II

In the pi-calculus, we consider decidability of certain safety properties expressed in a simple spatial logic. We first introduce a behavioural type system that, given a process <em>P</em> , tries to extract a spatial-behavioural type <em>T</em> , in ...

Reviews

Reviewer: Matthew Mark Huntbach

We are familiar with the notion of types as classifying what a program component does and permissible use of the component. A type system will tell us that a method call must have arguments of particular types and guarantee that it will return a value of a particular type. This paper is a survey of work that goes beyond this, into type systems that classify in more detail possible interactions between program components. This is of particular relevance in concurrent computation where we might want to know not just the type of a single message that one component might send to another, but a pattern of interaction involving the interchange of several messages between two components. An example used throughout the paper to illustrate this is the pattern of interaction between a client and an ATM. One possible type of interaction is: !auth; !balance; __?__amount; !withdraw; !amount; (__?__dispense+__?__overdraft); !quit meaning the client first sends a request to be authorized to use the machine; then a request for the current balance, which is returned; then a request to withdraw, followed by the amount to be withdrawn, which is either dispensed or notice is given that it would result in an overdraft; and then the interaction is concluded. The paper gives a good introduction to the general principles and variations of this sort of typing, with a comprehensive set of references to the many recent papers published in this area. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM Computing Surveys Volume 49, Issue 1

March 2017

705 pages

ISSN:0360-0300

EISSN:1557-7341

DOI:10.1145/2911992

Editor:
Sartaj Sahni
Department of Computer and Information Science and Engineering/University of Florida/Gainesville, FL

Issue’s Table of Contents

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 April 2016

Accepted: 01 January 2016

Revised: 01 August 2015

Received: 01 June 2014

Published in CSUR Volume 49, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tag

Behavioural types

Qualifiers

Survey
Research
Refereed

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

141
Total Citations
View Citations
3,247
Total Downloads

Downloads (Last 12 months)487
Downloads (Last 6 weeks)79

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Saffrich HNishida YThiemann P(2024)Law and Order for Typestate with BorrowingProceedings of the ACM on Programming Languages10.1145/36897638:OOPSLA2(1475-1503)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689763
Castellani I(2024)A simple view of multiparty session typesProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678252(1-3)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678252
Dal Lago UPadovani L(2024)On the Almost-Sure Termination of Binary SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678239(1-12)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678239
Dagnino FPadovani L(2024)sMALL CaPS: An Infinitary Linear Logic for a Calculus of Pure SessionsProceedings of the 26th International Symposium on Principles and Practice of Declarative Programming10.1145/3678232.3678234(1-13)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678232.3678234
Giallorenzo SMontesi FPeressotti M(2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
https://dl.acm.org/doi/10.1145/3632398
Horne RPadovani L(2024)A Logical Account of Subtyping for Session TypesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100986(100986)Online publication date: May-2024
https://doi.org/10.1016/j.jlamp.2024.100986
Ciccone LDagnino FPadovani L(2024)Fair Termination of Multiparty SessionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2024.100964(100964)Online publication date: Mar-2024
https://doi.org/10.1016/j.jlamp.2024.100964
Peters KYoshida N(2024)Mixed choice in session typesInformation and Computation10.1016/j.ic.2024.105164298:COnline publication date: 1-Jun-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105164
Jongmans S(2024)Discourje: Run-Time Verification of Communication Protocols in Clojure — Live at LastFormal Methods10.1007/978-3-031-71177-0_11(158-166)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71177-0_11
Burlò CFrancalanza AScalas ATuosto E(2024)COTS: Connected OpenAPI Test Synthesis for RESTful ApplicationsCoordination Models and Languages10.1007/978-3-031-62697-5_5(75-92)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62697-5_5
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Verifying message-passing programs with dependent behavioural types

Gradual session types

Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types

Reviews

Access critical reviews of Computing literature here