{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:13:34Z","timestamp":1762460014828,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T00:00:00Z","timestamp":1599004800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004895","name":"European Social Fund","doi-asserted-by":"publisher","award":["EFOP-3.6.2-16-2017-00013,EFOP-3.6.3-VEKOP-16-2017-00002"],"award-info":[{"award-number":["EFOP-3.6.2-16-2017-00013,EFOP-3.6.3-VEKOP-16-2017-00002"]}],"id":[{"id":"10.13039\/501100004895","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100012550","name":"Nemzeti Kutat\u00e1si, Fejleszt\u00e9si \u00e9s Innovaci\u00f3s Alap","doi-asserted-by":"publisher","award":["UNKP-20-4,TKP2020-NKA-06"],"award-info":[{"award-number":["UNKP-20-4,TKP2020-NKA-06"]}],"id":[{"id":"10.13039\/501100012550","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,2]]},"DOI":"10.1145\/3462172.3462200","type":"proceedings-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T22:06:52Z","timestamp":1627078012000},"page":"150-161","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Validating Formal Semantics by Property-Based Cross-Testing"],"prefix":"10.1145","author":[{"given":"P\u00e9ter","family":"Bereczky","sequence":"first","affiliation":[{"name":"ELTE, E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}]},{"given":"D\u00e1niel","family":"Horp\u00e1csi","sequence":"additional","affiliation":[{"name":"ELTE, E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}]},{"given":"Judit","family":"K\u0151szegi","sequence":"additional","affiliation":[{"name":"ELTE, E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}]},{"given":"Soma","family":"Szeier","sequence":"additional","affiliation":[{"name":"ELTE, E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}]},{"given":"Simon","family":"Thompson","sequence":"additional","affiliation":[{"name":"University of Kent, Canterbury, UK and ELTE, E\u00f6tv\u00f6s Lor\u00e1nd University, Budapest, Hungary"}]}],"member":"320","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"volume-title":"Trends in Functional Programming","author":"Bereczky P\u00e9ter","key":"e_1_3_2_1_1_1","unstructured":"P\u00e9ter Bereczky , D\u00e1niel Horp\u00e1csi , and Simon Thompson . 2020. A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang . In Trends in Functional Programming , Aleksander Byrski and John Hughes (Eds.). Springer International Publishing , Cham , 139\u2013158. https:\/\/doi.org\/10.1007\/978-3-030-57761-2_7 10.1007\/978-3-030-57761-2_7 P\u00e9ter Bereczky, D\u00e1niel Horp\u00e1csi, and Simon Thompson. 2020. A Proof Assistant Based Formalisation of a Subset of Sequential Core Erlang. In Trends in Functional Programming, Aleksander Byrski and John Hughes (Eds.). Springer International Publishing, Cham, 139\u2013158. https:\/\/doi.org\/10.1007\/978-3-030-57761-2_7"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406085.3409008"},{"key":"e_1_3_2_1_3_1","unstructured":"P\u00e9ter Bereczky D\u00e1niel Horp\u00e1csi and Simon Thompson. 2020. A Comparison of Big-step Semantics Definition Styles. arxiv:2011.10373\u00a0[cs.PL]  P\u00e9ter Bereczky D\u00e1niel Horp\u00e1csi and Simon Thompson. 2020. A Comparison of Big-step Semantics Definition Styles. arxiv:2011.10373\u00a0[cs.PL]"},{"key":"e_1_3_2_1_4_1","volume-title":"C\/C++ Verification Workshop.","author":"Blazy Sandrine","year":"2043","unstructured":"Sandrine Blazy . 2007. Experiments in validating formal semantics for C . In C\/C++ Verification Workshop. Oxford, United Kingdom , 95\u2013102. https:\/\/hal.inria.fr\/inria-0029 2043 Sandrine Blazy. 2007. Experiments in validating formal semantics for C. In C\/C++ Verification Workshop. Oxford, United Kingdom, 95\u2013102. https:\/\/hal.inria.fr\/inria-00292043"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_3_2_1_6_1","first-page":"1","volume":"49","author":"Bodin Martin","year":"2014","unstructured":"Martin Bodin 2014 . A Trusted Mechanised JavaScript Specification. SIGPLAN Not. 49 , 1 (Jan. 2014), 87\u2013100. https:\/\/doi.org\/10.1145\/2578855.2535876 10.1145\/2578855.2535876 Martin Bodin 2014. A Trusted Mechanised JavaScript Specification. SIGPLAN Not. 49, 1 (Jan. 2014), 87\u2013100. https:\/\/doi.org\/10.1145\/2578855.2535876","journal-title":"A Trusted Mechanised JavaScript Specification. SIGPLAN Not."},{"key":"e_1_3_2_1_7_1","first-page":"8","article-title":"A Trustworthy Mechanized Formalization of R","volume":"53","author":"Bodin Martin","year":"2018","unstructured":"Martin Bodin , Tom\u00e1s Diaz , and \u00c9ric Tanter . 2018 . A Trustworthy Mechanized Formalization of R . SIGPLAN Not. 53 , 8 (Oct. 2018), 13\u201324. https:\/\/doi.org\/10.1145\/3393673.3276946 10.1145\/3393673.3276946 Martin Bodin, Tom\u00e1s Diaz, and \u00c9ric Tanter. 2018. A Trustworthy Mechanized Formalization of R. SIGPLAN Not. 53, 8 (Oct. 2018), 13\u201324. https:\/\/doi.org\/10.1145\/3393673.3276946","journal-title":"SIGPLAN Not."},{"key":"e_1_3_2_1_8_1","unstructured":"Richard Carlsson 2004. Core Erlang 1.0.3 language specification. Technical Report. https:\/\/www.it.uu.se\/research\/group\/hipe\/cerl\/doc\/core_erlang-1.0.3.pdf  Richard Carlsson 2004. Core Erlang 1.0.3 language specification. Technical Report. https:\/\/www.it.uu.se\/research\/group\/hipe\/cerl\/doc\/core_erlang-1.0.3.pdf"},{"volume-title":"ERLANG Programming (1sted.). O\u2019Reilly Media","author":"Cesarini Francesco","key":"e_1_3_2_1_9_1","unstructured":"Francesco Cesarini and Simon Thompson . 2009. ERLANG Programming (1sted.). O\u2019Reilly Media , Inc . Francesco Cesarini and Simon Thompson. 2009. ERLANG Programming (1sted.). O\u2019Reilly Media, Inc."},{"key":"#cr-split#-e_1_3_2_1_10_1.1","doi-asserted-by":"crossref","unstructured":"Arthur Chargu\u00e9raud. 2013. Pretty-Big-Step Semantics. In Programming Languages and Systems Matthias Felleisen and Philippa Gardner (Eds.). Springer. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_3 10.1007\/978-3-642-37036-6_3","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"#cr-split#-e_1_3_2_1_10_1.2","doi-asserted-by":"crossref","unstructured":"Arthur Chargu\u00e9raud. 2013. Pretty-Big-Step Semantics. In Programming Languages and Systems Matthias Felleisen and Philippa Gardner (Eds.). Springer. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_3","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_3_2_1_11_1","volume-title":"Retrieved April 21st","author":"Coq","year":"2021","unstructured":"Coq documentation 2021 . Ltac documentation . Retrieved April 21st , 2021 from https:\/\/coq.inria.fr\/refman\/proof-engine\/ltac.html Coq documentation 2021. Ltac documentation. Retrieved April 21st, 2021 from https:\/\/coq.inria.fr\/refman\/proof-engine\/ltac.html"},{"key":"e_1_3_2_1_12_1","volume-title":"Retrieved April 21st","author":"Coq","year":"2021","unstructured":"Coq introduction 2021 . A short introduction to Coq . Retrieved April 21st , 2021 from https:\/\/coq.inria.fr\/a-short-introduction-to-coq Coq introduction 2021. A short introduction to Coq. Retrieved April 21st, 2021 from https:\/\/coq.inria.fr\/a-short-introduction-to-coq"},{"volume-title":"Retrieved April 21st","year":"2021","key":"e_1_3_2_1_13_1","unstructured":"Cross-testing semantics 2021 . Erlang semantics testing . Retrieved April 21st , 2021 from https:\/\/github.com\/harp-project\/erlang-semantics-testing Cross-testing semantics 2021. Erlang semantics testing. Retrieved April 21st, 2021 from https:\/\/github.com\/harp-project\/erlang-semantics-testing"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863509.1863521"},{"key":"e_1_3_2_1_15_1","volume-title":"Retrieved April 21st","author":"Syntax Tools OTP","year":"2021","unstructured":"Erlang\/ OTP Syntax Tools 2021 . Erlang\/OTP Syntax Tools . Retrieved April 21st , 2021 from http:\/\/erlang.org\/documentation\/doc-11.1.4\/lib\/syntax_tools-2.4\/doc\/pdf\/syntax_tools-2.4.pdf Erlang\/OTP Syntax Tools 2021. Erlang\/OTP Syntax Tools. Retrieved April 21st, 2021 from http:\/\/erlang.org\/documentation\/doc-11.1.4\/lib\/syntax_tools-2.4\/doc\/pdf\/syntax_tools-2.4.pdf"},{"volume-title":"Retrieved April 21st","year":"2021","key":"e_1_3_2_1_16_1","unstructured":"ErLLVM-bench 2021 . ErLLVM-bench . Retrieved April 21st , 2021 from https:\/\/github.com\/cstavr\/erllvm-bench ErLLVM-bench 2021. ErLLVM-bench. Retrieved April 21st, 2021 from https:\/\/github.com\/cstavr\/erllvm-bench"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_23"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.14778\/3151113.3151116"},{"key":"e_1_3_2_1_19_1","unstructured":"F. Hebert. 2019. Property-Based Testing with PropEr Erlang and Elixir: Find Bugs Before Your Users Do. Pragmatic Bookshelf. https:\/\/books.google.hu\/books?id=SGI0uQEACAAJ  F. Hebert. 2019. Property-Based Testing with PropEr Erlang and Elixir: Find Bugs Before Your Users Do. Pragmatic Bookshelf. https:\/\/books.google.hu\/books?id=SGI0uQEACAAJ"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278186.3278193"},{"key":"e_1_3_2_1_22_1","unstructured":"Xuan Huang. 2019. A Mechanized Formalization of the WebAssembly Specification in Coq. https:\/\/www.cs.rit.edu\/~mtf\/student-resources\/20191_huang_mscourse.pdf  Xuan Huang. 2019. A Mechanized Formalization of the WebAssembly Specification in Coq. https:\/\/www.cs.rit.edu\/~mtf\/student-resources\/20191_huang_mscourse.pdf"},{"key":"e_1_3_2_1_23_1","volume-title":"Retrieved April 21st","author":"K","year":"2021","unstructured":"K projects 2021 . K framework project catalogue . Retrieved April 21st , 2021 from https:\/\/github.com\/kframework K projects 2021. K framework project catalogue. Retrieved April 21st, 2021 from https:\/\/github.com\/kframework"},{"key":"e_1_3_2_1_24_1","volume-title":"CEUR Workshop Proceedings 2046 (2018","author":"K\u0151szegi Judit","year":"2018","unstructured":"Judit K\u0151szegi . 2018 . KErl: Executable semantics for Erlang . CEUR Workshop Proceedings 2046 (2018 ), 144\u2013160. http:\/\/ceur-ws.org\/Vol-2046\/koszegi.pdf Judit K\u0151szegi. 2018. KErl: Executable semantics for Erlang. CEUR Workshop Proceedings 2046 (2018), 144\u2013160. http:\/\/ceur-ws.org\/Vol-2046\/koszegi.pdf"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.56422"},{"key":"e_1_3_2_1_26_1","volume-title":"Retrieved April 21st","author":"Module","year":"2021","unstructured":"Module proper_erlang_abstract_code 2021 . PropEr generator of abstract code . Retrieved April 21st , 2021 from https:\/\/github.com\/proper-testing\/proper\/blob\/master\/src\/proper_erlang_abstract_code.erl Module proper_erlang_abstract_code 2021. PropEr generator of abstract code. Retrieved April 21st, 2021 from https:\/\/github.com\/proper-testing\/proper\/blob\/master\/src\/proper_erlang_abstract_code.erl"},{"key":"e_1_3_2_1_27_1","volume-title":"Retrieved April 21st","author":"Core Erlang Natural Semantics","year":"2021","unstructured":"Natural Semantics for Core Erlang 2021 . Core Erlang Formalization . Retrieved April 21st , 2021 from https:\/\/github.com\/harp-project\/Core-Erlang-Formalization Natural Semantics for Core Erlang 2021. Core Erlang Formalization. Retrieved April 21st, 2021 from https:\/\/github.com\/harp-project\/Core-Erlang-Formalization"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 6th International Workshop on Rewriting Logic and its Applications. ENTCS 176","author":"Neuh\u00e4u\u00dfer Martin","year":"2007","unstructured":"Martin Neuh\u00e4u\u00dfer and Thomas Noll . 2007 . Abstraction and model checking of Core Erlang programs in Maude , In Proceedings of the 6th International Workshop on Rewriting Logic and its Applications. ENTCS 176 , 4, 147\u2013163. https:\/\/doi.org\/10.1016\/j.entcs.2007.06.013 10.1016\/j.entcs.2007.06.013 Martin Neuh\u00e4u\u00dfer and Thomas Noll. 2007. Abstraction and model checking of Core Erlang programs in Maude, In Proceedings of the 6th International Workshop on Rewriting Logic and its Applications. ENTCS 176, 4, 147\u2013163. https:\/\/doi.org\/10.1016\/j.entcs.2007.06.013"},{"key":"e_1_3_2_1_29_1","volume-title":"Retrieved April 21st","author":"Erlang Parser Official Core","year":"2018","unstructured":"Official Core Erlang Parser 2018 . Core Erlang YECC Parser Grammar . Retrieved April 21st , 2021 from https:\/\/github.com\/erlang\/otp\/blob\/master\/lib\/compiler\/src\/core_parse.yrl Official Core Erlang Parser 2018. Core Erlang YECC Parser Grammar. Retrieved April 21st, 2021 from https:\/\/github.com\/erlang\/otp\/blob\/master\/lib\/compiler\/src\/core_parse.yrl"},{"volume-title":"Functional Big-Step Semantics","author":"Scott Owens","key":"e_1_3_2_1_30_1","unstructured":"Scott Owens 2016. Functional Big-Step Semantics . In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 589\u2013615. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23 10.1007\/978-3-662-49498-1_23 Scott Owens 2016. Functional Big-Step Semantics. In Programming Languages and Systems, Peter Thiemann (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 589\u2013615. https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23"},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of AST\u201911","author":"Pa\u0142ka H.","year":"2011","unstructured":"Micha\u0142\u00a0 H. Pa\u0142ka , Koen Claessen , Alejandro Russo , and John Hughes . 2011 . Testing an Optimising Compiler by Generating Random Lambda Terms . In Proceedings of AST\u201911 . ACM, New York, NY, USA, 91\u201397. https:\/\/doi.org\/10.1145\/ 1982595.1982615 10.1145\/1982595.1982615 Micha\u0142\u00a0H. Pa\u0142ka, Koen Claessen, Alejandro Russo, and John Hughes. 2011. Testing an Optimising Compiler by Generating Random Lambda Terms. In Proceedings of AST\u201911. ACM, New York, NY, USA, 91\u201397. https:\/\/doi.org\/10.1145\/1982595.1982615"},{"volume-title":"Programming Languages and Systems, Bruno C. d.\u00a0S","author":"Per\u00e9nyi \u00c1rp\u00e1d","key":"e_1_3_2_1_32_1","unstructured":"\u00c1rp\u00e1d Per\u00e9nyi and Jan Midtgaard . 2020. Stack-Driven Program Generation of WebAssembly . In Programming Languages and Systems, Bruno C. d.\u00a0S . Oliveira (Ed.). Springer International Publishing , Cham , 209\u2013230. https:\/\/doi.org\/10.1007\/978-3-030-64437-6_11 10.1007\/978-3-030-64437-6_11 \u00c1rp\u00e1d Per\u00e9nyi and Jan Midtgaard. 2020. Stack-Driven Program Generation of WebAssembly. In Programming Languages and Systems, Bruno C. d.\u00a0S. Oliveira (Ed.). Springer International Publishing, Cham, 209\u2013230. https:\/\/doi.org\/10.1007\/978-3-030-64437-6_11"},{"key":"e_1_3_2_1_33_1","first-page":"2","volume":"48","author":"Politz Joe\u00a0Gibbs","year":"2012","unstructured":"Joe\u00a0Gibbs Politz 2012 . A Tested Semantics for Getters, Setters, and Eval in JavaScript. SIGPLAN Not. 48 , 2 (oct 2012), 1\u201316. https:\/\/doi.org\/10.1145\/2480360.2384579 10.1145\/2480360.2384579 Joe\u00a0Gibbs Politz 2012. A Tested Semantics for Getters, Setters, and Eval in JavaScript. SIGPLAN Not. 48, 2 (oct 2012), 1\u201316. https:\/\/doi.org\/10.1145\/2480360.2384579","journal-title":"SIGPLAN Not."},{"key":"e_1_3_2_1_34_1","volume-title":"Retrieved January 7th","author":"Documentation QuickCheck","year":"2017","unstructured":"QuickCheck Documentation 2017 . QuviQ QuickCheck . Retrieved January 7th , 2021 from http:\/\/quviq.com\/documentation\/eqc QuickCheck Documentation 2017. QuviQ QuickCheck. Retrieved January 7th, 2021 from http:\/\/quviq.com\/documentation\/eqc"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294102"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364489.2364494"},{"key":"e_1_3_2_1_37_1","volume-title":"Retrieved April 21st","author":"Book The BEAM","year":"2020","unstructured":"The BEAM Book 2020 . The Erlang Runtime System . Retrieved April 21st , 2021 from https:\/\/github.com\/happi\/theBeamBook\/releases\/download\/0.0.14.fix\/beam-book.pdf The BEAM Book 2020. The Erlang Runtime System. Retrieved April 21st, 2021 from https:\/\/github.com\/happi\/theBeamBook\/releases\/download\/0.0.14.fix\/beam-book.pdf"},{"key":"e_1_3_2_1_38_1","volume-title":"Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language. arxiv:1803.09885\u00a0[cs.PL]","author":"Yang Zheng","year":"2018","unstructured":"Zheng Yang and Hang Lei . 2018 . Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language. arxiv:1803.09885\u00a0[cs.PL] Zheng Yang and Hang Lei. 2018. Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language. arxiv:1803.09885\u00a0[cs.PL]"}],"event":{"name":"IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages","acronym":"IFL 2020","location":"Canterbury United Kingdom"},"container-title":["Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462200","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462172.3462200","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:34Z","timestamp":1750191454000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462172.3462200"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,2]]},"references-count":38,"alternative-id":["10.1145\/3462172.3462200","10.1145\/3462172"],"URL":"https:\/\/doi.org\/10.1145\/3462172.3462200","relation":{},"subject":[],"published":{"date-parts":[[2020,9,2]]},"assertion":[{"value":"2021-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}