nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Context-Free Session Type Inference

verfasst von : Luca Padovani

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

Some interesting communication protocols can be precisely described only by context-free session types, an extension of conventional session types with a general form of sequential composition. The complex metatheory of context-free session types, however, hinders the definition of corresponding checking and inference algorithms. In this work we address and solve these problems introducing a new type system for context-free session types of which we provide two OCaml embeddings.

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 A Classical Sequent Calculus with Dependent Types

Nächstes Kapitel Modular Verification of Higher-Order Functional Programs

The claim made in [25] that send_tree_aux is ill typed is incorrect. There exist typing derivations for send_tree_aux proving that it has type \(\upalpha ~\mathtt {tree}\rightarrow T\rightarrow T\) for every \(T\) that satisfies the equation

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-54434-1_30/442829_1_En_30_IEq550_HTML.gif

Ahmed, A., Fluet, M., Morrisett, G.: L\({}^{{3}}\): a linear language with locations. Fundam. Informaticae 77(4), 397–449 (2007)MathSciNetMATH

Charguéraud, A., Pottier, F.: Functional translation of a calculus of capabilities. In: Proceedings of ICFP 2008, pp. 213–224. ACM (2008)

Courcelle, B.: Fundamental properties of infinite trees. Theor. Comput. Sci. 25, 95–169 (1983)MathSciNetCrossRef

Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. In: Proceedings of PPDP 2012, pp. 139–150. ACM (2012)

Demangeon, R., Honda, K.: Full abstraction in a subtyped pi-calculus with linear types. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23217-6_19CrossRef

Florijn, G.: Object protocols as functional parsers. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 351–373. Springer, Heidelberg (1995). doi:10.1007/3-540-49538-X_17CrossRef

Frisch, A., Garrigue, J.: First-class modules and composable signatures in Objective Caml 3.12. In: ACM SIGPLAN Workshop on ML (2010)

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

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

10.

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

11.

Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49665-7_24CrossRef

12.

Hüttel, H., Lanese, I., Vasconcelos, V.T., Caires, L., Carbone, M., Deniélou, P.-M., Mostrous, D., Padovani, L., Ravara, A., Tuosto, E., Vieira, H.T., Zavattaro, G.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3 (2016)CrossRef

13.

Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst. 15(2), 290–311 (1993)CrossRef

14.

Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol. 2757, pp. 439–453. Springer, Heidelberg (2003). doi:10.1007/978-3-540-40007-3_26. http://www.kb.ecei.tohoku.ac.jp/koba/papers/tutorial-type-extended.pdfCrossRef

15.

Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21(5), 914–947 (1999)CrossRef

16.

Launchbury, J., Jones, S.L.P.: State in Haskell. Lisp Symbolic Comput. 8(4), 293–341 (1995)CrossRef

17.

Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10(3), 470–502 (1988)CrossRef

18.

Moggi, E., Sabry, A.: Monadic encapsulation of effects: a revised approach (extended version). J. Funct. Program. 11(6), 591–627 (2001)MathSciNetCrossRef

19.

Nierstrasz, O.: Regular types for active objects. In: Proceedings of OOPSLA 1993, pp. 1–15. ACM (1993)

20.

Padovani, L.: Context-free session type inference. Technical report, Università di Torino (2016). https://hal.archives-ouvertes.fr/hal-01385258/document. Accessed 04 Jan 2017

21.

Padovani, L.: A simple library implementation of binary sessions. J. Funct. Program. 27 (2017). https://doi.org/10.1017/S0956796816000289

22.

Ravara, A., Vasconcelos, V.T.: Typing non-uniform concurrent objects. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 474–489. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_34CrossRef

23.

Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)CrossRef

24.

Südholt, M.: A model of components with non-regular protocols. In: Gschwind, T., Aßmann, U., Nierstrasz, O. (eds.) SC 2005. LNCS, vol. 3628, pp. 99–113. Springer, Heidelberg (2005). doi:10.1007/11550679_8CrossRef

25.

Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: Proceedings of ICFP 2016, pp. 462–475. ACM (2016)

26.

Tov, J.A.: Practical programming with substructural types. Ph.D. thesis, Northeastern University (2012)

27.

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

28.

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

29.

Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2–3), 384–418 (2014)MathSciNetCrossRef

30.

Walker, D., Watkins, K.: On regions and linear types. In: Proceedings of ICFP 2001, pp. 181–192. ACM (2001)

31.

Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)MathSciNetCrossRef

32.

Yallop, J., Kiselyov, O.: First-class modules: hidden power and tantalizing promises. In: ACM SIGPLAN Workshop on ML (2010)

Titel: Context-Free Session Type Inference
verfasst von: Luca Padovani
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_30

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"