Imperative functional programming in Isabelle/HOL

In: Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008) (Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, and John Matthews) PDF