{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:23:16Z","timestamp":1776316996712,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,4,26]],"date-time":"2018-04-26T00:00:00Z","timestamp":1524700800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ANR","award":["ELICA 14 CE25 0005 and LOCALI 11 IS02 0002"],"award-info":[{"award-number":["ELICA 14 CE25 0005 and LOCALI 11 IS02 0002"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2018,8,31]]},"abstract":"<jats:p>We present a probabilistic version of PCF, a well-known simply typed universal functional language. The type hierarchy is based on a single ground type of natural numbers. Even if the language is globally call-by-name, we allow a call-by-value evaluation for ground-type arguments to provide the language with a suitable algorithmic expressiveness. We describe a denotational semantics based on probabilistic coherence spaces, a model of classical Linear Logic developed in previous works. We prove an adequacy and an equational full abstraction theorem showing that equality in the model coincides with a natural notion of observational equivalence.<\/jats:p>","DOI":"10.1145\/3164540","type":"journal-article","created":{"date-parts":[[2018,4,27]],"date-time":"2018-04-27T16:00:21Z","timestamp":1524844821000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Full Abstraction for Probabilistic PCF"],"prefix":"10.1145","volume":"65","author":[{"given":"Thomas","family":"Ehrhard","sequence":"first","affiliation":[{"name":"CNRS, Universit\u00e9 Paris Diderot, Sorbonne Paris Cit\u00e9, France"}]},{"given":"Michele","family":"Pagani","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Diderot, Sorbonne Paris Cit\u00e9, CNRS, France"}]},{"given":"Christine","family":"Tasson","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Diderot, Sorbonne Paris Cit\u00e9, CNRS, France"}]}],"member":"320","published-online":{"date-parts":[[2018,4,26]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/307684"},{"key":"e_1_2_1_2_1","volume-title":"Number 752 in Lecture Notes in Mathematics","author":"Barr Michael","unstructured":"Michael Barr . 1979. *-autonomous Categories. Number 752 in Lecture Notes in Mathematics . Springer-Verlag , Berlin . Michael Barr. 1979. *-autonomous Categories. Number 752 in Lecture Notes in Mathematics. Springer-Verlag, Berlin."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.004"},{"key":"e_1_2_1_4_1","series-title":"Lecture Notes in Computer Science,Vol. 62","volume-title":"Proceedings of the 5th Colloquium Automata, Languages and Programming, Giorgio Ausiello and Corrado B\u00f6hm (Eds.)","author":"Berry G\u00e9rard","unstructured":"G\u00e9rard Berry . 1978. Stable models of typed lambda-calculi . In Proceedings of the 5th Colloquium Automata, Languages and Programming, Giorgio Ausiello and Corrado B\u00f6hm (Eds.) , Lecture Notes in Computer Science,Vol. 62 . Springer-Verlag , 72--89. G\u00e9rard Berry. 1978. Stable models of typed lambda-calculi. In Proceedings of the 5th Colloquium Automata, Languages and Programming, Giorgio Ausiello and Corrado B\u00f6hm (Eds.), Lecture Notes in Computer Science,Vol. 62. Springer-Verlag, 72--89."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(82)80002-9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671586"},{"key":"e_1_2_1_7_1","volume-title":"Marc Bezem (Ed.)","volume":"12","author":"Bucciarelli Antonio","year":"2011","unstructured":"Antonio Bucciarelli , Alberto Carraro , Thomas Ehrhard , and Giulio Manzonetto . 2011 . Full abstraction for resource calculus with tests. In CSL (LIPIcs) , Marc Bezem (Ed.) , Vol. 12 . Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 97--111. http:\/\/drops.dagstuhl.de\/opus\/portals\/extern\/index.php?semnr&equals;11007. Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. 2011. Full abstraction for resource calculus with tests. In CSL (LIPIcs), Marc Bezem (Ed.), Vol. 12. Schloss Dagstuhl, Leibniz-Zentrum fuer Informatik, 97--111. http:\/\/drops.dagstuhl.de\/opus\/portals\/extern\/index.php?semnr&equals;11007."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1033"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209198"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.02.001"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.788986"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000281"},{"key":"e_1_2_1_14_1","unstructured":"Thomas Ehrhard. 2017. An introduction to differential linear logic: Proof-nets models and antiderivatives. Mathematical Structures in Computer Science. 1--66.  Thomas Ehrhard. 2017. An introduction to differential linear logic: Proof-nets models and antiderivatives. Mathematical Structures in Computer Science. 1--66."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_9"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.29"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_2_1_18_1","volume-title":"Probabilistic call by push value. CoRR abs\/1607.04690","author":"Ehrhard Thomas","year":"2016","unstructured":"Thomas Ehrhard and Christine Tasson . 2016. Probabilistic call by push value. CoRR abs\/1607.04690 ( 2016 ). arxiv:1607.04690 http:\/\/arxiv.org\/abs\/1607.04690. Thomas Ehrhard and Christine Tasson. 2016. Probabilistic call by push value. CoRR abs\/1607.04690 (2016). arxiv:1607.04690 http:\/\/arxiv.org\/abs\/1607.04690."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/21541.21543"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90025-5"},{"key":"e_1_2_1_23_1","volume-title":"Linear Logic in Computer Science, Thomas Ehrhard, Jean-Yves Girard","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard . 2004. Between logic and quantic: A tract . In Linear Logic in Computer Science, Thomas Ehrhard, Jean-Yves Girard , Paul Ruet, and Philip Scott (Eds.), London Mathematical Society Lecture Notes Series,Vol. 316. Cambridge University Press , 346--381. Jean-Yves Girard. 2004. Between logic and quantic: A tract. In Linear Logic in Computer Science, Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Philip Scott (Eds.), London Mathematical Society Lecture Notes Series,Vol. 316. Cambridge University Press, 346--381."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.09.003"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.23"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00241-9"},{"key":"e_1_2_1_27_1","volume-title":"Plotkin","author":"Jones Claire","year":"1989","unstructured":"Claire Jones and Gordon D . Plotkin . 1989 . A probabilistic powerdomain of evaluations, See LICS\u2019 89 (1989), 186--195. Claire Jones and Gordon D. Plotkin. 1989. A probabilistic powerdomain of evaluations, See LICS\u201989 (1989), 186--195."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80216-6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.36"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 36th International Colloquium on Automata, Languages and Programming, (ICALP\u201909), Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E","author":"Melli\u00e8s Paul-Andr\u00e9","unstructured":"Paul-Andr\u00e9 Melli\u00e8s , Nicolas Tabareau , and Christine Tasson . 2009. An explicit formula for the free exponential modality of linear logic . In Proceedings of the 36th International Colloquium on Automata, Languages and Programming, (ICALP\u201909), Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E . Nikoletseas, and Wolfgang Thomas (Eds.), Lecture Notes in Computer Science,Vol. 5556. Springer-Verlag , 247--260. Paul-Andr\u00e9 Melli\u00e8s, Nicolas Tabareau, and Christine Tasson. 2009. An explicit formula for the free exponential modality of linear logic. In Proceedings of the 36th International Colloquium on Automata, Languages and Programming, (ICALP\u201909), Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas (Eds.), Lecture Notes in Computer Science,Vol. 5556. Springer-Verlag, 247--260."},{"key":"e_1_2_1_34_1","first-page":"1","article-title":"Categorical semantics of linear logic","volume":"27","author":"Melli\u00e8s Paul-Andr\u00e9","year":"2009","unstructured":"Paul-Andr\u00e9 Melli\u00e8s . 2009 . Categorical semantics of linear logic . Panor. Synth. 27 (2009), 1 -- 196 . Paul-Andr\u00e9 Melli\u00e8s. 2009. Categorical semantics of linear logic. Panor. Synth. 27 (2009), 1--196.","journal-title":"Panor. Synth."},{"key":"e_1_2_1_35_1","volume-title":"See LICS\u201989","author":"Moggi Eugenio","year":"1989","unstructured":"Eugenio Moggi . 1989. Computational lambda-calculus and monads , See LICS\u201989 ( 1989 ), 14--23. Eugenio Moggi. 1989. Computational lambda-calculus and monads, See LICS\u201989 (1989), 14--23."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45187-7_25"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503288"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90003-1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2014.03.003"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS\u201911)","year":"2011","unstructured":"LICS\u201911 2011 . Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS\u201911) . IEEE Computer Society. LICS\u201911 2011. Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS\u201911). IEEE Computer Society."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS\u201989)","year":"1989","unstructured":"LICS\u201989 1989 . Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS\u201989) . IEEE Computer Society. LICS\u201989 1989. Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS\u201989). IEEE Computer Society."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3164540","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3164540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:38Z","timestamp":1750212818000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3164540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,4,26]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,8,31]]}},"alternative-id":["10.1145\/3164540"],"URL":"https:\/\/doi.org\/10.1145\/3164540","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,4,26]]},"assertion":[{"value":"2015-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-04-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}