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



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



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