bitemyapp / Ledgertheory
Licence: other
Stars: ✭ 12
Labels
Projects that are alternatives of or similar to Ledgertheory
Micro Policies Coq
Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors
Stars: ✭ 18 (+50%)
Mutual labels: coq
Monads
Coq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-25%)
Mutual labels: coq
Unimath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Stars: ✭ 680 (+5566.67%)
Mutual labels: coq
Finset
A Coq library for extensional finite sets and comprehension
Stars: ✭ 6 (-50%)
Mutual labels: coq
Verdi
A framework for formally verifying distributed systems implementations in Coq
Stars: ✭ 496 (+4033.33%)
Mutual labels: coq
Category Theory
An axiom-free formalization of category theory in Coq for personal study and practical work
Stars: ✭ 562 (+4583.33%)
Mutual labels: coq
Software Foundations
Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
Stars: ✭ 9 (-25%)
Mutual labels: coq
Autosubst
Automation for de Bruijn syntax and substitution in Coq
Stars: ✭ 22 (+83.33%)
Mutual labels: coq
Stalin Sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+7133.33%)
Mutual labels: coq
Dblib Linear
Formalisation of the linear lambda calculus in Coq
Stars: ✭ 10 (-16.67%)
Mutual labels: coq
Cufp 2015 Tutorial
An introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (-25%)
Mutual labels: coq
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.
License
This is all being released as open source under the MIT/X11 software license. See http://www.opensource.org/licenses/mit-license.php This is also in the file LICENSE along with a bitcoin signature of the license.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].