{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:11:38Z","timestamp":1762459898777,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,8,23]],"date-time":"2020-08-23T00:00:00Z","timestamp":1598140800000},"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":[[2020,8,23]]},"DOI":"10.1145\/3406085.3409008","type":"proceedings-article","created":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T19:07:15Z","timestamp":1596222435000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Machine-checked natural semantics for Core Erlang: exceptions and side effects"],"prefix":"10.1145","author":[{"given":"P\u00e9ter","family":"Bereczky","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}]},{"given":"D\u00e1niel","family":"Horp\u00e1csi","sequence":"additional","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}]},{"given":"Simon J.","family":"Thompson","sequence":"additional","affiliation":[{"name":"University of Kent, UK \/ E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}]}],"member":"320","published-online":{"date-parts":[[2020,8,23]]},"reference":[{"volume-title":"Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf.","year":"2013","author":"Armstrong Joe","key":"e_1_3_2_2_1_1"},{"key":"e_1_3_2_2_2_1","volume-title":"18th International Conference, TPHOLs 2005 (LNCS","volume":"3603","author":"Brian","year":"1868"},{"key":"e_1_3_2_2_3_1","unstructured":"P\u00e9ter Bereczky D\u00e1niel Horp\u00e1csi and Simon Thompson. 2020. A Proof Assistant Based Formalisation of Core Erlang. ( 2020 ). arXiv: 2005.11821  P\u00e9ter Bereczky D\u00e1niel Horp\u00e1csi and Simon Thompson. 2020. A Proof Assistant Based Formalisation of Core Erlang. ( 2020 ). arXiv: 2005.11821"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30473-6_5"},{"key":"e_1_3_2_2_5_1","unstructured":"Richard Carlsson Bj\u00f6rn Gustavsson Erik Johansson Thomas Lindgren Sven-Olof Nystr\u00f6m Mikael Pettersson and Robert Virding. 2004. Core Erlang 1.0.3 language specification. Technical Report. htps:\/\/www.it. uu.se\/research\/group\/hipe\/cerl\/doc\/core_erlang-1.0.3.pdf  Richard Carlsson Bj\u00f6rn Gustavsson Erik Johansson Thomas Lindgren Sven-Olof Nystr\u00f6m Mikael Pettersson and Robert Virding. 2004. Core Erlang 1.0.3 language specification. Technical Report. htps:\/\/www.it. uu.se\/research\/group\/hipe\/cerl\/doc\/core_erlang-1.0.3.pdf"},{"volume-title":"Retrieved July 2st","year":"2020","author":"Coq","key":"e_1_3_2_2_6_1"},{"key":"e_1_3_2_2_7_1","unstructured":"Emanuele De Angelis Fabio Fioravanti Adri\u00e1n Palacios Alberto Pettorossi and Maurizio Proietti. 2018. Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs. ( 2018 ). arXiv: 1809.04770  Emanuele De Angelis Fabio Fioravanti Adri\u00e1n Palacios Alberto Pettorossi and Maurizio Proietti. 2018. Bounded Symbolic Execution for Runtime Error Detection of Erlang Programs. ( 2018 ). arXiv: 1809.04770"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Chucky Ellison and Grigore Rosu. 2012. An Executable Formal Semantics of C with Applications. ACM SIGPLAN Notices 47 1 ( 2012 ) 533-544. htps:\/\/doi.org\/10.1145\/2103621.2103719  Chucky Ellison and Grigore Rosu. 2012. An Executable Formal Semantics of C with Applications. ACM SIGPLAN Notices 47 1 ( 2012 ) 533-544. htps:\/\/doi.org\/10.1145\/2103621.2103719","DOI":"10.1145\/2103621.2103719"},{"volume-title":"Retrieved May 4th, 2020","year":"2015","author":"Exceptions","key":"e_1_3_2_2_9_1"},{"key":"e_1_3_2_2_10_1","unstructured":"Lars-\u00c5ke Fredlund. 2001. A framework for reasoning about Erlang code. Ph.D. Dissertation. Mikroelektronik och informationsteknik.  Lars-\u00c5ke Fredlund. 2001. A framework for reasoning about Erlang code. Ph.D. Dissertation. Mikroelektronik och informationsteknik."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100071"},{"volume-title":"Retrieved 11th","year":"2017","author":"Gumbs Kofi","key":"e_1_3_2_2_12_1"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3123569.3123576"},{"key":"e_1_3_2_2_14_1","unstructured":"D\u00e1niel Horp\u00e1csi Judit K\u0151szegi and Zolt\u00e1n Horv\u00e1th. 2017. Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study. ( 2017 ). arXiv: 1708. 07225  D\u00e1niel Horp\u00e1csi Judit K\u0151szegi and Zolt\u00e1n Horv\u00e1th. 2017. Trustworthy Refactoring via Decomposition and Schemes: A Complex Case Study. ( 2017 ). arXiv: 1708. 07225"},{"key":"e_1_3_2_2_15_1","unstructured":"D\u00e1niel Horp\u00e1csi Judit K\u0151szegi and Simon Thompson. 2016. Towards Trustworthy Refactoring in Erlang. ( 2016 ). arXiv: 1607. 02228  D\u00e1niel Horp\u00e1csi Judit K\u0151szegi and Simon Thompson. 2016. Towards Trustworthy Refactoring in Erlang. ( 2016 ). arXiv: 1607. 02228"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2678015.2682542"},{"volume-title":"CEUR Workshop Proceedings 2046 ( 2018 ), 144-160","year":"2018","author":"K\u0151szegi Judit","key":"e_1_3_2_2_17_1"},{"volume-title":"Principles of Programming Languages (POPL)","author":"Kumar Ramana","key":"e_1_3_2_2_18_1"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-90686-7_16"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"crossref","unstructured":"Ivan Lanese Naoki Nishida Adri\u00e1n Palacios and Germ\u00e1n Vidal. 2018. A theory of reversibility for Erlang. Journal of Logical and Algebraic Methods in Programming 100 ( 2018 ) 71-97. htps:\/\/doi.org\/10.1016\/j. jlamp. 2018. 06.004  Ivan Lanese Naoki Nishida Adri\u00e1n Palacios and Germ\u00e1n Vidal. 2018. A theory of reversibility for Erlang. Journal of Logical and Algebraic Methods in Programming 100 ( 2018 ) 71-97. htps:\/\/doi.org\/10.1016\/j. jlamp. 2018. 06.004","DOI":"10.1016\/j.jlamp.2018.06.004"},{"volume-title":"Models, Languages, and Tools for Concurrent and Distributed Programming","author":"Lanese Ivan","key":"e_1_3_2_2_21_1"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52 ( 2009 ). Issue 7. htps:\/\/doi.org\/10.1145\/1538788.1538814  Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52 ( 2009 ). Issue 7. htps:\/\/doi.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"volume-title":"Retrieved July 5th","year":"2020","author":"Core Erlang Natural Semantics","key":"e_1_3_2_2_23_1"},{"key":"e_1_3_2_2_24_1","unstructured":"Martin Neuh\u00e4u\u00dfer and Thomas Noll. 2007. Abstraction and model checking of Core Erlang programs in Maude. Electronic Notes in Theoretical Computer Science 176 4 ( 2007 ) 147-163. htps:\/\/doi.org\/10.1016\/ j.entcs. 2007. 06. 013 Proceedings of the 6th International Workshop on Rewriting Logic and its Applications (WRLA 2006 ).  Martin Neuh\u00e4u\u00dfer and Thomas Noll. 2007. Abstraction and model checking of Core Erlang programs in Maude. Electronic Notes in Theoretical Computer Science 176 4 ( 2007 ) 147-163. htps:\/\/doi.org\/10.1016\/ j.entcs. 2007. 06. 013 Proceedings of the 6th International Workshop on Rewriting Logic and its Applications (WRLA 2006 )."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63139-4_15"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"crossref","unstructured":"John C Reynolds. 1998. Definitional interpreters for higher-order programming languages. Higher-order and symbolic computation 11 4 ( 1998 ) 363-397. htps:\/\/doi.org\/10.1023\/A:1010027404223  John C Reynolds. 1998. Definitional interpreters for higher-order programming languages. Higher-order and symbolic computation 11 4 ( 1998 ) 363-397. htps:\/\/doi.org\/10.1023\/A:1010027404223","DOI":"10.1023\/A:1010027404223"},{"volume-title":"International Andrei Ershov Memorial Conference on Perspectives of System Informatics","author":"Vidal Germ\u00e1n","key":"e_1_3_2_2_27_1"},{"key":"e_1_3_2_2_28_1","unstructured":"Joel J Wright. 2005. Compiling and reasoning about exceptions and interrupts. Ph.D. Dissertation. University of Nottingham.  Joel J Wright. 2005. Compiling and reasoning about exceptions and interrupts. Ph.D. Dissertation. University of Nottingham."}],"event":{"name":"ICFP '20: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Event USA","acronym":"ICFP '20"},"container-title":["Proceedings of the 19th ACM SIGPLAN International Workshop on Erlang"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406085.3409008","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406085.3409008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:52Z","timestamp":1750195912000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406085.3409008"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,23]]},"references-count":28,"alternative-id":["10.1145\/3406085.3409008","10.1145\/3406085"],"URL":"https:\/\/doi.org\/10.1145\/3406085.3409008","relation":{},"subject":[],"published":{"date-parts":[[2020,8,23]]},"assertion":[{"value":"2020-08-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}