nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Linearity, Control Effects, and Behavioral Types

verfasst von : Luís Caires, Jorge A. Pérez

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Mainstream programming idioms intensively rely on state mutation, sharing, and concurrency. Designing type systems for handling and disciplining such idioms is challenging, due to long known conflicts between internal non-determinism, linearity, and control effects such as exceptions. In this paper, we present the first type system that accommodates non-deterministic and abortable behaviors in the setting of session-based concurrent programs. Remarkably, our type system builds on a Curry-Howard correspondence with (classical) linear logic conservatively extended with two dual modalities capturing an additive (co)monad, and provides a first example of a Curry-Howard interpretation of a realistic programming language with built-in internal non-determinism. Thanks to its deep logical foundations, our system elegantly addresses several well-known tensions between control, linearity, and non-determinism: globally, it enforces progress and fidelity; locally, it allows the specification of non-deterministic and abortable computations. The expressivity of our system is illustrated by several examples, including a typed encoding of a higher-order functional language with threads, session channels, non-determinism, and exceptions.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Incremental Update for Graph Rewriting

Nächstes Kapitel Temporary Read-Only Permissions for Separation Logic

We use \(\oplus \) for denoting internal non-determinism in processes since this is rather standard; indeed, this notation goes back at least to De Nicola and Hennessy [19].

Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297–347 (1992)MathSciNetCrossRef

Ariola, Z.M., Herbelin, H.: Minimal classical logic and control operators. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 871–885. Springer, Heidelberg (2003). doi:10.1007/3-540-45061-0_68CrossRefMATH

Atkey, R., Lindley, S., Morris, J.G.: Conflation confers concurrency. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 32–55. Springer, Heidelberg (2016). doi:10.1007/978-3-319-30936-1_2CrossRef

Barber, A.: Dual intuitionistic linear logic. Technical report LFCS-96-347 University of Edinburgh (1996)

Benton, P.N., Bierman, G.M., de Paiva, V.: Computational types from a logical perspective. J. Funct. Program. 8(2), 177–193 (1998)MathSciNetCrossRef

Benton, N., Bierman, G., Paiva, V., Hyland, M.: A term calculus for intuitionistic linear logic. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 75–90. Springer, Heidelberg (1993). doi:10.1007/BFb0037099CrossRefMATH

Boreale, M.: On the expressiveness of internal mobility in name-passing calculi. Theor. Comput. Sci. 195(2), 205–226 (1998)MathSciNetCrossRef

Caires, L.: Types and logic, concurrency and non-determinism. In: Abadi, M., Gardner, P., Gordon, A.D., Mardare, R. (eds.) Essays for the Luca Cardelli Fest, pp. 69–83. Microsoft Research TR MSR-TR–104 (2014)

Caires, L., Pérez, J.A.: Multiparty session types within a canonical binary theory, and beyond. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 74–95. Springer, Heidelberg (2016). doi:10.1007/978-3-319-39570-8_6CrossRefMATH

10.

Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 330–349. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37036-6_19CrossRefMATH

11.

Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222–236. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15375-4_16CrossRef

12.

Caires, L., Pfenning, F., Toninho, B.: Towards concurrent type theory. In: Types in Language Design and Implementation, pp. 1–12 (2012)

13.

Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(03), 367–423 (2016)MathSciNetCrossRef

14.

Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. Math. Struct. Comput. Sci. 26(2), 156–205 (2016)MathSciNetCrossRef

15.

Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 402–417. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85361-9_32CrossRef

16.

Carbone, M., Lindley, S., Montesi, F., Schürmann, C., Wadler, P.: Coherence generalises duality: a logical explanation of multiparty session types. In: CONCUR 2016, pp. 3:1–33:15 (2016)

17.

Carbone, M., Montesi, F., Schürmann, C., Yoshida, N.: Multiparty session types as coherence proofs. In: Proceedings of CONCUR 2015. LIPIcs, vol. 42, pp. 412–426. Schloss Dagstuhl (2015)

18.

Cardelli, L.: Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts, pp. 431–507 (1991)

19.

Nicola, R., Hennessy, M.: CCS without \(\tau \)’s. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) CAAP 1987. LNCS, vol. 249, pp. 138–152. Springer, Heidelberg (1987). doi:10.1007/3-540-17660-8_53CrossRef

20.

DeLine, R., Fähndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465–490. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24851-4_21CrossRef

21.

Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interruptible conversations: distributed dynamic verification with multiparty session types and python. Formal Methods Syst. Des. 46(3), 197–225 (2015)CrossRef

22.

Ehrhard, T., Regnier, L.: Differential interaction nets. Theor. Comput. Sci. 364(2), 166–195 (2006)MathSciNetCrossRef

23.

Ferreira, C., Lanese, I., Ravara, A., Vieira, H.T., Zavattaro, G.: Advanced mechanisms for service combination and transactions. In: Wirsing, M., Hölzl, M. (eds.) Rigorous Software Engineering for Service-Oriented Systems. LNCS, vol. 6582, pp. 302–325. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20401-2_14CrossRef

24.

Gardner, P., Laneve, C., Wischik, L.: Linear forwarders. Inf. Comput. 205(10), 1526–1550 (2007)MathSciNetCrossRef

25.

Gay, S., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19–50 (2010)MathSciNetCrossRef

26.

Griffin, T.: A formulae-as-types notion of control. In: POPL 1990, pp. 47–58 (1990)

27.

Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993). doi:10.1007/3-540-57208-2_35CrossRef

28.

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). doi:10.1007/BFb0053567CrossRef

29.

Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3 (2016)CrossRef

30.

Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. In: 23rd Symposium on Principles of Programming Languages, POPL 1996, pp. 358–371. ACM (1996)

31.

Krishnaswami, N.R., Turon, A., Dreyer, D., Garg, D.: Superficially substructural types. In: ICFP 2012, pp. 41–54 (2012)

32.

Lindley, S., Morris, J.G.: Embedding session types in Haskell. In: 9th International Symposium on Haskell, Haskell 2016, pp. 133–145 (2016)

33.

Militão, F., Aldrich, J., Caires, L.: Rely-guarantee protocols. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 334–359. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44202-9_14CrossRef

34.

Mostrous, D., Vasconcelos, V.T.: Affine sessions. In: Kühn, E., Pugliese, R. (eds.) COORDINATION 2014. LNCS, vol. 8459, pp. 115–130. Springer, Heidelberg (2014). doi:10.1007/978-3-662-43376-8_8CrossRef

35.

Orchard, D.A., Yoshida, N.: Effects as sessions, sessions as effects. In: Proceedings of the POPL 2016, pp. 568–581. ACM (2016)

36.

Parigot, M.: \(\lambda \upmu \)-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992). doi:10.1007/BFb0013061CrossRef

37.

Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations for session-based concurrency. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 539–558. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28869-2_27CrossRef

38.

Pfenning, F.: Structural cut elimination. In: 10th Annual IEEE Symposium on Logic in Computer Science, LICS 1995, pp. 156–166. IEEE Computer Society (1995)

39.

Plotkin, G.D.: A powerdomain construction. SIAM J. Comput. 5(3), 452–487 (1976)MathSciNetCrossRef

40.

Sangiorgi, D., Walker, D.: The \(\pi \)-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH

41.

Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: 30th European Conference on Object-Oriented Programming, ECOOP 2016, pp. 21:1–21:28 (2016)

42.

Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: PPDP 2011, pp. 161–172 (2011)

43.

Toninho, B., Caires, L., Pfenning, F.: Functions as session-typed processes. In: Birkedal, L. (ed.) FoSSaCS 2012. LNCS, vol. 7213, pp. 346–360. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28729-9_23CrossRef

44.

Toninho, B., Caires, L., Pfenning, F.: Higher-order processes, functions, and sessions: a monadic integration. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 350–369. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37036-6_20CrossRefMATH

45.

Tov, J.A., Pucella, R.: Stateful contracts for affine types. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 550–569. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11957-6_29CrossRef

46.

Tov, J.A., Pucella, R.: A theory of substructural types and control. In: OOPSLA 2011, pp. 625–642 (2011)

47.

Tov, J.A., Pucella, R.: Practical affine types. In: POPL 2011, pp. 447–458 (2011)

48.

Wadler, P.: Propositions as sessions. In: ICFP 2012, pp. 273–286. ACM (2012)

Titel: Linearity, Control Effects, and Behavioral Types
verfasst von: Luís Caires
Jorge A. Pérez
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54434-1_9

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"