Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Risk-Free Lending


view this post on Zulip Email Gateway (Sep 22 2022 at 15:19):

From: Manuel Eberl <manuel@pruvisto.org>
Risk-Free Landing

by Matthew Doty

We construct an abstract ledger supporting the risk-free lending
protocol. The risk-free lending protocol is a system for issuing and
exchanging novel financial products we call risk-free loan. The system
allows one party to lend money at 0% APY to another party in exchange
for a good or service. On every update of the ledger, accounts have
interest distributed to them. Holders of lent assets keep interest
accrued by those assets. After distributing interest, the system returns
a fixed fraction of each loan. These fixed fractions determine loan
periods. Loans for longer periods have a smaller fixed fraction
returned. Loans may be re-lent or used as collateral for other loans. We
give a sufficient criterion to enforce all accounts will forever be
solvent. We give a protocol for maintaining this invariant when
transferring or lending funds. We also show this invariant holds after
update. Even though the system does not track counter-party obligations,
we show that all credited and debited loans cancel and the monetary
supply grows at a specified interest rate.

https://www.isa-afp.org/entries/Risk_Free_Lending.html

Enjoy,

Manuel


Last updated: Mar 29 2024 at 04:18 UTC