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

Le Thu, 07 Feb 2013 14:19:13 +0100, Christian Sternagel <c.sternagel at> a écrit:

On 02/07/2013 09:54 PM, Yannick Duchêne (Hibou57) wrote:
Hi people,

The codegen.pdf document, says a single translations occurs before
serialization to a target language. This prior translation is said to
have a single target of its own: a kind of Mini-Haskell.

Is this Mini-Haskell described in some official or unofficial documents?
(I don't know Haskell, just SML)

and probably here

(I did not check, though)

I had a check. Seems to me the first former is the most relevant.

It appears code generation is really designed towards functional languages, which is not easily suitable for procedural and automata languages, even if those can of course be expressed in terms of lambda calculus.

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.

Any comments welcome.

P.S. I believe could be part of the standard documentations provided with the Isabelle package. It's both useful and good enough for that.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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