Email Gateway (Aug 22 2022 at 20:41): Email Gateway (Aug 22 2022 at 20:41):From: Alex Meyer <alex153@outlook.lv>
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
Email Gateway (Aug 22 2022 at 20:41):From: Dominic Mulligan <Dominic.Mulligan@arm.com>
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
Email Gateway (Aug 22 2022 at 20:41):From: Peter Lammich <lammich@in.tum.de>
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:
http://www21.in.tum.de/~lammich/isabelle_llvm/
Last updated: Apr 23 2024 at 20:15 UTC