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:

https://isabelle.in.tum.de/doc/codegen.pdf

Thanks,
Dominic

On 31/10/2019, 10:15, "cl-isabelle-users-bounces at lists.cam.ac.uk on behalf of Alex Meyer" <cl-isabelle-users-bounces at lists.cam.ac.uk on behalf of alex153 at outlook.lv> 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.