Decoding Lua: formal semantics for the developer and the semanticist
Trabajo presentado en el "13th ACM SIGPLAN International Symposium on on Dynamic Languages"
| Main Authors: | , , , , |
|---|---|
| Format: | conferenceObject |
| Language: | eng |
| Published: |
2024
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/552830 https://arxiv.org/abs/1706.02400v1 |
| _version_ | 1806012165902041088 |
|---|---|
| author | Soldevila, Mallku Ziliani, Beta Silvestre, Bruno Fridlender, Daniel Mascarenhas, Fabio |
| author_facet | Soldevila, Mallku Ziliani, Beta Silvestre, Bruno Fridlender, Daniel Mascarenhas, Fabio |
| author_sort | Soldevila, Mallku |
| collection | Repositorio Digital Universitario |
| description | Trabajo presentado en el "13th ACM SIGPLAN International Symposium on on Dynamic Languages" |
| format | conferenceObject |
| id | rdu-unc.552830 |
| institution | Universidad Nacional de Cordoba |
| language | eng |
| publishDate | 2024 |
| record_format | dspace |
| spelling | rdu-unc.5528302024-07-25T06:37:56Z Decoding Lua: formal semantics for the developer and the semanticist Soldevila, Mallku Ziliani, Beta Silvestre, Bruno Fridlender, Daniel Mascarenhas, Fabio Lua Operacional semantics PL formalization Trabajo presentado en el "13th ACM SIGPLAN International Symposium on on Dynamic Languages" Fil: Soldevila, Mallku. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Ziliani, Beta. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Silvestre, Bruno. Universidade Federal de Goiás; Brasil. Fil: Mascarenhas, Fabio. Universidade Federal do Rio de Janeiro; Brasil . Fil: Soldevila, Mallku. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Ziliani, Beta. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. We provide formal semantics for a large subset of the Lua programming language, in its version 5.2. We validate our model by mechanizing it and testing it against the test suite of the reference interpreter of Lua, confirming that our model accurately represents the language. In addition, we set us an ambitious goal: to target both a PL semanticist ---not necessarily versed in Lua---, and a Lua developer ---not necessarily versed in semantic frameworks. To the former, we present the peculiarities of the language, and how we model them in a traditional small-step operational semantics, embedded within Felleisen-Hieb's reduction semantics with evaluation contexts. The mechanization is, naturally, performed in PLT Redex, the de facto tool for mechanizing reduction semantics. To the reader unfamiliar with such concepts, we provide, to our best possible within the space limitations, a gentle introduction of the model. It is our hope that developers of the different Lua implementations and dialects understand the model and consider it both for testing their work and for experimenting with new language features. https://dl.acm.org/citation.cfm?id=3133841&picked=prox Fil: Soldevila, Mallku. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Ziliani, Beta. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Fridlender, Daniel. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. Fil: Silvestre, Bruno. Universidade Federal de Goiás; Brasil. Fil: Mascarenhas, Fabio. Universidade Federal do Rio de Janeiro; Brasil . Fil: Soldevila, Mallku. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Fil: Ziliani, Beta. Consejo Nacional de Investigaciones Científicas y Técnicas; Argentina. Ciencias de la Computación 2024-07-24T19:14:59Z 2024-07-24T19:14:59Z 2017 conferenceObject 0362-1340 http://hdl.handle.net/11086/552830 https://arxiv.org/abs/1706.02400v1 eng Versión publicada: https://doi.org/10.1145/3133841.3133848 Attribution-NonCommercial-NoDerivatives 4.0 International http://creativecommons.org/licenses/by-nc-nd/4.0/ Impreso; Electrónico y/o Digital |
| spellingShingle | Lua Operacional semantics PL formalization Soldevila, Mallku Ziliani, Beta Silvestre, Bruno Fridlender, Daniel Mascarenhas, Fabio Decoding Lua: formal semantics for the developer and the semanticist |
| title | Decoding Lua: formal semantics for the developer and the semanticist |
| title_full | Decoding Lua: formal semantics for the developer and the semanticist |
| title_fullStr | Decoding Lua: formal semantics for the developer and the semanticist |
| title_full_unstemmed | Decoding Lua: formal semantics for the developer and the semanticist |
| title_short | Decoding Lua: formal semantics for the developer and the semanticist |
| title_sort | decoding lua formal semantics for the developer and the semanticist |
| topic | Lua Operacional semantics PL formalization |
| url | http://hdl.handle.net/11086/552830 https://arxiv.org/abs/1706.02400v1 |
| work_keys_str_mv | AT soldevilamallku decodingluaformalsemanticsforthedeveloperandthesemanticist AT zilianibeta decodingluaformalsemanticsforthedeveloperandthesemanticist AT silvestrebruno decodingluaformalsemanticsforthedeveloperandthesemanticist AT fridlenderdaniel decodingluaformalsemanticsforthedeveloperandthesemanticist AT mascarenhasfabio decodingluaformalsemanticsforthedeveloperandthesemanticist |