TY - JOUR
TI - Continuous Probability Distributions in Concurrent Games
AU - Paquet, Hugo
AU - Winskel, Glynn
T2 - Electronic Notes in Theoretical Computer Science
T3 - Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV)
AB - We present a model of concurrent games in which strategies are probabilistic and support both discrete and continuous distributions. This is a generalisation of the probabilistic concurrent strategies of Winskel, based on event structures. We first introduce measurable event structures, discrete fibrations of event structures in which each fibre is turned into a measurable space. We then construct a bicategory of measurable games and measurable strategies based on measurable event structures, and add probability to measurable strategies using standard techniques of measure theory. We illustrate the model by giving semantics to an affine, higher-order, probabilistic language with a type of real numbers and continuous distributions.
DA - 2018/12/01/
PY - 2018
DO - 10/ggdmwv
DP - ScienceDirect
VL - 341
SP - 321
EP - 344
J2 - Electronic Notes in Theoretical Computer Science
LA - en
SN - 1571-0661
UR - http://www.sciencedirect.com/science/article/pii/S1571066118300975
Y2 - 2019/11/28/15:35:23
KW - Game semantics
KW - Interactive semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - The concurrent game semantics of Probabilistic PCF
AU - Castellan, Simon
AU - Clairambault, Pierre
AU - Paquet, Hugo
AU - Winskel, Glynn
T2 - the 33rd Annual ACM/IEEE Symposium
AB - We define a new games model of Probabilistic PCF (PPCF) by enriching thin concurrent games with symmetry, recently introduced by Castellan et al, with probability. This model supports two interpretations of PPCF, one sequential and one parallel. We make the case for this model by exploiting the causal structure of probabilistic concurrent strategies. First, we show that the strategies obtained from PPCF programs have a deadlock-free interaction, and therefore deduce that there is an interpretation-preserving functor from our games to the probabilistic relational model recently proved fully abstract by Ehrhard et al. It follows that our model is intensionally fully abstract. Finally, we propose a definition of probabilistic innocence and prove a finite definability result, leading to a second (independent) proof of full abstraction.
C1 - Oxford, United Kingdom
C3 - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18
DA - 2018///
PY - 2018
DO - 10/ggdjfz
DP - Crossref
SP - 215
EP - 224
LA - en
PB - ACM Press
SN - 978-1-4503-5583-4
UR - http://dl.acm.org/citation.cfm?doid=3209108.3209187
Y2 - 2019/11/26/16:57:36
KW - Denotational semantics
KW - Game semantics
KW - Interactive semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Geometry of Interaction and Linear Combinatory Algebras
AU - Abramsky, Samson
AU - Haghverdi, Esfandiar
AU - Scott, Philip
T2 - Mathematical. Structures in Comp. Sci.
AB - We present an axiomatic framework for Girard's Geometry of Interaction based on the notion of linear combinatory algebra. We give a general construction on traced monoidal categories, with certain additional structure, that is sufficient to capture the exponentials of Linear Logic, which produces such algebras (and hence also ordinary combinatory algebras). We illustrate the construction on six standard examples, representing both the ‘particle-style’ as well as the ‘wave-style’ Geometry of Interaction.
DA - 2002/10//
PY - 2002
DO - 10/fcsmhm
DP - ACM Digital Library
VL - 12
IS - 5
SP - 625
EP - 665
SN - 0960-1295
UR - http://dx.doi.org/10.1017/S0960129502003730
Y2 - 2019/11/28/15:33:04
KW - Interactive semantics
KW - Linear logic
ER -
TY - CONF
TI - Probabilistic game semantics
AU - Danos, Vincent
AU - Harmer, Russell
T2 - ACM Transactions on Computational Logic - TOCL
AB - A category of HO/N-style games and probabilistic strategies is developed where the possible choices of a strategy are quantified so as to give a measure of the likelihood of seeing a given play. A 2-sided die is shown to be universal in this category, in the sense that any strategy breaks down into a composition between some deterministic strategy and that die. The interpretative power of the category is then demonstrated by delineating a Cartesian closed subcategory which provides a fully abstract model of a probabilistic extension of Idealized Algol
DA - 2000/02/01/
PY - 2000
DO - 10/b6k43s
DP - ResearchGate
VL - 3
SP - 204
EP - 213
SN - 978-0-7695-0725-5
KW - Denotational semantics
KW - Game semantics
KW - Interactive semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - On Geometry of Interaction
AU - Girard, Jean-Yves
A2 - Schwichtenberg, Helmut
T3 - NATO ASI Series
AB - The paper expounds geometry of interaction, for the first time in the full case, i.e. for all connectives of linear logic, including additives and constants. The interpretation is done within a C*-algebra which is induced by the rule of resolution of logic programming, and therefore the execution formula can be presented as a simple logic programming loop. Part of the data is public (shared channels) but part of it can be viewed as private dialect (defined up to isomorphism) that cannot be shared during interaction, thus illustrating the theme of communication without understanding. One can prove a nilpotency (i.e. termination) theorem for this semantics, and also its soundness w.r.t. a slight modification of familiar sequent calculus in the case of exponential-free conclusions.
C1 - Berlin, Heidelberg
C3 - Proof and Computation
DA - 1995///
PY - 1995
DO - 10/fr557p
DP - Springer Link
SP - 145
EP - 191
LA - en
PB - Springer
SN - 978-3-642-79361-5
KW - Interactive semantics
KW - Linear logic
ER -