[isabelle] I/O for Imperative HOL

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?


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