Concrete Semantics with Isabelle/HOL
concrete-semantics.org
concrete-semantics.org
Its a fascinating introduction into general program semantics, formal analyses and proofs for program properties. During the lecture I struggled somewhat as I didn‘t really have sufficient background knowledge for it to run smoothly. But all the concepts are supported by, well, concrete examples which you can immediately try to solve in Isabelle. So I definitely recommend giving it a go!
It was an eye-opening experience for me, especially since I never really looked into formal program analysis.
What's the difference between TLA+, Coq & Isabelle?
Is there one should I prefer over the other? Or do they individualy satisfy distinctive purposes?
I really wish Coq had equally powerful automation tools and a more intuitive proof language, because it feels much more of a solid language and I really liked that the clear relation of types <-> statements, terms <-> proofs, type checking <-> proof verification; including the ability to print the raw proof terms of theorems.
Concrete?
• The book shows that a semantics is not a collection of abstract symbols on sheets of paper but formal text that can be checked and executed by the computer: Isabelle is also a programming environment and most of the definitions in the book are executable and can even be exported as programs in a number of (functional) programming languages. For a computer scientist, this is as concrete as it gets.
• Much of the book deals with concrete applications of semantics: compilers, type systems, program analysers.
• The predominant formalism in the book is operational semantics, the most concrete of the various forms of semantics.
• Foundations are made of concrete.