Re: [isabelle] Berghofer's program extraction mechanism and code generation



On Tue, 2021-02-23 at 19:08 +0100, Manuel Eberl wrote:
> One big problem is that (unless I misunderstood something) it only
> works as long as you don't use any non-constructive reasoning (i.e.
> no axiom of choice, no proof by contradiction).
>
> However, one of the big strengths of Isabelle/HOL is automation, and
> none of the automation cares about constructive vs non-constructive,
> [...]

This is ameliorated by the fact that lemmas often have no
"computational content": their proofs do not affect the extracted
program. Therefore Isabelle's automation may still be useful in
(possibly large) parts of a formalization intended for program
extraction.

Best,
Tjark









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy




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