Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Imperative Refinement Fram...


view this post on Zulip Email Gateway (Aug 22 2022 at 13:57):

From: Lawrence Paulson <lp15@cam.ac.uk>
Another AFP entry for today: The Imperative Refinement Framework by Peter Lammich: "a tool that supports a stepwise refinement based approach to imperative programs…. It uses the Monadic Refinement Framework as a frontend for the specification of the abstract programs, and Imperative/HOL as a backend to generate executable imperative programs"

More info here: https://www.isa-afp.org/entries/Refine_Imperative_HOL.shtml

Larry Paulson


Last updated: Apr 26 2024 at 16:20 UTC