Offline dengan aplikasi Player FM !
Mi-Cho-Coq: Michelson formalized and applied, in Coq
Manage episode 348630439 series 2823367
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" 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.
160 episode
Manage episode 348630439 series 2823367
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" 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.
160 episode
Semua episode
×Selamat datang di Player FM!
Player FM memindai web untuk mencari podcast berkualitas tinggi untuk Anda nikmati saat ini. Ini adalah aplikasi podcast terbaik dan bekerja untuk Android, iPhone, dan web. Daftar untuk menyinkronkan langganan di seluruh perangkat.