Stream: Beginner Questions

Topic: Sources for Isabelle knowledge

Gergely Buday (Aug 14 2023 at 09:46):

I have collected some sources for Isabelle knowledge:

• The docs in the distribution: Isabelle/Isar Reference Manual etc, including the old Tutorial
• Concrete Semantics Part I
• The code base of the distribution and of the Archive of Formal Proofs
• The Isabelle Community Cookbook
• The Isabelle Community Wiki
• The Isabelle Programming Tutorial by Christian Urban et al
• The Proofcraft Blog
• Blumson's Isabelle for Philosopers
• Breitner's Theorem Beweiser Praktikum
• Interactive Theorem Proving using Isabelle/HOL at Innsbruck
• Isabelle/HOL Exercises at TU Munich
• The archives of the Isabelle mailing list and of Isabelle Zulipchat
• The Serapis search engine
• Correctness Proofs of Distributed Systems with Isabelle, a talk by Martin Klepmann
  

I would love to hear additions to this list.

Wenda Li (Aug 14 2023 at 16:28):

Thanks for compiling this handy list! I am additionally considering:

• The MPhil course material delivered by Larry Paulson at Cambridge
• An introductory book to Isabelle in Chinese by Prof. Yongwang ZHAO.

Gergely Buday (Aug 16 2023 at 09:34):

@Wenda Li I tried to translate the Chinese book into English by Google Translate: it did translate the table of contents well, but failed to do that for the actual content. Even when I try to translate an individual page, it does not work. Do you know of a service that translates the book to English?

Wenda Li (Aug 16 2023 at 09:59):

@Gergely Buday I am afraid that I don't know any good systems for translating a whole book. Auto-translation of academic books/papers always appears to be challenging to me, as jargons and subtle nuances can lead to a lot of confusion...

I pointed to the book in case the user is more comfortable with Chinese. Nevertheless, I believe most of the content have also been covered by other materials (e.g., Concrete Semantics).

Gergely Buday (Aug 17 2023 at 07:57):

By chance, I have found the following draft:

Learn Mathematics and Computer Science with Isabelle

Gergely Buday (Aug 30 2023 at 08:04):

And the course Automated Reasoning by Jacques Fleuriot

Last updated: Apr 28 2024 at 12:28 UTC