Strong Normalization in the π-calculus with Intersection and Union Types

• Autorzy: Piccolo M.
• Języki publikacji: EN

Abstrakty

EN

In this work we present an extension of the linear typing discipline for π-calculus, introduced by Yoshida,Honda and Berger, with Intersection and Union Types. We show that we are able to define a typing system for the π-calculus, which guarantees that every well-typed term is strongly normalizing. This typing system is an extension of that presented in [30] since it is able to type more terms than that presented there.

Słowa kluczowe

EN

intersection types; union types

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2012
• Tom: Vol. 121, nr 1/4
• Strony: 227--252
• Opis fizyczny: Bibliogr. 30 poz.

Twórcy

autor

Piccolo M.

• Dipartimento di Informatica, Universita degli Studi di Torino Preuve Programmes et Systemes , Paris VII, France,

Bibliografia

• [1] Barbanera, F., Berardi, S.: A Symmetric Lambda Calculus for Classical Program Extraction, Information and Computation, 125(2), 1996, 103-117.
• [2] Barbanera, F., Dezani-Ciancaglini, M., de'Liguoro, U.: Intersection and Union Types: Syntax and Semantics, Information and Computation, 119, 1995, 202-230.
• [3] E. Beffara. Logique, Realisabilitè et Concurrence. PhD thesis, Universitè de Paris 7, 2005.
• [4] Berger, M., Honda, K., Yoshida, N.: Sequentiality and the pi-Calculus, Proceedings of Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001 (S. Abramsky, Ed.), 2044, Springer-Verlag, 2001, ISBN 3-540-41960-8.
• [5] Berger, M., Honda, K., Yoshida, N.: Genericity and the pi-Calculus, Proceedings of Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003 (A. D. Gordon, Ed.), 2620, Springer-Verlag, 2003, ISBN 3-540-00897-7.
• [6] M. Boreale On the Expressiveness of Internal Mobility in Name-Passing Calculi, Theoretical Computer Science, 195, 1998, 205-226.
• [7] L. Cardelli, S. Van Bakel and M.G. Vigliotti From X to Pi: Representing Classical Sequent Calculus in Pi-calculus In Proceedings of International Workshop on Classical Logic and Computation, CL&C'08 Reykjavik, Iceland 2008
• [8] G. Castagna, M. Dezani-Ciancaglini, and D. Varacca. Encoding cduce in the cpi-calculus. In C. Baier and H. Hermanns, editors, Proc. of CONCUR 2006, volume 4137 of Lecture Notes in Computer Science, pages 310-326. Springer, 2006.
• [9] Coppo, M., Dezani-Ciancaglini, M.: An Extension of the Basic Functionality Theory for the λ-Calculus, Notre Dame Journal of Formal Logic, 21(4), October 1980, 685-693.
• [10] C. Faggian and M. Piccolo. Ludics is a model for the finitary linear pi-calculus. In S. Ronchi Della Rocca, editor, Proc. of TLCA 2007, volume 4583 of Lecture Notes in Computer Science, pages 148-162. Springer, 2007.
• [11] Girard, J.-Y.: Interprétation fonctionelle et élimination des coupures dans l'arithmetique d'ordre supérieur, Ph.D. Thesis, Université de Paris 7, 1972.
• [12] Girard, J.-Y.: Linear Logic, Theoretical Computer Science, 50, 1987, 1-102.
• [13] Girard, J.-Y.: Locus Solum: from the rules of logics to the logics of rules, Mathematical Structures in Computer Science, 11, 2001, 301-506.
• [14] D. Gorla. Towards a Unified Approach to Encodability and Separation Results for Process Calculi In Proceedings of CONCUR'08 LNCS, 2008.
• [15] Honda, K., Yoshida, N., Berger, M.: Control in the π-calculus, 2004, Submitted.
• [16] A. Igarashi and N. Kobayashi. A generic type system for the pi-calculus. In Proc. of POPL 2001, pages 128-141, 2001.
• [17] A. L. B. Jr., C. Laneve, and L. G. Meredith. Piduce: A process calculus with native xml datatypes. In M. Bravetti, L. Kloul, and G. Zavattaro, editors, Proc. of EPEW 2005 and WS-FM 2005, volume 3670 of Lecture Notes in Computer Science, pages 18-34. Springer, 2005.
• [18] Kobayashi, N., Pierce, B. C., Turner, D. N.: Linearity and the Pi-Calculus, ACM Transactions on Computational Logic, 21(5), 1999, 914-947.
• [19] N. Kobayashi. A type system for lock-free processes. Information and Computation, 177(2):122-159, 2002.
• [20] Laird, J.: A Deconstruction of Non-deterministic Classical Cut Elimination, TLCA, 2001.
• [21] Milner, R.: The Polyadic π-Calculus: A Tutorial, Logic and Algebra of Specification, Proceedings of International NATO Summer School (Marktoberdorf, Germany, 1991) (F. L. Bauer, W. Brauer, H. Schwichtenberg, Eds.), 94, Springer-Verlag, 1993, Available as Technical Report ECS-LFCS-91-180, University of Edinburgh, October 1991.
• [22] Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, 281(1-2), 2002, 471-498.
• [23] Parrow, J.: An Introduction to the pi-calculus, Elsevier, 2001, 479-543.
• [24] Pottinger, G.: A type assignment for the strongly normalizable λ-terms, in: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (J. P. Seldin, J. R. Hindley, Eds.), Academic Press, 1980, 561-577.
• [25] Sangiorgi, D.: Internal Mobility and Agent-Passing Calculi, Proceedings of Automata, Languages and Programming, 22nd International Colloquium, ICALP95, Szeged, Hungary, July 10-14, 1995 (Z. Fülöp, F. Gécseg, Eds.), 944, Springer-Verlag, 1995, ISBN 3-540-60084-1.
• [26] D. Sangiorgi. Termination of processes. draft, 2001.
• [27] Sangiorgi, D., Walker, D.: The π-calculus: a theory of mobile processes, Cambridge University Press, Cambridge, 2001.
• [28] Tait, W. W.: Intensional interpretation of functionals of finite type, The Journal of Symbolic Logic, 32, 1967, 198-212.
• [29] Urban, C., Bierman, G. M.: Strong Normalization of Cut-Elimination in Classical Logic, Fundamenta Informaticæ, 20, 2000, 1-32.
• [30] Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the PI-Calculus, Information and Computation, 191(2), 2004, 145-202.