Hamed Hajisadeghian (Aug 27 2021 at 14:37): Hamed Hajisadeghian (Aug 27 2021 at 14:37):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.
Robert Soeldner (Aug 29 2021 at 14:39):I found the "Concrete Semantics" book a great introduction into the topic, and its freely available http://concrete-semantics.org/index.html
Last updated: Jul 15 2022 at 23:21 UTC