How to implement and prove the correctness of an algorithm in Isabelle/HOL, specially when the algorithm is non-recursive? For example the non-recursive version of gcd algorithm.
I found the "Concrete Semantics" book a great introduction into the topic, and its freely available http://concrete-semantics.org/index.html
Robert Soeldner said:
I found the "Concrete Semantics" book a great introduction into the topic, and its freely available http://concrete-semantics.org/index.html
Thanks for your help, I'll read it.
Hamed Hajisadeghian has marked this topic as resolved.
Last updated: Dec 07 2024 at 16:22 UTC