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)
> https://www21.in.tum.de/~berghofe/papers/phd.pdf
> 
> 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
programs.

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.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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