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

["Dr A. Koutsoukou-Argyraki" <ak2110 at cam.ac.uk>]

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