Re: [isabelle] I/O for Imperative HOL
Am 2013-02-09 10:04, schrieb Florian Haftmann:
the TPHOLs 2008 paper on Imperative/HOL mentions in section 7.4 that
Imperative HOL could be extended to cover external I/O. Has there
some work in that direction? Can anyone estimate how difficult such
extension would be?
Lukas once made an attempt, but I do not know why this got stuck.
Hi Andreas, Hi Florian,
I made an attempt and succeeded. But then, we realized that you have to
think about how "large" the outside world is.
For my application, I only had two fixed files, one for reading and one
Others might want to model and reason about the whole filesystem, and
even others might want to talk about their local network, and then you
might want to even reason about the internet---I guess the world cannot
get bigger than that ;)
A polymorphic monad solution for all models is disallowed by the logic
and we did not dig deeper back then.
This archive was generated by a fusion of
Pipermail (Mailman edition) and