[isabelle] Berghofer's program extraction mechanism and code generation



Dear all,

I'm interested to understand if/how Stefan Berghofer's program extraction mechanism for Isabelle as developed in his PhD thesis (in the sense of obtaining realizers)
https://www21.in.tum.de/~berghofe/papers/phd.pdf

is related to the current approaches for code generation from Isabelle/HOL.

It would be great if you could share your insights.

Many thanks in advance!
Angeliki





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