{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:30:19Z","timestamp":1750746619115,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001602","name":"Science Foundation Ireland","doi-asserted-by":"publisher","award":["13\/RC\/2094_P2"],"award-info":[{"award-number":["13\/RC\/2094_P2"]}],"id":[{"id":"10.13039\/501100001602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000923","name":"Silicon Valley Community Foundation","doi-asserted-by":"publisher","award":["2023-324819 (3696)"],"award-info":[{"award-number":["2023-324819 (3696)"]}],"id":[{"id":"10.13039\/100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662103","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T12:30:12Z","timestamp":1718973012000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3970-2486","authenticated-orcid":false,"given":"Vasileios","family":"Koutavas","sequence":"first","affiliation":[{"name":"Trinity College Dublin, Dublin, Ireland"},{"name":"Lero -- Science Foundation Ireland Research Centre for Software, Limerick, Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5783-9454","authenticated-orcid":false,"given":"Yu-Yang","family":"Lin","sequence":"additional","affiliation":[{"name":"Trinity College Dublin, Dublin, Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8509-8059","authenticated-orcid":false,"given":"Nikos","family":"Tzevelekos","sequence":"additional","affiliation":[{"name":"EECS, Queen Mary University of London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"volume-title":"Research Topics in Functional Programming","author":"Abramsky Samson","key":"e_1_3_2_1_1_1","unstructured":"Samson Abramsky. 1990. The Lazy Lambda Calculus. In Research Topics in Functional Programming. Addison-Wesley Longman Publishing Co., Inc., USA, 65--116."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705669"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_7"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_6"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:4)2014"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.24"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63141-0_10"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050120"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2014.01.016"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863566"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1007.4268"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45500-0_16"},{"volume-title":"The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages. Ph. D. Dissertation","author":"Felleisen Matthias","key":"e_1_3_2_1_15_1","unstructured":"Matthias Felleisen. 1987. The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages. Ph. D. Dissertation. Indiana University."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_3_2_1_19_1","unstructured":"Erich Gamma Richard Helm Ralph Johnson and John Vlissides. 1995. Design patterns: elements of reusable object-oriented software. Pearson Deutschland GmbH."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00315-3"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.08.013"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837631"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0075-2"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003482"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_63"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_17"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371127"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_15"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02059-9_3"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1155\/2008\/136939"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_10"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175778"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80083-5"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.15"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.068"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_23"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.26"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Yu-Yang Lin. 2024. LaifsV1\/Hobbit-PDNF: Initial Release. 10.5281\/zenodo.11128050","DOI":"10.5281\/zenodo.11128050"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"volume-title":"Lambda Calculus Models of Programming Languages. Ph. D. Dissertation","author":"Morris J. H.","key":"e_1_3_2_1_47_1","unstructured":"J. H. Morris, Jr. 1968. Lambda Calculus Models of Programming Languages. Ph. D. Dissertation. MIT, Cambridge, MA."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_19"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2017.02.008"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428676"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58140-5_25"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.007"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1042"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890002"},{"volume-title":"Model checking pushdown systems. Ph. D. Dissertation","author":"Schwoon Stefan","key":"e_1_3_2_1_55_1","unstructured":"Stefan Schwoon. 2002. Model checking pushdown systems. Ph. D. Dissertation. Technical University Munich, Germany."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/7.1.103"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190244"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.032"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1284320.1284325"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:3)2011"}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"],"location":"Tallinn Estonia","acronym":"LICS '24"},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662103","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:09Z","timestamp":1750290249000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":60,"alternative-id":["10.1145\/3661814.3662103","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662103","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}