Preventing Out-of-Gas Exceptions by Typing
<|reference_start|>Preventing Out-of-Gas Exceptions by Typing: We continue the development of TinySol, a minimal object-oriented language based on Solidity, the standard smart-contract language used for the Ethereum platform. We first extend TinySol with exceptions and a gas mechanism, and equip it with a small-step operational semantics. Introducing the gas mechanism is fundamental for modelling real-life smart contracts in TinySol, since this is the way in which termination of Ethereum smart contracts is usually ensured. We then devise a type system for smart contracts guaranteeing that such programs never run out of gas at runtime. This is a desirable property for smart contracts, since a transaction that runs out of gas is aborted, but the price paid to run the code is not returned to the invoker.<|reference_end|>
@article{aceto2024preventing,
    title={Preventing Out-of-Gas Exceptions by Typing},
    author={Luca Aceto, Daniele Gorla, Stian Lybech, Mohammad Hamdaqa},
    journal={arXiv preprint arXiv:2407.15676},
    year={2024},
    archivePrefix={arXiv},
    eprint={2407.15676},
    primaryClass={cs.PL}
}