PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

On the π-calculus and Co-intuitionistic Logic : Notes on Logic for Concurrency and λP Systems

Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
We reconsider work by Bellin and Scott in the 1990s on R. Milner and S. Abramsky’s encoding of linear logic in the π-calculus and give an account of efforts to establish a tight connection between the structure of proofs and of the cut elimination process in multiplicative linear logic, on one hand, and the input-output behaviour of the processes that represent them, on the other, resulting in a proof-theoretic account of (a variant of) Chu’s construction. But Milner’s encoding of the linear lambda calculus suggests consideration of multiplicative co-intuitionistic linear logic: we provide a term assignment for it, a calculus of coroutines which presents features of concurrent and distributed computing. Finally, as a test case of its adequacy as a logic for distributed computation, we represent our term assignment as a λP system. We argue that translations of typed functional languages in concurrent and distributed systems (such as π-calculi or λP systems) are best typed with co-intuitionistic logic, where some features of computations match the logical properties in a natural way.
Wydawca
Rocznik
Strony
21--65
Opis fizyczny
Bibliogr. 32 poz., tab.
Twórcy
autor
  • Dipartimento di Informatica, Universitá degli Studi di Verona, Italy
autor
  • Dipartimento di Informatica, Universitá degli Studi di Verona, Italy
Bibliografia
  • [1] Abramsky, S.: Proofs as Processes, Theor. Comput. Sci., 135(1), 1994, 5-9.
  • [2] Amadio, R. M.: An Asynchronous Model of Locality, Failure and Process Mobility, COORDINATION (D. Garlan, D. L. M˘atayer, Eds.), 1282, Springer, 1997, ISBN 3-540-63383-9.
  • [3] Beffara, E.: A Concurrent Model for Linear Logic., Electr. Notes Theor. Comput. Sci., 155, 2006, 147-168.
  • [4] Bellin, G.: Chu’s Construction: A Proof-theoretic Approach, Logic for Concurrency and Synchronisation (R. J. de Queiroz, Ed.), number 18 in Kluwer Trends in Logic, 2003.
  • [5] Bellin, G.: A Term Assignment for Dual Intuitionistic Logic, LICS’05-IMLA’05 Workshop, Chicago, IL, June 2005.
  • [6] Bellin, G.: Assertions, hypotheses, conjectures and expectations. Rough set semantics and proof-theory, Advances in Natural Deduction (V. De Paiva, L. C. Pereira, E. H. Haeusler, Eds.), Springer, 2013.
  • [7] Bellin, G., Biasi, C.: Towards a Logic for Pragmatics. Assertions and Conjectures., J. Log. Comput., 14(4), 2004, 473-506.
  • [8] Bellin, G., Scott, P. J.: On the _-Calculus and Linear Logic, Theor. Comput. Sci., 135(1), 1994, 11-65.
  • [9] Bierman, G.: On Intuitionistic Linear Logic, Technical Report 346, University of Cambridge Computer Laboratory, 1994, PhD Dissertation.
  • [10] Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions, CONCUR (P. Gastin, F. Laroussinie, Eds.), 6269, Springer, 2010, ISBN 978-3-642-15374-7.
  • [11] Cockett, R., Seely, R.: Linear Distributive Categories, Journal of Pure and Applied Algebra, (114), 1997, 133-173.
  • [12] Colson, L., Jonoska, N., Margenstern, M.: _-P Systems and Typed _-Calculus, Workshop on Membrane Computing (G. Mauri, G. Păun, M. J. Pérez-Jiménez, G. Rozenberg, A. Salomaa, Eds.), 3365, Springer, 2004, ISBN 3-540-25080-8.
  • [13] Crolard, T.: A Formulae-as-Types Interpretation of Subtractive Logic, J. Log. Comput., 14(4), 2004, 529-570.
  • [14] Girard, J.-Y.: Linear Logic, Theor. Comput. Sci., 50, 1987, 1-102.
  • [15] Hennessy, M.: A distributed _-calculus, Cambridge University Press, 2007.
  • [16] Hennessy, M., Merro, M., Rathke, J.: Towards a behavioural theory of access and mobility control in distributed systems, Theor. Comput. Sci., 322(3), 2004, 615-669.
  • [17] Hennessy, M., Riely, J.: Resource Access Control in Systems of Mobile Agents, Inf. Comput., 173(1), 2002, 82-120.
  • [18] Hyland, M., de Paiva, V.: Full Intuitionistic Linear Logic, Ann. Pure Appl. Logic, 64(3), 1993, 273-291.
  • [19] Jonoska, N., Margenstern, M.: Tree Operations in P Systems and _-Calculus, Fundam. Inform., 59(1), 2004, 67-90.
  • [20] Kleijn, J., Koutny, M., Rozenberg, G.: Towards a Petri Net Semantics for Membrane Systems., Workshop on Membrane Computing (R. Freund, G. Paun, G. Rozenberg, A. Salomaa, Eds.), 3850, Springer, 2005, ISBN 3-540-30948-9.
  • [21] Krivine, J.-L.: Lambda-calculus, types and models., Ellis Horwood series in computers and their applications, Masson, 1993, ISBN 978-0-13-062407-9.
  • [22] Lamarche, F.: Proof Nets for Intuitionistic Linear Logic: Essential Nets, 2008.
  • [23] Laneve, C., Victor, B.: Solos In Concert, Mathematical Structures in Computer Science, 13(5), 2003, 657-683.
  • [24] Martí–Oliet, N., Meseguer, J.: From Petri Nets to Linear Logic, Category Theory and Computer Science, Manchester, UK, number 389, Springer-Verlag, 1989.
  • [25] Merro, M.: On the observational theory of the CPS-calculus, Acta Inf., 47(2), 2010, 111-132.
  • [26] Milner, R.: The polyadic _-calculus: A tutorial, Logic and Algebra of Specification (Bauer, Brauer, Schwichtenberg, Eds.), 94, NATO ASI, Springer, 1993.
  • [27] Păun, G.: Computing with Membranes, J. Comput. Syst. Sci., 61(1), 2000, 108-143.
  • [28] Păun, G.: Introduction to Membrane Computing, in: Applications of Membrane Computing (G. Ciobanu, M. J. Pérez-Jiménez, G. Păun, Eds.), Natural Computing Series, Springer, 2006, ISBN 978-3-540-25017-3, page 1-42, Also available at http://psystems.disco.unimib.it/download/MembIntro2004.pdf.
  • [29] Sangiorgi, D., Walker, D.: The _-Calculus - a theory of mobile processes, Cambridge University Press, 2001, ISBN 978-0-521-78177-0.
  • [30] Sewell, P.: Global/Local Subtyping and Capability Inference for a Distributed _-calculus, ICALP (K. G. Larsen, S. Skyum, G. Winskel, Eds.), 1443, Springer, 1998, ISBN 3-540-64781-3.
  • [31] Thielecke, H.: Categorical Structure of Continuation Passing Style, Ph.D. Thesis, University of Edinburgh, 1997, Also available as technical report ECS-LFCS-97-376.
  • [32] Wadler, P.: Propositions as Sessions, Draft paper, available at http://homepages.inf.ed.ac.uk/wadler/topics/recent.html.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-7d34c03d-7505-4b77-98c0-92bdf9771f0b
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.