UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms

Lars Brünjes; Murdoch J. Gabbay

doi:10.1007/978-3-030-61467-6_6

UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms

Lars Brünjes, Murdoch J. Gabbay^*

^*Corresponding author for this work

IOHK

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 Citations (Scopus)

31 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 language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer
Pages	73-88
Number of pages	16
ISBN (Electronic)	9783030614676
ISBN (Print)	9783030614669
DOIs	https://doi.org/10.1007/978-3-030-61467-6_6
Publication status	Published - 2020
Event	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020 - Rhodes, Greece Duration: 20 Oct 2020 → 30 Oct 2020

Publication series

Name	Lecture Notes in Computer Science
Volume	12478
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020
Abbreviated title	ISoLA 2020
Country/Territory	Greece
City	Rhodes
Period	20/10/20 → 30/10/20

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-030-61467-6_6

Download pdf
The final authenticated version is available online at https://doi.org/10.1007/978-3-030-61467-6_6
Accepted author manuscript, 215 KB

https://arxiv.org/abs/2003.14271

Cite this

@inproceedings{01b1200d0d7c4699a01c34fcf6d60cfe,

title = "UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms",

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.",

author = "Lars Br{\"u}njes and Gabbay, {Murdoch J.}",

year = "2020",

doi = "10.1007/978-3-030-61467-6_6",

language = "English",

isbn = "9783030614669",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "73--88",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020",

note = "9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020, ISoLA 2020 ; Conference date: 20-10-2020 Through 30-10-2020",

}

Brünjes, L & Gabbay, MJ 2020, UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020. Lecture Notes in Computer Science, vol. 12478, Springer, pp. 73-88, 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020, Rhodes, Greece, 20/10/20. https://doi.org/10.1007/978-3-030-61467-6_6

UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms. / Brünjes, Lars; Gabbay, Murdoch J.

Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020. ed. / Tiziana Margaria; Bernhard Steffen. Springer, 2020. p. 73-88 (Lecture Notes in Computer Science; Vol. 12478).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms

AU - Brünjes, Lars

AU - Gabbay, Murdoch J.

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85096504298&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-61467-6_6

DO - 10.1007/978-3-030-61467-6_6

M3 - Conference contribution

AN - SCOPUS:85096504298

SN - 9783030614669

T3 - Lecture Notes in Computer Science

SP - 73

EP - 88

BT - Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

T2 - 9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation 2020

Y2 - 20 October 2020 through 30 October 2020

ER -

UTxO- vs Account-Based Smart Contract Blockchain Programming Paradigms

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this