Email Gateway (Aug 19 2022 at 16:14): Email Gateway (Aug 19 2022 at 16:14):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
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.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:21):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Nov 21 2024 at 12:39 UTC