乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:08:42Z","timestamp":1740179322463,"version":"3.37.3"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["818616"],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"We study the nature of applicative bisimilarity in \u03bb-calculi endowed with operators for sampling from contin- uous distributions. On the one hand, we show that bisimilarity, logical equivalence, and testing equivalence all coincide with contextual equivalence when real numbers can be manipulated through continuous functions only. The key ingredient towards this result is a notion of Feller-continuity for labelled Markov processes, which we believe of independent interest, giving rise a broad class of LMPs for which coinductive and logically inspired equivalences coincide. On the other hand, we show that if no constraint is put on the way real numbers are manipulated, characterizing contextual equivalence turns out to be hard, and most of the aforementioned notions of equivalence are even unsound.<\/jats:p>","DOI":"10.1145\/3547651","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"826-854","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["On Feller continuity and full abstraction"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3853-1777","authenticated-orcid":false,"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"MPI-SP, Germany \/ IMDEA Software Institute, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4197-0439","authenticated-orcid":false,"given":"Rapha\u00eblle","family":"Crubill\u00e9","sequence":"additional","affiliation":[{"name":"CNRS, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2159-0615","authenticated-orcid":false,"given":"Francesco","family":"Gavazzo","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"volume-title":"Research Topics in Functional Programming","author":"Abramsky Samson","key":"e_1_2_1_1_1","unstructured":"Samson Abramsky . 1990. The Lazy Lambda Calculus . In Research Topics in Functional Programming , D. Turner (Ed.). Addison Wesley , 65\u2013117. Samson Abramsky. 1990. The Lazy Lambda Calculus. In Research Topics in Functional Programming, D. Turner (Ed.). Addison Wesley, 65\u2013117."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1255631584"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57499-9_15"},{"key":"e_1_2_1_4_1","unstructured":"Hendrik Pieter Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland. \t\t\t\t Hendrik Pieter Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060439"},{"key":"e_1_2_1_6_1","volume-title":"Ugo Dal Lago, and Francesco Gavazzo","author":"Barthe Gilles","year":"2022","unstructured":"Gilles Barthe , Rapha\u00eblle Crubill\u00e9 , Ugo Dal Lago, and Francesco Gavazzo . 2022 . On Feller Continuity and Full Abstraction (Long Version) . arXiv preprint arXiv:2207.10590. Gilles Barthe, Rapha\u00eblle Crubill\u00e9, Ugo Dal Lago, and Francesco Gavazzo. 2022. On Feller Continuity and Full Abstraction (Long Version). arXiv preprint arXiv:2207.10590."},{"key":"e_1_2_1_7_1","unstructured":"Mathias Beiglb\u00f6ck Christian L\u00e9onard and Walter Schachermayer. 2009. A General Duality Theorem for the Monge\u2013Kantorovich Transport Problem. arXiv preprint arXiv:0911.4347. \t\t\t\t Mathias Beiglb\u00f6ck Christian L\u00e9onard and Walter Schachermayer. 2009. A General Duality Theorem for the Monge\u2013Kantorovich Transport Problem. arXiv preprint arXiv:0911.4347."},{"volume-title":"Probability and Measure","author":"Billingsley Patrick","key":"e_1_2_1_8_1","unstructured":"Patrick Billingsley . 1986. Probability and Measure ( second ed.). John Wiley and Sons . Patrick Billingsley. 1986. Probability and Measure (second ed.). John Wiley and Sons."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614943"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2019.04.002"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_12"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23506-6_7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.007"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.025"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535872"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.02.004"},{"key":"e_1_2_1_20_1","unstructured":"Vincent Danos Fran\u00e7ois Laviolette Jos\u00e9e Desharnais and Prakash Panangaden. 2005. Almost Sure Bisimulation in Labelled Markov Processes. Unpublished note. Available at https:\/\/www.cs.mcgill.ca\/ prakash\/Pubs\/new-neg.pdf \t\t\t\t Vincent Danos Fran\u00e7ois Laviolette Jos\u00e9e Desharnais and Prakash Panangaden. 2005. Almost Sure Bisimulation in Labelled Markov Processes. Unpublished note. Available at https:\/\/www.cs.mcgill.ca\/ prakash\/Pubs\/new-neg.pdf"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705681"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2962"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_19"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.09.013"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00068-1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ICALP.2017.105"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0092872"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(4:6)2018"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2015.156"},{"volume-title":"Classical Descriptive Set Theory","author":"Kechris Alexander S.","key":"e_1_2_1_32_1","unstructured":"Alexander S. Kechris . 2012. Classical Descriptive Set Theory . Springer New York . Alexander S. Kechris. 2012. Classical Descriptive Set Theory. Springer New York."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00532047"},{"key":"e_1_2_1_34_1","unstructured":"Gregory M. Kelly. 2005. Basic Concepts of Enriched Category Theory. Reprints in Theory and Applications of Categories 1\u2013136. \t\t\t\t Gregory M. Kelly. 2005. Basic Concepts of Enriched Category Theory. Reprints in Theory and Applications of Categories 1\u2013136."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.023"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"volume-title":"Relational Reasoning about Functions and Nondeterminism","author":"Lassen S\u00f8ren","key":"e_1_2_1_37_1","unstructured":"S\u00f8ren Lassen . 1998. Relational Reasoning about Functions and Nondeterminism . Aarhus University . BRICS Dissertation Series BRICS DS-98-2. S\u00f8ren Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Aarhus University. BRICS Dissertation Series BRICS DS-98-2."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80083-5"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.15"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_41_1","volume-title":"Arbib","author":"Manes Ernest G.","year":"1986","unstructured":"Ernest G. Manes and Michael A . Arbib . 1986 . Algebraic Approaches to Program Semantics. Springer . Ernest G. Manes and Michael A. Arbib. 1986. Algebraic Approaches to Program Semantics. Springer."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287580"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80602-4"},{"volume-title":"Labelled Markov Processes","author":"Panangaden Prakash","key":"e_1_2_1_46_1","unstructured":"Prakash Panangaden . 2009. Labelled Markov Processes . Imperial College Press . Prakash Panangaden. 2009. Labelled Markov Processes. Imperial College Press."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1090\/chel\/352"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.2307\/44151750"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434292"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1042"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_2_1_53_1","unstructured":"Jan Swart and Anita Winter. 2013. Markov processes: Theory and Examples. Course Notes. \t\t\t\t Jan Swart and Anita Winter. 2013. Markov processes: Theory and Examples. Course Notes."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2011.02.003"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290349"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.021"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/11548133_25"},{"key":"e_1_2_1_58_1","volume-title":"Optimal Transport: Old and New","author":"Villani C\u00e9dric","year":"2008","unstructured":"C\u00e9dric Villani . 2008 . Optimal Transport: Old and New . Springer Science & Business Media . C\u00e9dric Villani. 2008. Optimal Transport: Old and New. Springer Science & Business Media."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547651","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T08:51:02Z","timestamp":1672649462000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547651"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":56,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547651"],"URL":"https:\/\/doi.org\/10.1145\/3547651","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}