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



Hi,

Am Freitag, den 13.10.2017, 08:17 +0200 schrieb Andreas Lochbihler:
> 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.

cool stuff! I added a reference to the blog post.

Am Freitag, den 13.10.2017, 14:47 +0200 schrieb Lars Hupel:
> > 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.

you have a deep embedding of the extracted code equations, right? So
you could state termination, and (at least in theory) prove it in
Isabelle, couldnât you?

Joachim


-- 
Joachim Breitner
Post-Doctoral researcher
http://cis.upenn.edu/~joachim

Attachment: signature.asc
Description: This is a digitally signed message part



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