3 papers
cs.LO2024
Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
Mallku Soldevila, Rodrigo Ribeiro, Beta Ziliani
We propose the first steps in the development of a tool to automate the translation of Redex models into a (hopefully) semantically equivalent model in Coq, and to provide tactics…
cs.PL2020
Understanding Lua's Garbage Collection -- Towards a Formalized Static Analyzer
Mallku Soldevila, Beta Ziliani, Daniel Fridlender
We provide the semantics of garbage collection (GC) for the Lua programming language. Of interest are the inclusion of finalizers(akin to destructors in object-oriented languages)…
cs.PL2017
Decoding Lua: Formal Semantics for the Developer and the Semanticist
Mallku Soldevila, Beta Ziliani, Bruno Silvestre +2
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…