Stream: Isabelle/ML

Topic: Isar Virtual Machine

view this post on Zulip Gergely Buday (Mar 27 2023 at 15:45):

The Isabelle/Isar Implementation manual on page 130 writes:

Adding to the genuine structured proof language requires profound understanding of the Isar/VM machinery, though, so this is beyond the scope of this manual.

While I do not want to add new elements to the language, I would like to understand the virtual machine well. What is the source for that? Isar source code and Makarius' PhD Thesis?

view this post on Zulip Manuel Eberl (Mar 29 2023 at 09:54):

I would ask such questions on the mailing list. Probably only Makarius knows about this, and he doesn't read Zulip.

view this post on Zulip Gergely Buday (Mar 29 2023 at 14:11):

Thanks, that's a reasonable suggestion.

Last updated: Dec 07 2023 at 16:21 UTC