diff --git a/thys/Hello_World/HelloWorld.thy b/thys/Hello_World/HelloWorld.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hello_World/HelloWorld.thy
@@ -0,0 +1,56 @@
+theory HelloWorld
+  imports IO
+begin
+
+section\<open>Hello, World!\<close>
+
+text\<open>
+  The idea of a \<^term>\<open>main :: unit io\<close> function is that, upon start of your program, you will be
+  handed a value of type \<^typ>\<open>\<^url>\<close>. You can pass this world through your code and modify it.
+  Be careful with the \<^typ>\<open>\<^url>\<close>, it's the only one we have.
+\<close>
+
+
+text\<open>The main function, defined in Isabelle. It should have the right type in Haskell.\<close>
+definition main :: "unit io" where
+  "main \<equiv> do {
+               _ \<leftarrow> println (STR ''Hello World! What is your name?'');
+               name \<leftarrow> getLine;
+               println (STR ''Hello, '' + name + STR ''!'')
+             }"
+
+
+section\<open>Generating Code\<close>
+
+text\<open>Checking that the generated code compiles.\<close>
+export_code main checking Haskell? SML
+
+
+ML_val\<open>Isabelle_System.bash "echo ${ISABELLE_TMP} > ${ISABELLE_TMP}/self"\<close>
+text\<open>
+During the build of this session, the code generated in the following subsections will be
+written to
+\<close>
+text_raw\<open>\verbatiminput{${ISABELLE_TMP}/self}\<close>
+
+
+subsection\<open>Haskell\<close>
+
+export_code main in Haskell file "$ISABELLE_TMP/exported_hs"
+
+text\<open>The generated helper module \<^file>\<open>$ISABELLE_TMP/exported_hs/StdIO.hs\<close> is shown below.\<close>
+text_raw\<open>\verbatiminput{$ISABELLE_TMP/exported_hs/StdIO.hs}\<close>
+ 
+text\<open>The generated main file \<^file>\<open>$ISABELLE_TMP/exported_hs/HelloWorld.hs\<close> is shown below.\<close>
+text_raw\<open>\verbatiminput{$ISABELLE_TMP/exported_hs/HelloWorld.hs}\<close>
+
+
+subsection\<open>SML\<close>
+
+export_code main in SML file "$ISABELLE_TMP/exported.sml"
+
+text\<open>The generated SML code in \<^file>\<open>$ISABELLE_TMP/exported.sml\<close> is shown below.\<close>
+text_raw\<open>\verbatiminput{$ISABELLE_TMP/exported.sml}\<close>
+
+
+end
\ No newline at end of file
diff --git a/thys/Hello_World/HelloWorld_Proof.thy b/thys/Hello_World/HelloWorld_Proof.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hello_World/HelloWorld_Proof.thy
@@ -0,0 +1,73 @@
+theory HelloWorld_Proof
+  imports HelloWorld
+begin
+
+section\<open>Correctness\<close>
+
+
+subsection\<open>Modeling Input and Output\<close>
+
+text\<open>
+  With the appropriate assumptions about \<^const>\<open>println\<close> and \<^const>\<open>getLine\<close>,
+  we can even prove something.
+  We summarize our model about input and output in the assumptions of a \<^theory_text>\<open>locale\<close>.
+\<close>
+locale io_stdio =
+  \<comment> \<open>We model \<^verbatim>\<open>STDIN\<close> and \<^verbatim>\<open>STDOUT\<close> as part of the \<^typ>\<open>\<^url>\<close>.
+     Note that we know nothing about \<^typ>\<open>\<^url>\<close>,
+     we just model that we can find \<^verbatim>\<open>STDIN\<close> and \<^verbatim>\<open>STDOUT\<close> somewhere in there.\<close>
+  fixes stdout_of::"\<^url> \<Rightarrow> string list"
+  and stdin_of::"\<^url> \<Rightarrow> string list"
+
+  \<comment> \<open>Assumptions about \<^verbatim>\<open>STDIN\<close>:
+      Calling \<^const>\<open>println\<close> appends to the end of \<^verbatim>\<open>STDOUT\<close> and \<^const>\<open>getLine\<close> does not change
+      anything.\<close>
+assumes stdout_of_println[simp]:
+    "stdout_of (exec (println str) world) = stdout_of world@[String.explode str]"
+  and stdout_of_getLine[simp]:
+    "stdout_of (exec getLine world) = stdout_of world"
+
+  \<comment> \<open>Assumptions about \<^verbatim>\<open>STDIN\<close>:
+      Calling \<^const>\<open>println\<close> does not change anything and \<^const>\<open>getLine\<close> removes the first element
+      from the \<^verbatim>\<open>STDIN\<close> stream.\<close>
+  and stdin_of_println[simp]:
+    "stdin_of (exec (println str) world) = stdin_of world"
+  and stdin_of_getLine:
+    "stdin_of world = inp#stdin \<Longrightarrow>
+     stdin_of (exec getLine world) = stdin \<and> eval getLine world = String.implode inp"
+begin
+end
+
+
+subsection\<open>Correctness of Hello World\<close>
+
+text\<open>Correctness of \<^const>\<open>main\<close>:
+    If \<^verbatim>\<open>STDOUT\<close> is initially empty and only \<^term>\<open>''corny''\<close> will be typed into \<^verbatim>\<open>STDIN\<close>,
+    then the program will output: \<^term>\<open>[''Hello World! What is your name?'', ''Hello, corny!'']\<close>.
+  \<close>
+theorem (in io_stdio)
+  assumes stdout: "stdout_of world = []"
+       and stdin: "stdin_of world = [''corny'']"
+     shows "stdout_of (exec main world) =
+              [''Hello World! What is your name?'',
+               ''Hello, corny!'']"
+proof -
+  let ?world1="exec (println (STR ''Hello World! What is your name?'')) world"
+  have stdout_world2:
+    "literal.explode STR ''Hello World! What is your name?'' =
+     ''Hello World! What is your name?''"
+    by code_simp
+  from stdin_of_getLine[where stdin="[]", OF stdin] have stdin_world2:
+    "eval getLine ?world1 = String.implode ''corny''"
+    by (simp add: stdin_of_getLine stdin)
+  show ?thesis
+    unfolding main_def
+    apply(simp add: exec_bind)
+    apply(simp add: stdout)
+    apply(simp add: stdout_world2 stdin_world2)
+    apply(simp add: plus_literal.rep_eq)
+    apply code_simp
+    done
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Hello_World/IO.thy b/thys/Hello_World/IO.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hello_World/IO.thy
@@ -0,0 +1,272 @@
+theory IO
+  imports
+    Main
+    "HOL-Library.Monad_Syntax"
+begin
+
+section\<open>IO Monad\<close>
+text \<open>
+  Inspired by Haskell.
+  Definitions from \<^url>\<open>https://wiki.haskell.org/IO_inside\<close>
+\<close>
+
+subsection\<open>Real World\<close>
+text \<open>
+  We model the real world with a fake type.
+
+  WARNING:
+    Using low-level commands such as \<^theory_text>\<open>typedecl\<close> instead of high-level \<^theory_text>\<open>datatype\<close> is dangerous.
+    We explicitly use a \<^theory_text>\<open>typedecl\<close> instead of a \<^theory_text>\<open>datatype\<close> because we never want to instantiate
+    the world. We don't need a constructor, we just need the type.
+
+  The following models an arbitrary type we cannot reason about.
+  Don't reason about the complete world! Only write down some assumptions about parts of the world.
+\<close>
+typedecl real_world (\<open>\<^url>\<close>)
+
+text\<open>
+  For examples, see \<^file>\<open>HelloWorld_Proof.thy\<close>.
+  In said theory, we model \<^verbatim>\<open>STDIN\<close> and \<^verbatim>\<open>STDOUT\<close> as parts of the world and describe how this part
+  of the wold can be affected. We don't model the rest of the world. This allows us to reason about
+  \<^verbatim>\<open>STDIN\<close> and \<^verbatim>\<open>STDOUT\<close> as part of the world, but nothing more.
+\<close>
+
+
+subsection\<open>IO Monad\<close>
+text \<open>
+  The set of all functions which take a \<^typ>\<open>\<^url>\<close> and return an \<^typ>\<open>'\<alpha>\<close> and a \<^typ>\<open>\<^url>\<close>.
+
+  The rough idea of all IO functions is the following: You are given the world in its current state.
+  You can do whatever you like to the world. You can produce some value of type \<^typ>\<open>'\<alpha>\<close> and you
+  have to return the modified world.
+
+  For example, the \<^verbatim>\<open>main\<close> function is Haskell does not produce a value, therefore, \<^verbatim>\<open>main\<close> in
+  Haskell is of type \<^verbatim>\<open>IO ()\<close>. Another example in Haskell is \<^verbatim>\<open>getLine\<close>, which returns \<^verbatim>\<open>String\<close>.
+  It's type in Haskell is \<^verbatim>\<open>IO String\<close>. All those functions may also modify the state of the world.
+\<close>
+
+typedef '\<alpha> io = "UNIV :: (\<^url> \<Rightarrow> '\<alpha> \<times> \<^url>) set"
+proof -
+  show "\<exists>x. x \<in> UNIV" by simp
+qed
+
+text \<open>
+  Related Work:
+  \<^emph>\<open>Programming TLS in Isabelle/HOL\<close> by Andreas Lochbihler and Marc Züst uses a partial function
+  (\<open>\<rightharpoonup>\<close>).
+  \<^theory_text>\<open>
+    typedecl real_world
+    typedef '\<alpha> io = "UNIV :: (\<^url> \<rightharpoonup> '\<alpha> \<times> \<^url>) set" by simp
+  \<close>
+  We use a total function. This implies the dangerous assumption that all IO functions are total
+  (i.e., terminate).
+\<close>
+
+text \<open>
+  The \<^theory_text>\<open>typedef\<close> above gives us some convenient definitions.
+  Since the model of \<^typ>\<open>'\<alpha> io\<close> is just a mode, those definitions should not end up in generated
+  code.
+\<close>
+term Abs_io \<comment> \<open>Takes a \<^typ>\<open>(\<^url> \<Rightarrow> '\<alpha> \<times> \<^url>)\<close> and abstracts it to an \<^typ>\<open>'\<alpha> io\<close>.\<close>
+term Rep_io \<comment> \<open>Unpacks an \<^typ>\<open>'\<alpha> io\<close> to a \<^typ>\<open>(\<^url> \<Rightarrow> '\<alpha> \<times> \<^url>)\<close>\<close>
+
+
+subsection\<open>Monad Operations\<close>
+text\<open>
+  Within an \<^typ>\<open>'\<alpha> io\<close> context, execute \<^term>\<open>action\<^sub>1\<close> and \<^term>\<open>action\<^sub>2\<close> sequentially.
+  The world is passed through and potentially modified by each action.
+\<close>
+definition bind :: "'\<alpha> io \<Rightarrow> ('\<alpha> \<Rightarrow> '\<beta> io) \<Rightarrow> '\<beta> io" where [code del]:
+  "bind action\<^sub>1 action\<^sub>2 = Abs_io (\<lambda>world\<^sub>0.
+                                  let (a, world\<^sub>1) = (Rep_io action\<^sub>1) world\<^sub>0;
+                                      (b, world\<^sub>2) = (Rep_io (action\<^sub>2 a)) world\<^sub>1
+                                  in (b, world\<^sub>2))"
+
+text \<open>
+  In Haskell, the definition for \<^verbatim>\<open>bind\<close> (\<^verbatim>\<open>>>=\<close>) is:
+  \<^verbatim>\<open>
+    (>>=) :: IO a -> (a -> IO b) -> IO b
+    (action1 >>= action2) world0 =
+       let (a, world1) = action1 world0
+           (b, world2) = action2 a world1
+       in (b, world2)
+  \<close>
+\<close>
+
+hide_const (open) bind
+adhoc_overloading bind IO.bind
+
+text \<open>Thanks to \<^theory_text>\<open>adhoc_overloading\<close>, we can use monad syntax.\<close>
+lemma "bind (foo :: '\<alpha> io) (\<lambda>a. bar a) = foo \<bind> (\<lambda>a. bar a)"
+  by simp
+
+
+definition return :: "'\<alpha> \<Rightarrow> '\<alpha> io" where [code del]:
+  "return a \<equiv> Abs_io (\<lambda>world. (a, world))"
+
+hide_const (open) return
+
+text \<open>
+  In Haskell, the definition for \<^verbatim>\<open>return\<close> is::
+  \<^verbatim>\<open>
+    return :: a -> IO a
+    return a world0  =  (a, world0)
+  \<close>
+\<close>
+
+
+subsection\<open>Monad Laws\<close>
+lemma left_id:
+  fixes f :: "'\<alpha> \<Rightarrow> '\<beta> io" \<comment> \<open>Make sure we use our \<^const>\<open>IO.bind\<close>.\<close>
+  shows "(IO.return a \<bind> f) = f a"
+  by(simp add: return_def IO.bind_def Abs_io_inverse Rep_io_inverse)
+
+lemma right_id:
+  fixes m :: "'\<alpha> io" \<comment> \<open>Make sure we use our \<^const>\<open>IO.bind\<close>.\<close>
+  shows "(m \<bind> IO.return) = m"
+  by(simp add: return_def IO.bind_def Abs_io_inverse Rep_io_inverse)
+    
+lemma bind_assoc:
+  fixes m :: "'\<alpha> io" \<comment> \<open>Make sure we use our \<^const>\<open>IO.bind\<close>.\<close>
+  shows "((m \<bind> f) \<bind> g) = (m \<bind> (\<lambda>x. f x \<bind> g))"
+  by(simp add: IO.bind_def Abs_io_inverse Abs_io_inject fun_eq_iff split: prod.splits)
+
+
+subsection\<open>Code Generator Setup\<close>
+text \<open>
+  We don't expose our \<^const>\<open>IO.bind\<close> definition to code.
+  We use the built-in definitions of the target language (e.g., Haskell, SML).
+\<close>
+code_printing constant IO.bind \<rightharpoonup> (Haskell) "_ >>= _"
+                                  and (SML) "bind"
+            | constant IO.return \<rightharpoonup> (Haskell) "return"
+                                    and (SML) "(() => _)"
+
+text\<open>SML does not come with a bind function. We just define it (hopefully correct).\<close>
+code_printing code_module Bind \<rightharpoonup> (SML) \<open>
+fun bind x f () = f (x ()) ();
+\<close>
+code_reserved SML bind return
+  
+text\<open>
+  Make sure the code generator does not try to define \<^typ>\<open>'\<alpha> io\<close> by itself, but always uses
+  the one of the target language.
+  For Haskell, this is the fully qualified Prelude.IO.
+  For SML, we wrap it in a nullary function.
+\<close>
+code_printing type_constructor io \<rightharpoonup> (Haskell) "Prelude.IO _"
+                                     and (SML) "unit -> _"
+
+
+text\<open>
+In Isabelle, a \<^typ>\<open>string\<close> is just a type synonym for \<^typ>\<open>char list\<close>.
+When translating a \<^typ>\<open>string\<close> to Haskell, Isabelle does not use Haskell's \<^verbatim>\<open>String\<close> or 
+\<^verbatim>\<open>[Prelude.Char]\<close>. Instead, Isabelle serializes its own
+  \<^verbatim>\<open>data Char = Char Bool Bool Bool Bool Bool Bool Bool Bool\<close>.
+The resulting code will look just ugly.
+
+To use the native strings of Haskell, we use the Isabelle type \<^typ>\<open>String.literal\<close>.
+This gets translated to a Haskell \<^verbatim>\<open>String\<close>.
+
+A string literal in Isabelle is created with \<^term>\<open>STR ''foo'' :: String.literal\<close>.
+\<close>
+
+text\<open>
+  We define IO functions in Isabelle without implementation.
+  For a proof in Isabelle, we will only describe their externally observable properties.
+  For code generation, we map those functions to the corresponding function of the target language.
+
+  Our assumption is that our description in Isabelle corresponds to the real behavior of those
+  functions in the respective target language.
+
+  We use \<^theory_text>\<open>axiomatization\<close> instead of \<^theory_text>\<open>consts\<close> to axiomatically define that those functions exist,
+  but there is no implementation of them. This makes sure that we have to explicitly write down all
+  our assumptions about their behavior. Currently, no assumptions (apart from their type) can be
+  made about those functions.
+\<close>
+axiomatization
+  println :: "String.literal \<Rightarrow> unit io" and
+  getLine :: "String.literal io"
+
+text \<open>A Haskell module named \<^verbatim>\<open>StdIO\<close> which just implements \<^verbatim>\<open>println\<close> and \<^verbatim>\<open>getLine\<close>.\<close>
+code_printing code_module StdIO \<rightharpoonup> (Haskell) \<open>
+module StdIO (println, getLine) where
+import qualified Prelude (putStrLn, getLine)
+println = Prelude.putStrLn
+getLine = Prelude.getLine
+\<close>                              and (SML) \<open>
+(* Newline behavior in SML is odd.*)
+fun println s () = TextIO.print (s ^ "\n");
+fun getLine () = case (TextIO.inputLine TextIO.stdIn) of
+                  SOME s => String.substring (s, 0, String.size s - 1)
+                | NONE => raise Fail "getLine";
+\<close>
+
+code_reserved Haskell StdIO println getLine
+code_reserved SML println print getLine TextIO
+
+text\<open>
+  When the code generator sees the functions \<^const>\<open>println\<close> or \<^const>\<open>getLine\<close>, we tell it to use
+  our language-specific implementation.
+  \<close>
+code_printing constant println \<rightharpoonup> (Haskell) "StdIO.println"
+                              and (SML) "println"
+            | constant getLine \<rightharpoonup> (Haskell) "StdIO.getLine"
+                              and (SML) "getLine"
+
+
+text\<open>Monad syntax and \<^const>\<open>println\<close> examples.\<close>
+lemma "bind (println (STR ''foo''))
+            (\<lambda>_.  println (STR ''bar'')) =
+       println (STR ''foo'') \<bind> (\<lambda>_. println (STR ''bar''))"
+  by simp 
+lemma "do { _ \<leftarrow> println (STR ''foo'');
+            println (STR ''bar'')} =
+      println (STR ''foo'') \<then> (println (STR ''bar''))"
+  by simp
+
+
+
+subsection\<open>Modelling Running an \<^typ>\<open>'\<alpha> io\<close> Function\<close>
+text\<open>
+  Apply some function \<^term>\<open>iofun :: '\<alpha> io\<close> to a specific world and return the new world
+  (discarding the result of \<^term>\<open>iofun\<close>).
+\<close>
+definition exec :: "'\<alpha> io \<Rightarrow> \<^url> \<Rightarrow> \<^url>" where
+  "exec iofun world = snd (Rep_io iofun world)"
+
+text\<open>Similar, but only get the result.\<close>
+definition eval :: "'\<alpha> io \<Rightarrow> \<^url> \<Rightarrow> '\<alpha>" where
+  "eval iofun world = fst (Rep_io iofun world)"
+
+text\<open>
+  Essentially, \<^const>\<open>exec\<close> and \<^const>\<open>eval\<close> extract the payload \<^typ>\<open>'\<alpha>\<close> and \<^typ>\<open>\<^url>\<close>
+  when executing an \<^typ>\<open>'\<alpha> io\<close>.
+\<close>
+lemma "Abs_io (\<lambda>world. (eval iofun world, exec iofun world)) = iofun"
+  by(simp add: exec_def eval_def Rep_io_inverse)
+
+lemma exec_Abs_io: "exec (Abs_io f) world = snd (f world)"
+  by(simp add: exec_def Abs_io_inverse)
+
+
+lemma exec_then:
+    "exec (io\<^sub>1 \<then> io\<^sub>2) world = exec io\<^sub>2 (exec io\<^sub>1 world)"
+  and eval_then:
+    "eval (io\<^sub>1 \<then> io\<^sub>2) world = eval io\<^sub>2 (exec io\<^sub>1 world)"
+  by (simp_all add: exec_def eval_def bind_def Abs_io_inverse split_beta)
+
+lemma exec_bind:
+    "exec (io\<^sub>1 \<bind> io\<^sub>2) world = exec (io\<^sub>2 (eval io\<^sub>1 world)) (exec io\<^sub>1 world)"
+  and eval_bind:
+    "eval (io\<^sub>1 \<bind> io\<^sub>2) world = eval (io\<^sub>2 (eval io\<^sub>1 world)) (exec io\<^sub>1 world)"
+  by(simp_all add: exec_def eval_def bind_def Abs_io_inverse split_beta)
+
+lemma exec_return:
+    "exec (IO.return a) world = world"
+  and
+    "eval (IO.return a) world = a"
+  by (simp_all add: exec_def eval_def Abs_io_inverse return_def)
+
+
+end
\ No newline at end of file
diff --git a/thys/Hello_World/ROOT b/thys/Hello_World/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Hello_World/ROOT
@@ -0,0 +1,12 @@
+session Hello_World = HOL +
+  options [timeout = 600]
+  sessions
+    "HOL-Library"
+  theories
+    IO
+    HelloWorld
+    HelloWorld_Proof
+  theories [document = false]
+    RunningCodeFromIsabelle
+  document_files
+    "root.tex"
diff --git a/thys/Hello_World/RunningCodeFromIsabelle.thy b/thys/Hello_World/RunningCodeFromIsabelle.thy
new file mode 100644
--- /dev/null
+++ b/thys/Hello_World/RunningCodeFromIsabelle.thy
@@ -0,0 +1,81 @@
+theory RunningCodeFromIsabelle
+  imports HelloWorld
+begin
+
+section\<open>Running the Generated Code inside Isabelle\<close>
+
+(*Maintainer note: We invoke the generated code ON PURPOSE from bash to demonstrate how to use
+  the generated code from outside Isabelle and make sure the code runs.*)
+
+
+text\<open>
+  Usually, one would use \<^theory_text>\<open>export_code\<close> to generate code. Here, we want to write the code to
+  a temp directory and execute it right afterwards inside Isablle, so we invoke the code generator
+  directly from Isabelle/ML.
+\<close>
+
+subsection\<open>Haskell\<close>
+
+ML\<open>
+val (files, _) =
+  Code_Target.produce_code @{context} false [@{const_name main}] "Haskell" "Main" NONE []
+
+val target = File.tmp_path (Path.basic ("export" ^ serial_string ()))
+
+val ghc = getenv "ISABELLE_GHC";
+
+val cmd =
+  "cd " ^ Path.implode target ^ " && " ^
+    Bash.string ghc ^ " Main.hs && " ^
+    "(  echo 'Cyber Cat 42' | ./Main )";
+
+Isabelle_System.mkdirs target;
+
+app (fn ([file], content) =>
+   let
+     val path = Path.append target (Path.basic file)
+   in
+     File.write path content
+   end) files;
+
+val exitcode =
+  if ghc <> "" then
+    Isabelle_System.bash cmd
+  else
+    (writeln "not running Haskell, because $ISABELLE_GHC is not set."; 0);
+
+if exitcode <> 0 then
+  raise (Fail ("example Haskell code did not run as expected, " ^
+                 "exit code was " ^ (Int.toString exitcode)))
+else ()
+\<close>
+
+
+subsection\<open>SML\<close>
+
+ML\<open>
+
+val ([(_, content)], _) =
+  Code_Target.produce_code @{context} false [@{const_name main}] "SML" "HelloWorld" NONE []
+
+val target = File.tmp_path (Path.basic ("export" ^ serial_string ()))
+val file = Path.append target (Path.basic "main.ML")
+
+val cmd =
+  "echo 'Super Goat 2000' | " ^
+    "\"${POLYML_EXE?}\" --use " ^ Path.implode file ^
+    " --eval 'HelloWorld.main ()'";
+
+Isabelle_System.mkdirs target;
+File.write file content;
+
+val exitcode = Isabelle_System.bash cmd;
+
+if exitcode <> 0 then
+  raise (Fail ("example SML code did not run as expected, " ^
+                 "exit code was " ^ (Int.toString exitcode)))
+else ()
+\<close>
+
+
+end
\ No newline at end of file
diff --git a/thys/Hello_World/document/root.tex b/thys/Hello_World/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Hello_World/document/root.tex
@@ -0,0 +1,48 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+
+\usepackage{marvosym} % world symbol
+\newcommand{\isactrlurl}[0]{\Mundus}
+
+\usepackage{verbatim}
+
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Hello World}
+\author{Cornelius Diekmann, Lars Hupel}
+\maketitle
+
+\begin{abstract}
+In this article, we present a formalization of the well-known ``Hello, World!'' code, including a formal framework for reasoning about IO.
+Our model is inspired by the handling of IO in Haskell.
+We start by formalizing the \isactrlurl{} and embrace the IO monad afterwards.
+Then we present a sample \verb~main :: IO ()~, followed by its proof of correctness.
+\end{abstract}
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,521 +1,522 @@
 AODV
 Auto2_HOL
 Auto2_Imperative_HOL
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 AutoFocus-Stream
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_Operations
 Bell_Numbers_Spivey
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BNF_CC
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CYK
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Completeness
 Complete_Non_Orders
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Consensus_Refined
 Constructive_Cryptography
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 DFS_Framework
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 Discrete_Summation
 DiscretePricing
 DiskPaxos
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Factored_Transition_System_Bounding
 Farkas
 FFT
 FLP
 FOL-Fitting
 FOL_Harrison
 FOL_Seq_Calc1
 Falling_Factorial_Sum
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite_Automata_HF
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 GPU_Kernel_PL
 Gabow_SCC
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
+Hello_World
 HereditarilyFinite
 Hermite
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interval_Arithmetic_Word32
 Iptables_Semantics
 Irrationality_J_Hancl
 Isabelle_C
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_to_DRA
 LTL_to_GBA
 LTL_Master_Theorem
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Lambda_Free_EPO
 Launchbury
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 MFMC_Countable
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mersenne_Primes
 MFOTL_Monitor
 MiniML
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multirelations
 Multi_Party_Computation
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 Open_Induction
 OpSets
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PCF
 PLM
 Pell
 POPLmark-deBruijn
 PSemigroupsConvolution
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Perfect-Number-Thm
 Perron_Frobenius
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Poincare_Bendixson
 Poincare_Disc
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Projective_Geometry
 Program-Conflict-Analysis
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Randomised_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 Safe_OCL
 SATSolverVerification
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Timed_Automata
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Universal_Turing_Machine
 UPF
 UPF_Firewall
 UpDown_Scheme
 UTP
 Valuation
 VectorSpace
 VeriComp
 Verified-Prover
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 VolpanoSmith
 WHATandWHERE_Security
 WebAssembly
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 Zeta_Function
 Zeta_3_Irrational
 ZFC_in_HOL
 pGCL