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

Hi Joachim,

Just two pointers on this.

1. CakeML has a linkup from HOL4 function definitions to their deeply embedded CakeML semantics. This linkup is used for code generation and ensures that the generated code terminates.

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. He has a draft paper on his homepage:


On 12/10/17 21:57, Joachim Breitner wrote:
Am Donnerstag, den 12.10.2017, 19:40 +0000 schrieb Andrei Popescu:
Many people will probably agree with you when you declare

Isabelle functions do not compute (unlike, say, Coq functions)

However, I think stopping at this declaration means giving up too
easily on what Isabelle/HOL (and HOL in general) have to offer w.r.t.
certified programming.

Good point. I should add  section

### You can still compute with Isabelle functions

Say you prove something about the source functions in each of these
provers. Is the fact proved in Coq more relevant for the OCaml
program than that proved in Isabelle?

The answer is: No, provided some minimal precautions are taken about
the specification and the code extraction setup. One can of course go
into a discussion about the partial correctness restriction stemming
from the additional flexibility of Isabelle/HOL's code generator
(discussed by Haftmann and Nipkow), but this can be alleviated by
removing that flexibility.

How can you achieve that?

Coq users stress the point that when you extract from Coq to Haskell,
you know it terminates. And similarly, when you translate Haskell to
Coq, and Coq accepts it, then this is in a way a termination proof of
the Haskell code.

Can we say the same for Isabelle code extraction?

(I guess we can say the same for Haskabelle translation from Haskell to
Coq, because `fun` requires well-founded recursion.)


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