[isabelle] Berghofer's program extraction mechanism and code generation
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Berghofer's program extraction mechanism and code generation
- From: "Dr A. Koutsoukou-Argyraki" <ak2110 at cam.ac.uk>
- Date: Tue, 23 Feb 2021 17:56:55 +0000
- User-agent: Roundcube Webmail/1.4.11
I'm interested to understand if/how Stefan Berghofer's program
for Isabelle as developed in his PhD thesis (in the sense of obtaining
is related to the current approaches for code generation from
It would be great if you could share your insights.
Many thanks in advance!
This archive was generated by a fusion of
Pipermail (Mailman edition) and