Published in Volume XXII, Issue 1, 2012, pages 147-199, doi: 10.7561/SACS.2012.1.147
Authors: T. Hirschowitz, D. Pous
Abstract
Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner’s CCS. We construct a category E of plays, and a subcategory V of views. We argue that presheaves on V adequately represent innocent strategies, in the sense of game semantics. We equip innocent strategies with a simple notion of interaction.
Full Text (PDF)References
[1] Emmanuel Beffara. Logique, realisabilite et concurrence. PhD thesis, -Universite Paris 7, December 2005.
[2] Marcello M. Bonsangue, Jan J. M. M. Rutten, and Alexandra Silva. A Kleene theorem for polynomial coalgebras. In Luca de Alfaro, editor, FOSSACS, volume 5504 of Lecture Notes in Computer Science, pages 122-136. Springer, 2009.
[3] Ed Brinksma, Arend Rensink, and Walter Vogler. Fair testing. In Insup Lee and Scott A. Smolka, editors, CONCUR, volume 962 of Lecture Notes in Computer Science, pages 313-327. Springer, 1995.
[4] Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical Computer Science, 115(1):43-62, 1993. http://dx.doi.org/10.1016/0304-3975(93)90054-W
[5] Aurelio Carboni and Peter Johnstone. Connected limits, familial representability and artin glueing. Mathematical Structures in Computer Science, 5(4):441-459, 1995. http://dx.doi.org/10.1017/S0960129500001183
[6] Aurelio Carboni and Peter Johnstone. Corrigenda for `connected limits, familial representability and artin glueing’. Mathematical Structures in Computer Science, 14(1):185-187, 2004. http://dx.doi.org/10.1017/S0960129503004080
[7] Rocco De Nicola and Matthew Hennessy. Testing equivalences for processes. Theor. Comput. Sci., 34:83-133, 1984. http://dx.doi.org/10.1016/0304-3975(84)90113-0
[8] Olivier Delande and Dale Miller. A neutral approach to proof and refutation in mall. In LICS ’08 [30], pages 498-508.
[9] H. Ehrig, H.-J. Kreowski, Ugo Montanari, and Grzegorz Rozenberg, editors. Handbook of Graph Grammars and Computing by Graph Transformation, Volume 3: Concurrency, Parallelism and Distribution. World Scientific, 1999.
[10] Marcelo P. Fiore. Second-order and dependently-sorted abstract syntax. In LICS ’08 [30], pages 57-68.
[11] Fabio Gadducci, Reiko Heckel, and Merce Llabres. A bi-categorical axiomatisation of concurrent graph rewriting. Electronic Notes in Theoretical Computer Science, 29, 1999.
[12] Fabio Gadducci and Ugo Montanari. The tile model. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, pages 133-166. The MIT Press, 2000.
[13] Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, 2001. http://dx.doi.org/10.1017/S096012950100336X
[14] Yves Guiraud and Philippe Malbos. Higher-dimensional categories with finite derivation type. Theory and Applications of Categories, 22(18):420-278, 2009.
[15] Andre Hirschowitz and Marco Maggesi. Modules over monads and linearity. In Daniel Leivant and Ruy J. G. B. de Queiroz, editors, WoLLIC, volume 4576 of Lecture Notes in Computer Science, pages 218-237. Springer, 2007.
[16] Andre Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Information and Computation, 208(5):545-564, 2010. http://dx.doi.org/10.1016/j.ic.2009.07.003
[17] Andre, Michel, and Tom Hirschowitz. Contraction-free proofs and finitary games for linear logic. Electronic Notes in Theoretical Computer Science, 249:287-305, 2009. http://dx.doi.org/10.1016/j.entcs.2009.07.095
[18] Tom Hirschowitz. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Preprint. http://hal.archives-ouvertes.fr/hal-00540205/en/, 2010.
[19] Tom Hirschowitz and Damien Pous. Innocent strategies as presheaves and interactive equivalences for CCS. In Alexandra Silva, Simon Bliudze, Roberto Bruni, and Marco Carbone, editors, ICE, volume 59 of EPTCS, pages 2-24, 2011.
[20] Martin Hyland. Semantics and Logics of Computation, chapter Game Semantics. Cambridge University Press, 1997.
[21] Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999.
[22] Ole H. Jensen and Robin Milner. Bigraphs and mobile processes (revised). Technical Report TR580, University of Cambridge, 2004.
[23] P. T. Johnstone, S. Lack, and P. Sobocinski. Quasitoposes, quasiadhesive categories and Artin glueing. In CALCO, volume 4624 of LNCS, pages 312-326. Springer Verlag, 2007.
[24] Andre Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation and open maps. In LICS ’93, pages 418-427. IEEE Computer Society, 1993.
[25] Stefano Kasangian and Anna Labella. Observational trees as models for concurrency. Mathematical Structures in Computer Science, 9(6):687-718, 1999. http://dx.doi.org/10.1017/S0960129599002935
[26] G. M. Kelly. Elementary observations on 2-categorical limits. Bulletin of the Australian Mathematical Society, 39:301-317, 1989. http://dx.doi.org/10.1017/S0004972700002781
[27] Joachim Kock. Polynomial functors and trees. International Mathematics Research Notices, 2011(3):609-673, 2011.
[28] Jean-Louis Krivine. Dependent choice, `quote’ and the clock. Theor. Comput. Sci., 308(1-3):259-276, 2003. http://dx.doi.org/10.1016/S0304-3975(02)00776-4
[29] James J. Leifer and Robin Milner. Deriving bisimulation congruences for reactive systems. In Catuscia Palamidessi, editor, CONCUR, volume 1877 of Lecture Notes in Computer Science, pages 243-258. Springer, 2000.
[30] Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA. IEEE Computer Society, 2008.
[31] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer, 2nd edition, 1998.
[32] Saunders MacLane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext. Springer, 1992.
[33] Paul-Andre Mellies. Asynchronous games 2: the true concurrency of innocence. In Proc. CONCUR ’04, volume 3170 of LNCS, pages 448-465. Springer Verlag, 2004.
[34] Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980.
[35] V. Natarajan and Rance Cleaveland. Divergence and fair testing. In Zoltan Fulop and Ferenc Gecseg, editors, ICALP, volume 944 of Lecture Notes in Computer Science, pages 648-659. Springer, 1995.
[36] Tobias Nipkow. Higher-order critical pairs. In LICS ’91, pages 342-349. IEEE Computer Society, 1991.
[37] Gordon D. Plotkin. A structural approach to operational semantics. DAIMI Report FN-19, Computer Science Department, Aarhus University, 1981.
[38] Julian Rathke and Pawel Sobocinski. Deconstructing behavioural theories of mobility. In Ifip TCS, volume 273 of IFIP, pages 507-520. Springer, 2008.
[39] Vladimiro Sassone and Pawel Sobocinski. Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing, 10(2), 2003.
[40] Peter Sewell. From rewrite to bisimulation congruences. In Davide Sangiorgi and Robert de Simone, editors, CONCUR, volume 1466 of Lecture Notes in Computer Science, pages 269-284. Springer, 1998.
[41] Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In LICS ’97, pages 280-291, 1997.
[42] Rob J. van Glabbeek. The linear time-branching time spectrum (extended abstract). In Jos C. M. Baeten and Jan Willem Klop, editors, CONCUR, volume 458 of Lecture Notes in Computer Science, pages 278-297. Springer, 1990.
[43] Angelo Vistoli. Notes on Grothendieck topologies, fibered categories and descent theory. Preprint. http://arxiv.org/abs/math/0412512 , 2007.
Bibtex
@article{sacscuza:hirschowitz2013isapaiefc,
title={Innocent Strategies as Presheaves and Interactive Equivalences for CCS},
author={T. Hirschowitz and D. Pous},
journal={Scientific Annals of Computer Science},
volume={22},
number={1},
organization={``A.I. Cuza'' University, Iasi, Romania},
year={2013},
pages={147--199},
doi={10.7561/SACS.2012.1.147},
publisher={``A.I. Cuza'' University Press}
}