*To*: Joachim Breitner <joachim at cis.upenn.edu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Isabelle functions: Always total, sometimes undefined*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 13 Oct 2017 08:17:04 +0200*In-reply-to*: <1507838225.1851.11.camel@cis.upenn.edu>*References*: <1507832320.1851.4.camel@cis.upenn.edu> <AM4PR0101MB2132033CB9DA7B111FE354EAB74B0@AM4PR0101MB2132.eurprd01.prod.exchangelabs.com> <1507838225.1851.11.camel@cis.upenn.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.3.0

Hi Joachim, Just two pointers on this.

https://www21.in.tum.de/~hupel/pub/isabelle-cakeml.pdf Andreas 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 declareIsabelle 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 functionsSay 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.) Greetings, Joachim

**Follow-Ups**:**Re: [isabelle] Isabelle functions: Always total, sometimes undefined***From:*Lars Hupel

**References**:**[isabelle] Isabelle functions: Always total, sometimes undefined***From:*Joachim Breitner

**Re: [isabelle] Isabelle functions: Always total, sometimes undefined***From:*Andrei Popescu

**Re: [isabelle] Isabelle functions: Always total, sometimes undefined***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Next by Date: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Previous by Thread: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Next by Thread: Re: [isabelle] Isabelle functions: Always total, sometimes undefined
- Cl-isabelle-users October 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list