Title: Ledger Theory Coq Development Post by: HostFat on February 08, 2015, 09:57:09 PM https://github.com/billlwhite/ledgertheory
Ledger Theory Coq Development This repository contains a Coq development of a theory of lightweight cryptographic ledgers. The files should be compiled in the following order (see also the file coqcompile): Prelude.v Addrs.v CryptoHashes.v CryptoSignatures.v Assets.v Transactions.v LedgerStates.v MTrees.v CTrees.v CTreeGrafting.v Blocks.v White Paper There is also a white paper lightcrypto.pdf providing a high level description and overview of what is here. More detailed descriptions of the various parts will hopefully be written soon. https://github.com/billlwhite/ledgertheory/blob/master/lightcrypto.pdf Quote Abstract We present representations for cryptographic ledgers which do not require storing excessive information about transaction histories. Such representations may allow for the creation of cryptocurrencies which do not suffer from so-called “block chain bloat.” A corresponding theory has been formalized in the proof assistant Coq. We give a high level description and a simplified example. We then give some of the main definitions and theorems which can be found in the formal development. I'm not the author Title: Re: Ledger Theory Coq Development Post by: ffe on February 10, 2015, 06:32:33 PM Still reading through this and so far it's very interesting but I wanted to make one comment. The paper should make clear up front that your use of the term "forge" is related to mining a block and not related to creating an illegal block. You mean forge as in create not forgery.
Title: Re: Ledger Theory Coq Development Post by: tzpardi on February 11, 2015, 11:58:11 AM This seems really interesting.
Title: Re: Ledger Theory Coq Development Post by: kanzure on June 19, 2016, 04:41:08 PM Above hyperlink is 404, an alternative link seems to be https://github.com/bitemyapp/ledgertheory
|