{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:18:45Z","timestamp":1781893125645,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009876","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"586-598","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["LOIS: syntax and semantics"],"prefix":"10.1145","author":[{"given":"Eryk","family":"Kopczy\u0144ski","sequence":"first","affiliation":[{"name":"University of Warsaw, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Szymon","family":"Toru\u0144czyk","sequence":"additional","affiliation":[{"name":"University of Warsaw, Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_3_1","volume-title":"Department of Computer Science","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . The SMT-LIB Standard: Version 2.0. Technical report , Department of Computer Science , The University of Iowa , 2010 . Available at www.SMT-LIB.org. Clark Barrett, Aaron Stump, and Cesare Tinelli. The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010. Available at www.SMT-LIB.org."},{"key":"e_1_3_2_1_4_1","first-page":"885","volume-title":"Handbook of Satisfiability","author":"Barrett Clark W.","year":"2009","unstructured":"Clark W. Barrett , Roberto Sebastiani , Sanjit A. Seshia , and Cesare Tinelli . Satisfiability modulo theories . In Handbook of Satisfiability , pages 825\u2013 885 , 2009 . Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, pages 825\u2013885, 2009."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103704"},{"key":"e_1_3_2_1_6_1","first-page":"364","volume-title":"LICS","author":"Boja\u00b4nczyk Miko\u0142aj","unstructured":"Miko\u0142aj Boja\u00b4nczyk , Bartek Klin , and S\u0142awomir Lasota . Automata with group actions . In LICS , pages 355\u2013 364 . IEEE Computer Society, 2011. Miko\u0142aj Boja\u00b4nczyk, Bartek Klin, and S\u0142awomir Lasota. Automata with group actions. In LICS, pages 355\u2013364. IEEE Computer Society, 2011."},{"key":"e_1_3_2_1_7_1","first-page":"10","article-title":"Automata theory in nominal sets","author":"Boja\u00b4nczyk Miko\u0142aj","year":"2014","unstructured":"Miko\u0142aj Boja\u00b4nczyk , Bartek Klin , and S\u0142awomir Lasota . Automata theory in nominal sets . Log. Meth. Comp. Sci. , 10 , 2014 . Miko\u0142aj Boja\u00b4nczyk, Bartek Klin, and S\u0142awomir Lasota. Automata theory in nominal sets. Log. Meth. Comp. Sci., 10, 2014.","journal-title":"Log. Meth. Comp. Sci."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_12"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_12"},{"key":"e_1_3_2_1_10_1","series-title":"LIPIcs","first-page":"15","volume-title":"Deepak D\u2019Souza","author":"Boja\u00b4nczyk Miko\u0142aj","unstructured":"Miko\u0142aj Boja\u00b4nczyk and Szymon Toru\u00b4nczyk . Imperative programming in sets with atoms . In Deepak D\u2019Souza , Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, FSTTCS , volume 18 of LIPIcs , pages 4\u2013 15 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Miko\u0142aj Boja\u00b4nczyk and Szymon Toru\u00b4nczyk. Imperative programming in sets with atoms. In Deepak D\u2019Souza, Telikepalli Kavitha, and Jaikumar Radhakrishnan, editors, FSTTCS, volume 18 of LIPIcs, pages 4\u2013 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012."},{"key":"e_1_3_2_1_11_1","first-page":"259","volume-title":"Proc. CSL\u201915","author":"Clemente L.","year":"2015","unstructured":"L. Clemente and S. Lasota . Reachability analysis of first-order definable pushdown systems . In Proc. CSL\u201915 , pages 244\u2013 259 , 2015 . L. Clemente and S. Lasota. Reachability analysis of first-order definable pushdown systems. In Proc. CSL\u201915, pages 244\u2013259, 2015."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01895716"},{"key":"e_1_3_2_1_13_1","volume-title":"Fenton and Ed Dubinsky. Introduction to discrete mathematics with ISETL","author":"William","year":"1996","unstructured":"William E. Fenton and Ed Dubinsky. Introduction to discrete mathematics with ISETL . Springer , 1996 . William E. Fenton and Ed Dubinsky. Introduction to discrete mathematics with ISETL. Springer, 1996."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/262326"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90242-9"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80011-5"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_3_2_1_20_1","unstructured":"Eryk Kopczy\u00b4nski and Szymon Toru\u00b4nczyk. LOIS website. See http:\/\/www.mimuw.edu.pl\/~erykk\/lois.  Eryk Kopczy\u00b4nski and Szymon Toru\u00b4nczyk. LOIS website. See http:\/\/www.mimuw.edu.pl\/~erykk\/lois."},{"key":"e_1_3_2_1_21_1","unstructured":"Eryk Kopczy\u00b4nski and Szymon Toru\u00b4nczyk. LOIS: technical documentation. See http:\/\/www.mimuw.edu.pl\/~erykk\/lois.  Eryk Kopczy\u00b4nski and Szymon Toru\u00b4nczyk. LOIS: technical documentation. See http:\/\/www.mimuw.edu.pl\/~erykk\/lois."},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, SMT@IJCAR 2016","author":"Kopczynski Eryk","year":"2016","unstructured":"Eryk Kopczynski and Szymon Toru\u00b4nczyk . LOIS : an application of SMT solvers. In Tim King and Ruzica Piskac, editors , Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, SMT@IJCAR 2016 , Coimbra, Portugal , July 1-2, 2016 . Eryk Kopczynski and Szymon Toru\u00b4nczyk. LOIS: an application of SMT solvers. In Tim King and Ruzica Piskac, editors, Proceedings of the 14th International Workshop on Satisfiability Modulo Theories affiliated with the International Joint Conference on Automated Reasoning, SMT@IJCAR 2016, Coimbra, Portugal, July 1-2, 2016."},{"key":"e_1_3_2_1_23_1","unstructured":"volume \n  1617\n   of \n  CEUR Workshop Proceedings pages 51\u2013\n  60\n  . CEUR-WS.org 2016. volume 1617 of CEUR Workshop Proceedings pages 51\u201360. CEUR-WS.org 2016."},{"key":"e_1_3_2_1_24_1","volume-title":"MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I","volume":"8634","author":"Murawski Andrzej S.","year":"2014","unstructured":"Andrzej S. Murawski , Steven J. Ramsay , and Nikos Tzevelekos . Reachability in pushdown register automata. In Erzs\u00e9bet Csuhaj-Varj\u00b4u, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium , MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I , volume 8634 of Lecture Notes in Computer Science, pages 464\u2013473. Springer , 2014 . Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Reachability in pushdown register automata. In Erzs\u00e9bet Csuhaj-Varj\u00b4u, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 464\u2013473. Springer, 2014."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4064\/aa-9-4-331-340"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/7349"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009876","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009876","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:33Z","timestamp":1750259133000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":25,"alternative-id":["10.1145\/3009837.3009876","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009876","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009876","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}