Based on:

Joachim Zahnentferner, 2018, May. "An Abstract Model of UTxO-based Cryptocurrencies with Scripts"

and

Joachim Zahnentferner, 2018, March. "Chimeric Ledgers: Translating and Unifying UTXO-based and Account-based Cryptocurrencies"

and

IOHK, 2019. "The Extended UTXO Ledger Model"

Browse the Agda code in HTML here.