{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:18:04Z","timestamp":1750306684468,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100005370","name":"Gates Cambridge Trust","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100005370","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>\n            When defining computations over syntax as data, one often runs into tedious issues concerning\n            <jats:italic>\u03b1<\/jats:italic>\n            -equivalence and semantically correct manipulations of binding constructs. Here we study a semantic framework in which these issues can be dealt with automatically by the programming language. We take the user-friendly \u201cnominal\u201d approach in which bound objects are named. In particular, we develop a version of Scott domains within nominal sets and define two programming languages whose denotational semantics are based on those domains. The first language,\n            <jats:italic>\u03bb\u03bd<\/jats:italic>\n            -PCF, is an extension of Plotkin\u2019s PCF with names that can be swapped, tested for equality and locally scoped; although simple, it already exposes most of the semantic subtleties of our approach. The second language, PNA, extends the first with name abstraction and concretion so that it can be used for metaprogramming over syntax with binders.\n          <\/jats:p>\n          <jats:p>For both languages, we prove a full abstraction result for nominal Scott domains analogous to Plotkin\u2019s classic result about PCF and conventional Scott domains: two program phrases have the same observable operational behaviour in all contexts if and only if they denote equal elements of the nominal Scott domain model. This is the first full abstraction result we know of for languages combining higher-order functions with some form of locally scoped names which uses a domain theory based on ordinary extensional functions, rather than using the more intensional approach of game semantics.<\/jats:p>\n          <jats:p>To obtain full abstraction, we need to add two functionals, one for existential quantification over names and one for \u201cdefinite description\u201d over names. Only adding one of them is not enough, as we give counter-examples to full abstraction in both cases.<\/jats:p>","DOI":"10.1145\/2629529","type":"journal-article","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T13:53:48Z","timestamp":1407851628000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Denotational Semantics with Nominal Scott Domains"],"prefix":"10.1145","volume":"61","author":[{"given":"Steffen","family":"L\u00f6sch","sequence":"first","affiliation":[{"name":"University of Cambridge"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew M.","family":"Pitts","sequence":"additional","affiliation":[{"name":"University of Cambridge"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021851"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_1_4_1","volume-title":"Maibaum Eds.","volume":"3","author":"Abramsky S.","unstructured":"S. Abramsky and A. Jung . 1994. Domain theory. In Handbook of Logic in Computer Science, S. Abramsky, D. M. Gabbay, and T. S. E . Maibaum Eds. , vol. 3 , Clarendon Press, 1--168. S. Abramsky and A. Jung. 1994. Domain theory. In Handbook of Logic in Computer Science, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum Eds., vol. 3, Clarendon Press, 1--168."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103704"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.48"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_12"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.10.007"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.011"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.11.013"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1305810911"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of FOSSACS","volume":"6604","author":"Gabbay M. J.","year":"2011","unstructured":"M. J. Gabbay and V. Ciancia . 2011. Freshness and name-restriction in sets of traces with names . In Proceedings of FOSSACS 2011 . Lecture Notes in Computer Science , vol. 6604 , Springer-Verlag, 365--380. M. J. Gabbay and V. Ciancia. 2011. Freshness and name-restriction in sets of traces with names. In Proceedings of FOSSACS 2011. Lecture Notes in Computer Science, vol. 6604, Springer-Verlag, 365--380."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_1_15_1","volume-title":"Lokal Pr\u00e4sentierbare Kategorien. Lecture Notes in Mathematics","volume":"221","author":"Gabriel P.","unstructured":"P. Gabriel and F. Ulmer . 1971 . Lokal Pr\u00e4sentierbare Kategorien. Lecture Notes in Mathematics , vol. 221 , Springer-Verlag. P. Gabriel and F. Ulmer. 1971. Lokal Pr\u00e4sentierbare Kategorien. Lecture Notes in Mathematics, vol. 221, Springer-Verlag."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8749-3"},{"volume-title":"Practical Foundation for Programming Languages","author":"Harper R.","key":"e_1_2_1_17_1","unstructured":"R. Harper . 2013. Practical Foundation for Programming Languages . Cambridge University Press . R. Harper. 2013. Practical Foundation for Programming Languages. Cambridge University Press."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"volume-title":"A Topos Theory Compendium, Volumes 1 and 2. Number 43--44 in Oxford Logic Guides","author":"Johnstone P. T.","key":"e_1_2_1_19_1","unstructured":"P. T. Johnstone . 2002. Sketches of an Elephant , A Topos Theory Compendium, Volumes 1 and 2. Number 43--44 in Oxford Logic Guides , Oxford University Press . P. T. Johnstone. 2002. Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2. Number 43--44 in Oxford Logic Guides, Oxford University Press."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.10.006"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596571"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of CSL","volume":"12","author":"L\u00f6sch S.","year":"2011","unstructured":"S. L\u00f6sch and A. M. Pitts . 2011. Relating two semantics of locally scoped names . In Proceedings of CSL 2011 , vol. 12 , Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 396--411. S. L\u00f6sch and A. M. Pitts. 2011. Relating two semantics of locally scoped names. In Proceedings of CSL 2011, vol. 12, Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, 396--411."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429073"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02485815"},{"volume-title":"Department of Computer Science","author":"Moggi E.","key":"e_1_2_1_25_1","unstructured":"E. Moggi . 1989. An abstract view of programming languages. Tech. rep. ECS-LFCS-90-113 , Department of Computer Science , University of Edinburgh. E. Moggi. 1989. An abstract view of programming languages. Tech. rep. ECS-LFCS-90-113, Department of Computer Science, University of Edinburgh."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of MFCS","volume":"1893","author":"Montanari U.","year":"2000","unstructured":"U. Montanari and M. Pistore . 2000. &pi;-calculus, structured coalgebras and minimal HD-automata . In Proceedings of MFCS 2000 . Lecture Notes in Computer Science , vol. 1893 , Springer-Verlag, 569--578. U. Montanari and M. Pistore. 2000. &pi;-calculus, structured coalgebras and minimal HD-automata. In Proceedings of MFCS 2000. Lecture Notes in Computer Science, vol. 1893, Springer-Verlag, 569--578."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_30"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.175187"},{"volume-title":"Applied Semantics, Advanced Lectures, International Summer School (APPSEM\u201900)","author":"Pitts A. M.","key":"e_1_2_1_30_1","unstructured":"A. M. Pitts . 2002. Operational semantics and program equivalence . In Applied Semantics, Advanced Lectures, International Summer School (APPSEM\u201900) . G. Barthe, P. Dybjer, and J. Saraiva Eds., Lecture Notes in Computer Science, Tutorial, vol. 2395 , Springer-Verlag , 378--412. A. M. Pitts. 2002. Operational semantics and program equivalence. In Applied Semantics, Advanced Lectures, International Summer School (APPSEM\u201900). G. Barthe, P. Dybjer, and J. Saraiva Eds., Lecture Notes in Computer Science, Tutorial, vol. 2395, Springer-Verlag, 378--412."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000116"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2512979"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of MPC","volume":"1837","author":"Pitts A. M.","year":"2000","unstructured":"A. M. Pitts and M. J. Gabbay . 2000. A metalanguage for programming with bound names modulo renaming . In Proceedings of MPC 2000 . Lecture Notes in Computer Science , vol. 1837 , Springer-Verlag, 230--255. A. M. Pitts and M. J. Gabbay. 2000. A metalanguage for programming with bound names modulo renaming. In Proceedings of MPC 2000. Lecture Notes in Computer Science, vol. 1837, Springer-Verlag, 230--255."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/645722.666533"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.44"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_16"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/646236.682867"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.003"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944729"},{"volume-title":"Domain-Theoretic Foundations of Functional Programming. World Scientific","author":"Streicher T.","key":"e_1_2_1_45_1","unstructured":"T. Streicher . 2006. Domain-Theoretic Foundations of Functional Programming. World Scientific , Singapore . T. Streicher. 2006. Domain-Theoretic Foundations of Functional Programming. World Scientific, Singapore."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"D. C.\n      Turner\n     and \n      G.\n      Winskel\n  . \n  2009\n  . Nominal domain theory for concurrency. In Proceedings of CSL 2009. E. Gr\u00e4del and R. Kahle Eds. Lecture Notes in Computer Science vol. \n  5771 Springer-Verlag 546--560.   D. C. Turner and G. Winskel. 2009. Nominal domain theory for concurrency. In Proceedings of CSL 2009 . E. Gr\u00e4del and R. Kahle Eds. Lecture Notes in Computer Science vol. 5771 Springer-Verlag 546--560.","DOI":"10.1007\/978-3-642-04027-6_39"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926420"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cl.2012.02.002"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629529","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629529","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:18Z","timestamp":1750230078000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629529"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":44,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2629529"],"URL":"https:\/\/doi.org\/10.1145\/2629529","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2013-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}