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

> 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)
> is related to the current approaches for code generation from Isabelle/HOL.

Note that code generation using extraction from proofs works in two steps:

a) The extraction part: Turning a proof into a set of definitions and
corresponding equational theorems in Isabelle/HOL

b) The code generation part: Turning those theorems into executable

Hence there is no fundamental difference: both approaches rely on a
regular code generator, although that has been replaced in the meantime.

Personally I tend to view proof terms in Isabelle as a device to bolster
the logical foundations.  The code generation examples in the
distributions are nice demonstrations – but the mechanism so far has no
impact on practical applications.


Attachment: signature.asc
Description: OpenPGP digital signature

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