Tytuł artykułu
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
Abstrakty
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
Czasopismo
Rocznik
Tom
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