I'm interested in proving correctness of the interpreter of Appel's compiler (appendix B), and compare it to the machine semantics given by Kennedy on his paper. The interpreter acts as a denotational semantics for the compiler's IR, effectively executing a syntactic object (as a datatype) and returning a computation on the host language. I have a formalization for the machine semantics already (available on GitHub), however, the algorithm is built relying on a type declared (in ML) as:
datatype dvalue = ... | FUNC of dvalue list -> answer | ...
dvalue type (which is the result type of the interpreter) includes a negative recursive occurrence, which I understand is problematic. So my question is: is there any trick that could be used to formalize the algorithm such that I could still extract executable code from it?
I mean "trick" in the same sense that we can get general recursion by using a coinductive partiality monad, which I was already planning on using anyway since the algorithm does not necessarily terminate. I could, of course, model ML on top of Coq then the algorithm on top of it, but this would be an overkill for reasoning about the algorithm, specially as the extracted code wouldn't really match the original (so I'll leave that as a plan B). Unfortunately, changing this type would deviate too much from the algorithm I'd like to verify and prove correct.
Though I'm asking particularly about Coq (as I've already a bunch of stuff formalized in there...), if this can't be done, could Agda do something like that (perhaps with guarded types)?