Re: [isabelle] Semantics of code adaptations

Hi Andreas,

> I am looking for a (formal) semantics of the adaptation facilities that
> the code generator offers. I am aware of the correctness proof for the
> dictionary construction in Florian's and Tobias' FLOPS 2010 paper (which
> essentially summarises Florian's PhD thesis) and the correctness proof
> for the subtype translation (code abstract) in the data refinement paper
> at ITP 2013. As I understand it, both take a closed-world perspective in
> that they assume that the code generator generates everything and
> nothing is serialised to target-language primitives (list, option,
> boolean, ...). So I am wondering whether there has been given some
> rigorous thought on the (formal) conditions on the adaptations that make
> these correctness guarantees extend to code serialised with adaptations
> in place.

indeed, there are no formal pointers whatsoever on adaptation.
Informally, there is the idea of adaptations describing an isomorphism, e.g.

  bool <-> bool
  True <-> true
  False <-> false

Advanced instances of adaptation (e.g. numerals) are already more involved.

What is done in Imperative-HOL is yet another story.

I admit that in presence of abstract datatypes things get more delicate
also.  But to approach a more rigorous treatment of adaptations, we
would need a more abstract technical serialization stack: not directly
going from IML to, say, SML, but first to an abstract syntax tree on
which certain well-understood transformations can be carried out.

When starting the code generator business almost one decade ago, I
refrained from having such a full-blown stack: on the one hand side, it
would be conceptually clearer, but from a practical point of view it
would introduce yet another layer of trusted code – unless the
transition IML -> abstract syntax tree is bolstered somehow.

Maybe Lars Hupel can tell whether his work can contribute here.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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