Stream: Beginner Questions

Topic: ✔ proving the correctness of an algorithm


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Hamed Hajisadeghian (Aug 30 2021 at 18:24):

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.

view this post on Zulip Notification Bot (Aug 30 2021 at 18:24):

Hamed Hajisadeghian has marked this topic as resolved.


Last updated: Dec 07 2024 at 16:22 UTC