6 citations · 6 across the 4 of their papers we have counts for
Showing 2021Show all
2 papers · 1 filter
cs.LO2021
Money grows on (proof-)trees: the formal FA1.2 ledger standard
Murdoch Gabbay, Arvid Jakobsson, Kristina Sojakova
Once you have invented digital money, you may need a ledger to track who owns what -- and an interface to that ledger so that users of your money can transact. On the Tezos blockch…
cs.LO2021
Syllepsis in Homotopy Type Theory
Kristina Sojakova
It is well-known that in homotopy type theory (HoTT), one can prove the Eckmann-Hilton theorem: given two 2-loops p, q : 1 = 1 on the reflexivity path at an arbitrary point a : A,…