English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

This article presents the formal syntax and semantics for a large subset ofthe Solidity programming language developed for the Etheruem blockchainplatform based on our resent work about developing a general, extensible, andreusable formal memory (GERM) framework and an extension of Curry-Howardisomorphism, denoted as execution-verification isomorphism (EVI). This subsetis denoted as Lolisa, which, to our knowledge, is the first mechanized andvalidated formal syntax and semantics developed for Solidity. The formal syntaxof Lolisa adopts a stronger static type system than Solidity for enhanced typesafety. In addition, Lolisa not only includes nearly all the syntax componentsof Solidity, such as mapping, modifier, contract, and address types, but italso contains general-purpose programming language features, such as multiplereturn values, pointer arithmetic, struct, and field access. Therefore, theinherent compatibility of Lolisa allows Solidity programs to be directlytranslated into Lolisa with a line-by-line correspondence without rebuilding orabstracting, and, in addition, the inherent generality of Lolisa allows it tobe extended to express other programming languages as well. To this end, wealso present a preliminary scheme for extending Lolisa to other languagessystematically.

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