DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2025.10

Program Logics for Ledgers

Authors: Orestis Melkonian, Wouter Swierstra, and James Chapman

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract

Distributed ledgers nowadays manage substantial monetary funds in the form of cryptocurrencies such as Bitcoin, Ethereum, and Cardano. For such ledgers to be safe, operations that add new entries must be cryptographically sound - but it is less clear how to reason effectively about such ever-growing linear data structures. This paper demonstrates how distributed ledgers may be viewed as computer programs, that, when executed, transfer funds between various parties. As a result, familiar program logics, such as Hoare logic, are applied in a novel setting. Borrowing ideas from concurrent separation logic, this enables modular reasoning principles over arbitrary fragments of any ledger. All of our results have been mechanised in the Agda proof assistant.

Cite as

Orestis Melkonian, Wouter Swierstra, and James Chapman. Program Logics for Ledgers. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{melkonian_et_al:OASIcs.FMBC.2025.10,
  author =	{Melkonian, Orestis and Swierstra, Wouter and Chapman, James},
  title =	{{Program Logics for Ledgers}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{10:1--10:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.10},
  URN =		{urn:nbn:de:0030-drops-230370},
  doi =		{10.4230/OASIcs.FMBC.2025.10},
  annote =	{Keywords: blockchain, distributed ledgers, UTxO separation logic, program semantics, formal verification, Agda}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2015.9

Pi-Ware: Hardware Description and Verification in Agda

Authors: João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling

Published in: LIPIcs, Volume 69, 21st International Conference on Types for Proofs and Programs (TYPES 2015) (2018)

Abstract

There is a long tradition of modelling digital circuits using functional programming languages. This paper demonstrates that by employing dependently typed programming languages, it becomes possible to define circuit descriptions that may be simulated, tested, verified and synthesized using a single language. The resulting domain specific embedded language, Pi-Ware, makes it possible to define and verify entire families of circuits at once. We demonstrate this by defining an algebra of parallel prefix circuits, proving their correctness and further algebraic properties.

Cite as

João Paulo Pizani Flor, Wouter Swierstra, and Yorick Sijsling. Pi-Ware: Hardware Description and Verification in Agda. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 9:1-9:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{pizaniflor_et_al:LIPIcs.TYPES.2015.9,
  author =	{Pizani Flor, Jo\~{a}o Paulo and Swierstra, Wouter and Sijsling, Yorick},
  title =	{{Pi-Ware: Hardware Description and Verification in Agda}},
  booktitle =	{21st International Conference on Types for Proofs and Programs (TYPES 2015)},
  pages =	{9:1--9:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-030-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{69},
  editor =	{Uustalu, Tarmo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2015.9},
  URN =		{urn:nbn:de:0030-drops-84791},
  doi =		{10.4230/LIPIcs.TYPES.2015.9},
  annote =	{Keywords: dependently typed programming, Agda, EDSL, hardware description languages, functional programming}
}

Search Results

Documents authored by Swierstra, Wouter

Program Logics for Ledgers

Abstract

Cite as

Pi-Ware: Hardware Description and Verification in Agda

Abstract

Cite as

Thanks for your feedback!

Could not send message