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

Hi Alex,

actually, many of the algorithms formalised in the AFP already contain
code generator setup, and can be readily exported to various
(functional) languages, i.e., Haskell, Scala, OCaml, and SML.

More recently, also support for exporting to LLVM-IR is available,
though not (yet) in the AFP:


On Thu, 2019-10-31 at 10:31 +0000, Dominic Mulligan wrote:
> 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:
> Thanks,
> Dominic
> 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?
>     Alex
> 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.