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


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:

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here:

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