Re: [isabelle] I/O for Imperative HOL



Am 2013-02-09 10:04, schrieb Florian Haftmann:
Hi Andreas,

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 been some work in that direction? Can anyone estimate how difficult such an
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 for writing. 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.

Lukas





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