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 gmail.com> a écrit:
On 02/07/2013 09:54 PM, Yannick Duchêne (Hibou57) wrote:
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
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and