  The Ethereum platform supports the decentralized execution of smart
contracts, i.e. computer programs that transfer digital assets between users.
The most common language used to develop these contracts is Solidity, a
Javascript-like language which compiles into EVM bytecode, the language
actually executed by Ethereum nodes. While much research has addressed the
formalisation of the semantics of EVM bytecode, relatively little attention has
been devoted to that of Solidity. In this paper we propose a minimal calculus
for Solidity contracts, which extends an imperative core with a single
primitive to transfer currency and invoke contract procedures. We build upon
this formalisation to give semantics to the Ethereum blockchain. We show our
calculus expressive enough to reason about some typical quirks of Solidity,
like e.g. re-entrancy.
