{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:32:14Z","timestamp":1760146334364,"version":"build-2065373602"},"reference-count":33,"publisher":"MDPI AG","issue":"11","license":[{"start":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T00:00:00Z","timestamp":1729641600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"\u00daNKP-23-3 New National Excellence Program of the Ministry for Culture and Innovation from the source of the National Research, Development and Innovation Fund","award":["TKP2021-NVA"],"award-info":[{"award-number":["TKP2021-NVA"]}]},{"name":"Ministry of Culture and Innovation of Hungary from the National Research, Development and Innovation Fund","award":["TKP2021-NVA"],"award-info":[{"award-number":["TKP2021-NVA"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers"],"abstract":"<jats:p>This paper presents the formal semantics of concurrency in Core Erlang, an intermediate language for Erlang, along with a notion of program equivalence (based on barbed bisimulation) that is able to model equivalence between programs that have different communication structures but the same observable behaviour. The novelty in our formalisation is its extent: it includes semantics for messages and exit and link signals, in addition to most of Core Erlang\u2019s sequential features. Furthermore, unlike previous studies, this work formalises message receipt using primitive operations, consistent with the standard as of Erlang\/OTP 23. In this novel formalisation, we show some generally applicable program equivalences (such as process identifier renaming and silent evaluation) and present a practical case study featuring the equivalence of sequential and concurrent list processing.<\/jats:p>","DOI":"10.3390\/computers13110276","type":"journal-article","created":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T12:04:22Z","timestamp":1729685062000},"page":"276","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Program Equivalence in the Erlang Actor Model"],"prefix":"10.3390","volume":"13","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3183-0712","authenticated-orcid":false,"given":"P\u00e9ter","family":"Bereczky","sequence":"first","affiliation":[{"name":"Department of Programming Languages and Compilers, ELTE E\u00f6tv\u00f6s Lor\u00e1nd University, 1117 Budapest, Hungary"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0261-0091","authenticated-orcid":false,"given":"D\u00e1niel","family":"Horp\u00e1csi","sequence":"additional","affiliation":[{"name":"Department of Programming Languages and Compilers, ELTE E\u00f6tv\u00f6s Lor\u00e1nd University, 1117 Budapest, Hungary"}]},{"given":"Simon","family":"Thompson","sequence":"additional","affiliation":[{"name":"Department of Programming Languages and Compilers, ELTE E\u00f6tv\u00f6s Lor\u00e1nd University, 1117 Budapest, Hungary"},{"name":"School of Computing, University of Kent, Canterbury CT2 7NZ, UK"}]}],"member":"1968","published-online":{"date-parts":[[2024,10,23]]},"reference":[{"key":"ref_1","unstructured":"Fowler, M. (1999). Refactoring: Improving the Design of Existing Code, Addison-Wesley Longman Publishing Co., Inc."},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Kim, M., Zimmermann, T., and Nagappan, N. (2012, January 11\u201316). A field study of refactoring challenges and benefits. Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, Cary, NC, USA.","DOI":"10.1145\/2393596.2393655"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Ivers, J., Nord, R.L., Ozkaya, I., Seifried, C., Timperley, C.S., and Kessentini, M. (2022, January 14\u201318). Industry experiences with large-scale refactoring. Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Singapore.","DOI":"10.1145\/3540250.3558954"},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Bagheri, A., and Heged\u00fcs, P. (2022, January 23\u201324). Is refactoring always a good egg? exploring the interconnection between bugs and refactorings. Proceedings of the 19th International Conference on Mining Software Repositories, Pittsburgh, PA, USA.","DOI":"10.1145\/3524842.3528034"},{"key":"ref_5","unstructured":"(2024, May 15). Erlang\/OTP Compiler, Version 24.0. Available online: https:\/\/www.erlang.org\/patches\/otp-24.0."},{"key":"ref_6","unstructured":"Carlsson, R., Gustavsson, B., Johansson, E., Lindgren, T., Nystr\u00f6m, S.O., Pettersson, M., and Virding, R. (2024, May 15). Core Erlang 1.0.3 Language Specification. Available online: https:\/\/www.it.uu.se\/research\/group\/hipe\/cerl\/doc\/core_erlang-1.0.3.pdf."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"564","DOI":"10.1007\/s10766-013-0266-5","article-title":"Cost-Directed Refactoring for Parallel Erlang Programs","volume":"42","author":"Brown","year":"2014","journal-title":"Int. J. Parallel Program."},{"key":"ref_8","unstructured":"Bond, A.H., and Gasser, L. (1988). Concurrent programming using actors: Exploiting large-scale parallelism. Readings in Distributed Artificial Intelligence, Morgan Kaufmann."},{"key":"ref_9","unstructured":"Erlang Documentation (2024, May 15). Processes. Available online: https:\/\/www.erlang.org\/doc\/reference_manual\/processes.html."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"373","DOI":"10.14232\/actacyb.298977","article-title":"A Formalisation of Core Erlang, a Concurrent Actor Language","volume":"26","author":"Bereczky","year":"2024","journal-title":"Acta Cybern."},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Bereczky, P., Horp\u00e1csi, D., and Thompson, S. (2023, January 29\u201331). A frame stack semantics for sequential Core Erlang. Proceedings of the 35th Symposium on Implementation and Application of Functional Languages (IFL 2023), Braga, Portugal.","DOI":"10.1145\/3652561.3652566"},{"key":"ref_12","unstructured":"Fredlund, L.\u00c5. (2001). A Framework for Reasoning About Erlang Code. [Ph.D. Thesis, Mikroelektronik och Informationsteknik]."},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Hermenegildo, M.V., and Lopez-Garcia, P. (2016, January 6\u20138). A reversible semantics for Erlang. Proceedings of the International Symposium on Logic-Based Program Synthesis and Transformation, Edinburgh, UK.","DOI":"10.1007\/978-3-319-63139-4"},{"key":"ref_14","unstructured":"Voronkov, A., and Virbitskaite, I. (2014, January 24\u201327). Towards symbolic execution in Erlang. Proceedings of the International Andrei Ershov Memorial Conference on Perspectives of System Informatics, Petersburg, Russia."},{"key":"ref_15","unstructured":"Gallagher, J.P., and Sulzmann, M. (2018, January 9\u201311). CauDEr: A causal-consistent reversible debugger for Erlang. Proceedings of the International Symposium on Functional and Logic Programming, Nagoya, Japan."},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Boreale, M., Corradini, F., Loreti, M., and Pugliese, R. (2019). Playing with bisimulation in Erlang. Models, Languages, and Tools for Concurrent and Distributed Programming, Springer.","DOI":"10.1007\/978-3-030-21485-2"},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Harrison, J.R. (2017, January 8). Towards an Isabelle\/HOL formalisation of Core Erlang. Proceedings of the 16th ACM SIGPLAN International Workshop on Erlang, Oxford, UK.","DOI":"10.1145\/3123569.3123576"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Kong Win Chang, A., Feret, J., and G\u00f6ssler, G. (2023, January 4). A semantics of Core Erlang with handling of signals. Proceedings of the 22nd ACM SIGPLAN International Workshop on Erlang, Seattle, WA, USA.","DOI":"10.1145\/3609022.3609417"},{"key":"ref_19","unstructured":"Gustavsson, B. (2024, October 15). EEP 52: Allow Key and Size Expressions in Map and Binary Matching. Available online: https:\/\/www.erlang.org\/eeps\/eep-0052."},{"key":"ref_20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes, I","volume":"100","author":"Milner","year":"1992","journal-title":"Inf. Comput."},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Cleaveland, W. (1992, January 24\u201327). The problem of \u201cweak bisimulation up to\u201d. Proceedings of the CONCUR\u201892, Stony Brook, NY, USA.","DOI":"10.1007\/BFb0084777"},{"key":"ref_22","unstructured":"Milner, R. (1989). Communication and Concurrency, Prentice-Hall, Inc."},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Kuich, W. (1992, January 13\u201317). Barbed bisimulation. Proceedings of the Automata, Languages and Programming, Wien, Austria.","DOI":"10.1007\/3-540-55719-9"},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., and Sirjani, M. (2022). A model of actors and grey failures. Coordination Models and Languages, Springer.","DOI":"10.1007\/978-3-031-08143-9"},{"key":"ref_25","unstructured":"Plotkin, G.D. (1981). A Structural Approach to Operational Semantics, Aarhus University."},{"key":"ref_26","unstructured":"Felleisen, M., and Friedman, D.P. (1986, January 25\u201328). Control operators, the SECD-machine, and the \u03bb-calculus. Proceedings of the Formal Description of Programming Concepts\u2014III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts\u2014III, Ebberup, Denmark."},{"key":"ref_27","unstructured":"Pitts, A.M., and Stark, I.D. (1998). Operational reasoning for functions with local state. Higher Order Operational Techniques in Semantics, Cambridge University Press."},{"key":"ref_28","unstructured":"Cesarini, F., and Thompson, S. (2009). Erlang Programming, O\u2019Reilly Media, Inc.. [1st ed.]."},{"key":"ref_29","unstructured":"(2024, October 04). Core Erlang Formalization. Available online: https:\/\/github.com\/harp-project\/Core-Erlang-Formalization\/releases\/tag\/v1.0.7."},{"key":"ref_30","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0304-3975(97)00223-5","article-title":"On bisimulations for the asynchronous \u03c0-calculus","volume":"195","author":"Amadio","year":"1998","journal-title":"Theor. Comput. Sci."},{"key":"ref_31","unstructured":"Urban, C., and Zhang, X. (2015, January 24\u201327). Autosubst: Reasoning with de Bruijn terms and parallel substitutions. Proceedings of the Interactive Theorem Proving, Nanjing, China."},{"key":"ref_32","unstructured":"(2024, October 01). Stdpp: An Extended \u201cStandard Library\u201d for Coq. Available online: https:\/\/gitlab.mpi-sws.org\/iris\/stdpp."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Wiedermann, J., and H\u00e1jek, P. (September, January 28). On the proof method for bisimulation. Proceedings of the Mathematical Foundations of Computer Science 1995, Prague, Czech Republic.","DOI":"10.1007\/3-540-60246-1"}],"container-title":["Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-431X\/13\/11\/276\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T16:18:49Z","timestamp":1760113129000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-431X\/13\/11\/276"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,23]]},"references-count":33,"journal-issue":{"issue":"11","published-online":{"date-parts":[[2024,11]]}},"alternative-id":["computers13110276"],"URL":"https:\/\/doi.org\/10.3390\/computers13110276","relation":{},"ISSN":["2073-431X"],"issn-type":[{"type":"electronic","value":"2073-431X"}],"subject":[],"published":{"date-parts":[[2024,10,23]]}}}