7 Search Results for "Castellan, Simon"


Document
Causal Unfoldings

Authors: Marc de Visme and Glynn Winskel

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)


Abstract
In the simplest form of event structure, a prime event structure, an event is associated with a unique causal history, its prime cause. However, it is quite common for an event to have disjunctive causes in that it can be enabled by any one of multiple sets of causes. Sometimes the sets of causes may be mutually exclusive, inconsistent one with another, and sometimes not, in which case they coexist consistently and constitute parallel causes of the event. The established model of general event structures can model parallel causes. On occasion however such a model abstracts too far away from the precise causal histories of events to be directly useful. For example, sometimes one needs to associate probabilities with different, possibly coexisting, causal histories of a common event. Ideally, the causal histories of a general event structure would correspond to the configurations of its causal unfolding to a prime event structure; and the causal unfolding would arise as a right adjoint to the embedding of prime in general event structures. But there is no such adjunction. However, a slight extension of prime event structures remedies this defect and provides a causal unfolding as a universal construction. Prime event structures are extended with an equivalence relation in order to dissociate the two roles, that of an event and its enabling; in effect, prime causes are labelled by a disjunctive event, an equivalence class of its prime causes. With this enrichment a suitable causal unfolding appears as a pseudo right adjoint. The adjunction relies critically on the central and subtle notion of extremal causal realisation as an embodiment of causal history.

Cite as

Marc de Visme and Glynn Winskel. Causal Unfoldings. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{devisme_et_al:LIPIcs.CALCO.2019.9,
  author =	{de Visme, Marc and Winskel, Glynn},
  title =	{{Causal Unfoldings}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{9:1--9:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.9},
  URN =		{urn:nbn:de:0030-drops-114376},
  doi =		{10.4230/LIPIcs.CALCO.2019.9},
  annote =	{Keywords: Event Structures, Parallel Causes, Causal Unfolding, Probability}
}
Document
Event Structures for Mixed Choice

Authors: Marc de Visme

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
In the context of models with mixed nondeterministic and probabilistic choice, we present a concurrent model based on partial orders, more precisely Winskel’s event structures. We study its relationship with the interleaving-based model of Segala’s probabilistic automata. Lastly, we use this model to give a truly concurrent semantics to an extension of CCS with probabilistic choice, and relate this concurrent semantics to the usual interleaving semantics, thus generalising existing results on CCS, event structures and labelled transition systems.

Cite as

Marc de Visme. Event Structures for Mixed Choice. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{devisme:LIPIcs.CONCUR.2019.11,
  author =	{de Visme, Marc},
  title =	{{Event Structures for Mixed Choice}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.11},
  URN =		{urn:nbn:de:0030-drops-109137},
  doi =		{10.4230/LIPIcs.CONCUR.2019.11},
  annote =	{Keywords: probability, nondeterminism, concurrency, event structures, CCS}
}
Document
Distributed Strategies Made Easy

Authors: Simon Castellan, Pierre Clairambault, and Glynn Winskel

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)


Abstract
Distributed/concurrent strategies have been introduced as special maps of event structures. As such they factor through their "rigid images," themselves strategies. By concentrating on such "rigid image" strategies we are able to give an elementary account of distributed strategies and their composition, resulting in a category of games and strategies. This is in contrast to the usual development where composition involves the pullback of event structures explicitly and results in a bicategory. It is shown how, in this simpler setting, to extend strategies to probabilistic strategies; and indicated how through probability we can track nondeterministic branching behaviour, that one might otherwise think lost irrevocably in restricting attention to "rigid image" strategies.

Cite as

Simon Castellan, Pierre Clairambault, and Glynn Winskel. Distributed Strategies Made Easy. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 81:1-81:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.MFCS.2017.81,
  author =	{Castellan, Simon and Clairambault, Pierre and Winskel, Glynn},
  title =	{{Distributed Strategies Made Easy}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{81:1--81:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.81},
  URN =		{urn:nbn:de:0030-drops-81315},
  doi =		{10.4230/LIPIcs.MFCS.2017.81},
  annote =	{Keywords: Games, Strategies, Event Structures, Probability}
}
Document
Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or

Authors: Simon Castellan, Pierre Clairambault, and Glynn Winskel

Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.FSCD.2017.12,
  author =	{Castellan, Simon and Clairambault, Pierre and Winskel, Glynn},
  title =	{{Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Miller, Dale},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.12},
  URN =		{urn:nbn:de:0030-drops-77219},
  doi =		{10.4230/LIPIcs.FSCD.2017.12},
  annote =	{Keywords: Game semantics, parallel-or, concurrent games, event structures, full abstraction}
}
Document
Causality vs. Interleavings in Concurrent Game Semantics

Authors: Simon Castellan and Pierre Clairambault

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)


Abstract
We investigate relationships between interleaving and causal notions of game semantics for concurrent programming languages, focusing on the existence of canonical compact causal representations of the interleaving game semantics of programs. We perform our study on an affine variant of Idealized Parallel Algol (IPA), for which we present two games model: and interleaving model (an adaptation of Ghica and Murawski’s fully abstract games model for IPA up to may-testing), and a causal model (a variant of Rideau and Winskel’s games on event structures). Both models are sound and adequate for affine IPA. Then, we relate the two models. First we give a causality-forgetting operation mapping functorially the causal model to the interleaving one. We show that from an interleaving strategy we can reconstruct a causal strategy, from which it follows that the interleaving model is the observational quotient of the causal one. Then, we investigate several reconstructions of causal strategies from interleaving ones, showing finally that there are programs which are inherently causally ambiguous, with several distinct minimal causal representations.

Cite as

Simon Castellan and Pierre Clairambault. Causality vs. Interleavings in Concurrent Game Semantics. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 32:1-32:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.CONCUR.2016.32,
  author =	{Castellan, Simon and Clairambault, Pierre},
  title =	{{Causality vs. Interleavings in Concurrent Game Semantics}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.32},
  URN =		{urn:nbn:de:0030-drops-61620},
  doi =		{10.4230/LIPIcs.CONCUR.2016.32},
  annote =	{Keywords: Game semantics, concurrency, causality, event structures}
}
Document
An Intensionally Fully-abstract Sheaf Model for pi

Authors: Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)


Abstract
Following previous work on CCS, we propose a compositional model for the pi-calculus in which processes are interpreted as sheaves on certain simple sites. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, whose heart is a combinatorial presentation of pi-calculus traces in the spirit of string diagrams. As in previous work, the sheaf condition is analogous to innocence in Hyland-Ong/Nickau games.

Cite as

Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An Intensionally Fully-abstract Sheaf Model for pi. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 86-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{eberhart_et_al:LIPIcs.CALCO.2015.86,
  author =	{Eberhart, Clovis and Hirschowitz, Tom and Seiller, Thomas},
  title =	{{An Intensionally Fully-abstract Sheaf Model for pi}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{86--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.86},
  URN =		{urn:nbn:de:0030-drops-55284},
  doi =		{10.4230/LIPIcs.CALCO.2015.86},
  annote =	{Keywords: concurrency, sheaves, causal models, games}
}
Document
Undecidability of Equality in the Free Locally Cartesian Closed Category

Authors: Simon Castellan, Pierre Clairambault, and Peter Dybjer

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)


Abstract
We show that a version of Martin-Löf type theory with extensional identity, a unit type N1, Sigma, Pi, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.

Cite as

Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{castellan_et_al:LIPIcs.TLCA.2015.138,
  author =	{Castellan, Simon and Clairambault, Pierre and Dybjer, Peter},
  title =	{{Undecidability of Equality in the Free Locally Cartesian Closed Category}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{138--152},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138},
  URN =		{urn:nbn:de:0030-drops-51602},
  doi =		{10.4230/LIPIcs.TLCA.2015.138},
  annote =	{Keywords: Extensional type theory, locally cartesian closed categories, undecidab- ility}
}
  • Refine by Author
  • 4 Castellan, Simon
  • 4 Clairambault, Pierre
  • 3 Winskel, Glynn
  • 2 de Visme, Marc
  • 1 Dybjer, Peter
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Parallel computing models

  • Refine by Keyword
  • 3 concurrency
  • 3 event structures
  • 2 Event Structures
  • 2 Game semantics
  • 2 Probability
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 2 2015
  • 2 2017
  • 2 2019
  • 1 2016

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