Observed communication semantics for classical processes. (English) Zbl 1485.68156
Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 56-82 (2017).
Summary: Classical linear logic (CLL) has long inspired readings of its proofs as communicating processes. Wadler’s CP calculus is one of these readings. Wadler gave CP an operational semantics by selecting a subset of the cut-elimination rules of CLL to use as reduction rules. This semantics has an appealing close connection to the logic, but does not resolve the status of the other cut-elimination rules, and does not admit an obvious notion of observational equivalence. We propose a new operational semantics for CP based on the idea of observing communication. We use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, we use the standard relational denotational semantics of CLL. We show that this denotational semantics is adequate for our operational semantics. This allows us to deduce that, for instance, all the cut-elimination rules of CLL are observational equivalences.
For the entire collection see [Zbl 1360.68021].
For the entire collection see [Zbl 1360.68021].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 03F05 | Cut-elimination and normal-form theorems |
| 03F52 | Proof-theoretic aspects of linear logic and other substructural logics |
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | Abramsky, S., Computational interpretations of linear logic, Theor. Comput. Sci., 111, 3-57 (1993) · Zbl 0791.03003 · doi:10.1016/0304-3975(93)90181-R |
| [2] | Abramsky, S., Proofs as processes, Theor. Comput. Sci., 135, 1, 5-9 (1992) · Zbl 0850.68297 · doi:10.1016/0304-3975(94)00103-0 |
| [3] | Accattoli, B.: Linear logic and strong normalization. In: 24th International Conference on Rewriting Techniques and Applications, RTA 2013, 24-26 June 2013, Eindhoven, The Netherlands, pp. 39-54 (2013) · Zbl 1356.03102 |
| [4] | Atkey, R.; Lindley, S.; Morris, JG; Lindley, S.; McBride, C.; Trinder, P.; Sannella, D., Conflation confers concurrency, A List of Successes That Can Change the World, 32-55 (2016), Heidelberg: Springer, Heidelberg · Zbl 1343.68159 · doi:10.1007/978-3-319-30936-1_2 |
| [5] | Baelde, D., Least, greatest fixed points in linear logic, ACM Trans. Comput. Logic, 13, 1, 2:1-2:44 (2012) · Zbl 1352.03072 · doi:10.1145/2071368.2071370 |
| [6] | Barr, M., *-Autonomous categories and linear logic, Math. Struct. Comput. Sci., 1, 2, 159-178 (1991) · Zbl 0777.18006 · doi:10.1017/S0960129500001274 |
| [7] | Bellin, G.; Scott, PJ, On the \(\uppi \)-calculus and linear logic, Theoret. Comput. Sci., 135, 1, 11-65 (1994) · Zbl 0817.03001 · doi:10.1016/0304-3975(94)00104-9 |
| [8] | Berger, M.; Honda, K.; Yoshida, N.; Gordon, AD, Genericity and the \(\uppi \)-calculus, Foundations of Software Science and Computation Structures, 103-119 (2003), Heidelberg: Springer, Heidelberg · Zbl 1029.68039 · doi:10.1007/3-540-36576-1_7 |
| [9] | Caires, L.; Pfenning, F.; Gastin, P.; Laroussinie, F., Session types as intuitionistic linear propositions, CONCUR 2010 - Concurrency Theory, 222-236 (2010), Heidelberg: Springer, Heidelberg · Zbl 1287.68125 · doi:10.1007/978-3-642-15375-4_16 |
| [10] | Curry, HB, Functionality in combinatory logic, Proc. Natl. Acad. Sci., 20, 584-590 (1934) · Zbl 0010.24201 · doi:10.1073/pnas.20.11.584 |
| [11] | Danos, V.; Ehrhard, T., Probabilistic coherence spaces as a model of higher-order probabilistic computation, Inf. Comput., 209, 6, 966-991 (2011) · Zbl 1267.68085 · doi:10.1016/j.ic.2011.02.001 |
| [12] | Davey, BA; Priestley, HA, Introduction to Lattices and Order (2002), Cambridge: Cambridge University Press, Cambridge · Zbl 1002.06001 · doi:10.1017/CBO9780511809088 |
| [13] | Ehrhard, T., Finiteness spaces, Math. Struct. Comput. Sci., 15, 4, 615-646 (2005) · Zbl 1084.03048 · doi:10.1017/S0960129504004645 |
| [14] | Ehrhard, T.; Laurent, O., Interpreting a finitary \(\uppi \)-calculus in differential interaction nets, Inf. Comput., 208, 6, 606-633 (2010) · Zbl 1205.68242 · doi:10.1016/j.ic.2009.06.005 |
| [15] | Gay, SJ; Vasconcelos, VT, Linear type theory for asynchronous session types, J. Funct. Program., 20, 1, 19-50 (2010) · Zbl 1185.68194 · doi:10.1017/S0956796809990268 |
| [16] | Girard, J-Y, Linear logic, Theor. Comput. Sci., 50, 1-101 (1987) · Zbl 0625.03037 · doi:10.1016/0304-3975(87)90045-4 |
| [17] | Honda, K.; Best, E., Types for dyadic interaction, CONCUR’93, 509-523 (1993), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-57208-2_35 |
| [18] | Howard, WA; Seldin, JP; Hindley, JR, The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (1980), Boston: Academic Press, Boston |
| [19] | Laird, J., Manzonetto, G., McCusker, G., Pagani, M.: Weighted relational models of typed \(\lambda \)-calculi. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, 25-28 June 2013, New Orleans, LA, USA, pp. 301-310 (2013) · Zbl 1366.03171 |
| [20] | Lindley, S.; Morris, JG; Vitek, J., A semantics for propositions as sessions, Programming Languages and Systems, 560-584 (2015), Heidelberg: Springer, Heidelberg · Zbl 1335.68060 · doi:10.1007/978-3-662-46669-8_23 |
| [21] | Lindley, S., Morris, J.G.: Talking bananas: structural recursion for session types. In: ICFP (2016, to appear) · Zbl 1360.68334 |
| [22] | Loader, R.: Linear logic, totality and full completeness. In: Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS 1994), 4-7 July 1994, Paris, France, pp. 292-298 (1994) |
| [23] | Mazza, D.: The true concurrency of differential interaction nets. Math. Struct. Comput. Sci. (2015, to appear) · Zbl 1398.68370 |
| [24] | McBride, C.; Lindley, S.; McBride, C.; Trinder, P.; Sannella, D., I got plenty o’ nuttin’, A List of Successes That Can Change the World, 207-233 (2016), Heidelberg: Springer, Heidelberg · Zbl 1343.68060 · doi:10.1007/978-3-319-30936-1_12 |
| [25] | Melliès, P.-A.: Categorical semantics of linear logic. In: Curien, P.-L., Herbelin, H., Krivine, J.-L., Melliès, P.-A. (eds.) Interactive Models of Computation and Program Behavior, Number 27 in Panoramas et Synthèses. Société Mathématique de France (2009) · Zbl 1206.03052 |
| [26] | Milner, R.; Sangiorgi, D.; Kuich, W., Barbed bisimulation, Automata, Languages and Programming, 685-695 (1992), Heidelberg: Springer, Heidelberg · Zbl 1425.68298 · doi:10.1007/3-540-55719-9_114 |
| [27] | Pérez, JA; Caires, L.; Pfenning, F.; Toninho, B., Linear logical relations and observational equivalences for session-based concurrency, Inf. Comput., 239, 254-302 (2014) · Zbl 1309.68141 · doi:10.1016/j.ic.2014.08.001 |
| [28] | Plotkin, GD, LCF considered as a programming language, Theor. Comput. Sci., 5, 3, 223-255 (1977) · Zbl 0369.68006 · doi:10.1016/0304-3975(77)90044-5 |
| [29] | Retoré, C.; Groote, P.; Roger Hindley, J., Pomset logic: a non-commutative extension of classical linear logic, Typed Lambda Calculi and Applications, 300-318 (1997), Heidelberg: Springer, Heidelberg · Zbl 1063.03536 · doi:10.1007/3-540-62688-3_43 |
| [30] | Roscoe, AW, The Theory and Practice of Concurrency (1998), Upper Saddle River: Prentice Hall, Upper Saddle River |
| [31] | Sangiorgi, D.; Walker, D., The \(\uppi \)-Calculus - A Theory of Mobile Processes (2001), Cambridge: Cambridge University Press, Cambridge · Zbl 0981.68116 |
| [32] | Stark, I.: A fully abstract domain model for the \(\uppi \)-calculus. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, 27-30 July 1996, New Brunswick, New Jersey, USA, pp. 36-42 (1996) |
| [33] | Toninho, B., Caires, L., Pfenning, F.: Dependent session types via intuitionistic linear type theory. In: Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 20-22 July 2011, Odense, Denmark, pp. 161-172 (2011) · Zbl 1350.68204 |
| [34] | Toninho, B., Yoshida, N.: Certifying data in multiparty session types. In: A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pp. 433-458 (2016) · Zbl 1343.68063 |
| [35] | Wadler, P.: Propositions as sessions. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012. ACM (2012) · Zbl 1291.68134 |
| [36] | Wadler, P., Propositions as sessions, J. Funct. Program., 24, 2-3, 384-418 (2014) · Zbl 1307.68025 · doi:10.1017/S095679681400001X |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
