A model of Solidity-style smart contracts in the theorem prover Agda - Anton Setzer (IEEE, 2023)