Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Intro to Isabelle for distributed algorithms

Email Gateway (Aug 22 2022 at 21:09):

From: Martin Kleppmann <mk428@cam.ac.uk>
Dear Isabelle users,

I have recently produced some videos aimed at introducing Isabelle/HOL to software developers who have never seen a proof assistant before. The example proof in this talk is the verification of a simple consensus algorithm (a standard problem in distributed computing). I gave a 40-minute version of the talk at the industry conference Strange Loop:
https://www.youtube.com/watch?v=7w4KC6i9Yac
And I also recorded an extended 2-hour version that goes into more details of the proof:
https://www.youtube.com/watch?v=Uav5jWHNghY
I thought I'd share it on this list in case someone finds it helpful.

Regards,
Martin

Email Gateway (Aug 22 2022 at 21:10):

From: Makarius <makarius@sketis.net>
This is indeed very helpful.

See also the subsequent blog post, which I have now updated to include the
extended version from 11-Dec-2019:
https://sketis.net/2019/isabelle-as-the-worlds-most-complicated-video-game

Makarius

Last updated: Apr 20 2024 at 08:16 UTC