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

Best,
Andreas




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