[isabelle] Semantics of code adaptations
Dear experts of the code generator,
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.
Thanks in advance for any pointers.
This archive was generated by a fusion of
Pipermail (Mailman edition) and