Document Open Access Logo

Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or

Authors Simon Castellan, Pierre Clairambault, Glynn Winskel

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.12.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Author Details

Simon Castellan
Pierre Clairambault
Glynn Winskel

Cite As Get BibTex

Simon Castellan, Pierre Clairambault, and Glynn Winskel. Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.12

Abstract

Although Plotkin’s parallel-or is inherently deterministic, it has a non-deterministic interpretation in games based on (prime) event structures -  in which an event has a unique causal history - because they do not directly support disjunctive causality. General event structures can express disjunctive causality and have a more permissive notion of determinism, but do not support hiding. We show that (structures equivalent to) deterministic general event structures do support hiding, and construct a new category of games based on them with a deterministic interpretation of aPCFpor, an affine variant of PCF extended with parallel-or. We then exploit this deterministic interpretation to give a relaxed notion of determinism (observable determinism) on the plain event structures model. Putting this together with our previously introduced concurrent notions of well-bracketing and innocence, we obtain an intensionally fully abstract model of aPCFpor.

Subject Classification

Keywords
  • Game semantics
  • parallel-or
  • concurrent games
  • event structures
  • full abstraction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In LICS, Indianapolis, Indiana, USA, June 21-24, 1998, pages 334-344. IEEE Computer Society, 1998. Google Scholar
  2. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409-470, 2000. Google Scholar
  3. Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. ENTCS, 3:2-14, 1996. Google Scholar
  4. Samson Abramsky and Paul-André Melliès. Concurrent games and full completeness. In LICS, Trento, Italy, July 2-5, 1999, pages 431-442. IEEE Computer Society, 1999. Google Scholar
  5. Robert Cartwright, Pierre-Louis Curien, and Matthias Felleisen. Fully abstract semantics for observably sequential languages. Inf. Comput., 111(2):297-401, 1994. Google Scholar
  6. Simon Castellan and Pierre Clairambault. Causality vs. interleavings in concurrent game semantics. In CONCUR 2016, August 23-26, 2016, Québec City, Canada, pages 32:1-32:14, 2016. Google Scholar
  7. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures, 2016. Submitted, URL: https://arxiv.org/abs/1604.04390.
  8. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of PCF. In LICS, Kyoto, Japan, July 6-10, 2015, pages 232-243. IEEE Computer Society, 2015. Google Scholar
  9. Marc de Visme and Glynn Winskel. Strategies with Parallel Causes. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 41:1-41:21, Dagstuhl, Germany, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.41.
  10. Dan R. Ghica. Applications of game semantics: From program analysis to hardware synthesis. In LICS, 11-14 August 2009, Los Angeles, CA, USA, pages 17-26. IEEE Computer Society, 2009. Google Scholar
  11. Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Logic, 151(2-3):89-114, 2008. Google Scholar
  12. Tom Hirschowitz. Full abstraction for fair testing in CCS (expanded version). Logical Methods in Computer Science, 10(4), 2014. Google Scholar
  13. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000. Google Scholar
  14. James Laird. Full abstraction for functional languages with control. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 58-67. IEEE Computer Society, 1997. Google Scholar
  15. Paul-André Melliès and Samuel Mimram. Asynchronous games: Innocence without alternation. In CONCUR, Lisbon, Portugal, September 3-8, 2007, volume 4703 of Lecture Notes in Computer Science, pages 395-411. Springer, 2007. Google Scholar
  16. Gordon D. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5(3):223-255, 1977. Google Scholar
  17. Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, June 21-24, 2011, Toronto, Ontario, Canada, pages 409-418, 2011. Google Scholar
  18. Glynn Winskel. Events in computation. PhD Thesis, Edinburgh University, 1980. Google Scholar
  19. Glynn Winskel. Event structure semantics for CCS and related languages. In ICALP, Aarhus, Denmark, July 12-16, 1982, Proceedings, pages 561-576, 1982. Google Scholar
  20. Glynn Winskel. Event structures. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, 8.-19. September 1986, pages 325-392, 1986. Google Scholar
  21. Glynn Winskel. Deterministic concurrent strategies. Formal Asp. Comput., 24(4-6):647-660, 2012. Google Scholar
  22. Glynn Winskel. Strategies as profunctors. In FOSSACS, Held as Part of ETAPS 2013, Rome, Italy, March 16-24, 2013, pages 418-433, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact