Re: [isabelle] Where to learn about the Mini-Haskell of the code generator?



Hi Yannick,

>>> (I don't know Haskell, just SML)
>> here
>>  http://www4.informatik.tu-muenchen.de/~haftmann/pdf/code_generation_haftmann_nipkow.pdf

a good entrance point indeed

>> and probably here
>>  http://www4.informatik.tu-muenchen.de/~haftmann/pdf/codegen_hol_haftmann_phd.pdf

for some technical details, e.g. syntactic restrictions (there is a
small guide how to approach this thesis on
http://isabelle.in.tum.de/~haftmann/)

> It appears code generation is really designed towards functional
> languages

Yes.

> For other targets which are not functional languages, this may be better
> to have a model of the target, as an Isabelle theory, then prove the
> properties of a construct in that model (I don't know if “construct in
> that model” is the proper wording, may be that should be “an instance of
> that model”); then use a mapping from the modelled constructs to their
> serialization in the target language. That would rather looks like
> writing in the target language inside of Isabelle, and not be proper
> code generation from any kind of proof, but that's more safe I believe.

Code generation »as it is« is indeed based on shallow embedding.  With
some ambition this can be carried to parallel programming
(src/HOL/Library/Parallel) and imperative data structures
(src/HOL/Imperative-HOL).

> P.S. I believe
> http://www4.informatik.tu-muenchen.de/~haftmann/pdf/code_generation_haftmann_nipkow.pdf
> could be part of the standard documentations provided with the Isabelle
> package. It's both useful and good enough for that.

There are many papers with explain conceptual background of Isabelle.
Once there has been a list of them maintained by Larry Paulson, but I do
not know if it is still publicly available.  But they are accessible
through references from the official Isabelle manuals, sometimes by
direct delegation (cf. »If you consider imperative data structures as
inevitable for a specific application, you should consider […]
; the framework described there is available in session @{text
Imperative_HOL}, together with a short primer document.« in the code
generator tutorial).

Nevertheless such papers allows accumulate some dust over they years –
not wrt. to the concepts, but to the actual surface appearance in
implementation, naming, syntax etc.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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