Re: [isabelle] Some Remarks to Code Generation



Hi Florian,

>> 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.

Admittedly our pretty printing from abstract syntax to concrete SML
syntax is ad hoc at the moment. However, we do perform this
translation inside the logic, i.e. by inferences inside the logic, and
hope to prove it correct w.r.t. an SML parser function. You can find
the definition of the "dec_to_sml_string" function in the following
Lem file

https://github.com/mn200/HOL/blob/master/examples/miniML/semantics/print_ast.lem

which is used to generate the HOL4 definition. For evaluation inside
the logic, we use HOL4's standard EVAL conversion, which is not super
fast but fast enough.

My original comment was not so much to do with parsing and printing,
but more with the fact that you claim with no justification that the
semantics of "full-blown SML" matches the equational semantics of your
HRSs.

This is not to say that our work solves that problem completely
either! We worry that our MiniML semantics doesn't perfectly match
"full-blown SML". That is partly our motivation for implementing a
verified runtime for MiniML, so that we can extend this guarantee down
to the machine code (where e.g. concrete syntax is trivial).

Cheers,
Magnus





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