A Formalization of the Yul Language and Some Verified Yul Code Transformations
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913959694565376 |
|---|---|
| author | Coglio, Alessandro McCarthy, Eric |
| author_facet | Coglio, Alessandro McCarthy, Eric |
| contents | Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these transformations and their sequencing, we used the ACL2 theorem prover to develop a formalization of the syntax and semantics of Yul, proofs relating static and dynamic semantics, a formalization of some Yul code transformations, and correctness proofs for these transformations.
|
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_19012 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formalization of the Yul Language and Some Verified Yul Code Transformations Coglio, Alessandro McCarthy, Eric Logic in Computer Science Programming Languages Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these transformations and their sequencing, we used the ACL2 theorem prover to develop a formalization of the syntax and semantics of Yul, proofs relating static and dynamic semantics, a formalization of some Yul code transformations, and correctness proofs for these transformations. |
| title | A Formalization of the Yul Language and Some Verified Yul Code Transformations |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2507.19012 |