EPISODE · Dec 2, 2022 · 15 MIN
Mi-Cho-Coq: Michelson formalized and applied, in Coq
from Iowa Type Theory Commute · host Aaron Stump
In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for CertifyingTezos Smart Contracts", by Bernardo et al. The paper gives a nice and very clear introduction to the Michelson language, and a formalization of it in Coq. This is used to prove a correctness property about a Multisig contract.I also kindly solicit your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout. To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science. Select the Computer Science Development Fund, College of Liberal Arts and Sciences. Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump. Sorry it's that complicated.
Embed this episode
What this episode covers
In this episode, I discuss this paper, "Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts", by Bernardo et al. The paper gives a nice and very clear introduction to the Michelson language, and a formalization of it in Coq. This is used to prove a correctness property about a Multisig contract. I also kindly solicit your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout. To donate, click here, and then under "Gift details" s...
NOW PLAYING
Mi-Cho-Coq: Michelson formalized and applied, in Coq
No transcript for this episode yet
Similar Episodes
No similar episodes found.
Similar Podcasts
No similar podcasts found.