Email Gateway (Aug 19 2022 at 10:03): Email Gateway (Aug 19 2022 at 10:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
Lukas once made an attempt, but I do not know why this got stuck.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 10:07):From: Lukas Bulwahn <bulwahn@in.tum.de>
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
Email Gateway (Aug 19 2022 at 10:24):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
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?
Andreas
Last updated: Apr 30 2024 at 12:28 UTC