UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms

Lars Brünjes, Murdoch J. Gabbay

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Downloads (Pure)

Abstract

We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020
EditorsTiziana Margaria, Bernhard Steffen
PublisherSpringer
Pages73-88
Number of pages16
ISBN (Electronic)9783030614676
ISBN (Print)9783030614669
DOIs
Publication statusPublished - 2020
Event9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020 - Rhodes, Greece
Duration: 20 Oct 202030 Oct 2020

Publication series

NameLecture Notes in Computer Science
Volume12478
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020
Abbreviated titleISoLA 2020
Country/TerritoryGreece
CityRhodes
Period20/10/2030/10/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms'. Together they form a unique fingerprint.

Cite this