Re: [isabelle] Some Remarks to Code Generation



Hi Magnus,

> By the way, the last part of the following sentence from Haftmann and
> Nipkow's FLOPS'10 paper is a brave statement with no justification:
>
>   "The transformation of an intermediate program to a program in a
>    full-blown SML or Haskell-like target language is again a mere
>    syntactic adjustment and does not change the equational semantics."

here you are comparing apples with bananas.  We do not claim anything
beyond preservation of equational semantics, and argue that our abstract
intermediate language is appropriately close to ML or Haskell such that
the final transition »only« involves turning abstract into concrete
syntax, but no transformations introducing new equations etc.  This,
naturally, is technically involved, but if I have a look at your
reference, it also admits that a formal treatment of this is beyond scope:

> We have not attempted to solve the problem of verified
> parsing or pretty printing.

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.