Lolisa: Formal syntax and semantics for a subset of the solidity programming language in Mathematical Tool Coq

Understand

This article presents the formal syntax and semantics for a large subset of the Solidity programming language developed for the Etheruem blockchain platform based on our resent work about developing a general, extensible, and reusable formal memory (GERM) framework and an extension of Curry-Howard isomorphism, denoted as execution-verification isomorphism (EVI).

• This subset is denoted as Lolisa, which, to our knowledge, is the first mechanized and validated formal syntax and semantics developed for Solidity.
• The formal syntax of Lolisa adopts a stronger static type system than Solidity for enhanced type safety.
• In addition, Lolisa not only includes nearly all the syntax components of Solidity, such as mapping, modifier, contract, and address types, but it also contains general-purpose programming language features, such as multiple return values, pointer arithmetic, struct, and field access.