Re: [isabelle] Isabelle functions: Always total, sometimes undefined



> 2. Lars Hupel has been working on a link from Isabelle/HOL functions to
> CakeML's semantics, using similar ideas. He is also able to generate
> CakeML code out of Isabelle/HOL function definitions. I'm not sure,
> though, whether he has also shown that all generated programs terminate.
> But the theory would definitely allow you to track that fairly easily.

I only show that all the functions that I compile terminate (a side
effect of the dictionary construction), but I haven't show total
correctness of the resulting CakeML program.

Cheers
Lars




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