Re: [isabelle] Source code generation/synthesis for the implementation of the algorithm that is formalized in AFP

Hi Alex,

Isabelle/HOL features a code generation facility that is able to generate executable Haskell, OCaml, Scala, and Standard ML code from many HOL definitions.  See e.g. the code generator documentation for more details:


On 31/10/2019, 10:15, "cl-isabelle-users-bounces at on behalf of Alex Meyer" <cl-isabelle-users-bounces at on behalf of alex153 at> wrote:

    AFP contains about 10 formalizations of the algorithms. Have there been attempts to generate source code in C++, Java, Haskell or similar language, so, that the generated source code implements the formalized algorithm? Maybe the generation can be with some annotation - e.g. for the single thread/CPU implemenation, for the parallel implementation of shared address space of MPI.

    I have hear, that Coq allows the generation of the Haskell code from the Coq proof of the correctness. Maybe similar efforts are possible in Isabelle as well?


IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.