Fix bibliography: add missing year

This commit fixes a typo in the type signature of `init` (thanks to
Ramsay Carslaw for spotting it). This commit also structures the last
sentence of Section 2.7 to read slightly better.

Makefile

@@ -3,8 +3,10 @@ CFLAGS=-interaction=nonstopmode -halt-on-error -file-line-error
 BIBC=bibtex
 PAPER=thesis
 BIBLIO=$(PAPER)
+LATEST_COMMIT=$(shell git log --format="%h" -n 1)
 
 all: $(PAPER).pdf
+draft: $(PAPER).pdf-draft
 
 $(PAPER).aux: $(PAPER).tex
 	$(TEXC) $(CFLAGS) $(PAPER)
@@ -16,6 +18,11 @@ $(PAPER).pdf: $(PAPER).aux $(BIBLIO).bbl
 	$(TEXC) $(CFLAGS) $(PAPER)
 	$(TEXC) $(CFLAGS) $(PAPER)
 
+$(PAPER).pdf-draft: CFLAGS:=$(CFLAGS) "\def\DRAFT{$(LATEST_COMMIT)}\input{$(PAPER)}"
+$(PAPER).pdf-draft: all
+	mv $(PAPER).pdf $(PAPER)-draft.pdf
+	tar cf thesis-draft.tar.gz $(PAPER)-draft.pdf
+
 clean:
 	rm -f *.log *.aux *.toc *.out
 	rm -f *.bbl *.blg *.fls *.xml

README.md

@@ -1,6 +1,120 @@
-# PhD dissertation on foundations for programming and implementing effect handlers
+# Foundations for programming and implementing effect handlers
+
+A copy of my dissertation can be [downloaded via my
+website](https://dhil.net/research/papers/thesis.pdf).
+
+----
+
+Submitted on May 30, 2021. Examined on August 13, 2021.
+
+The board of examiners were
+
+* [Andrew Kennedy](https://github.com/andrewjkennedy) (Facebook London)
+* [Edwin Brady](https://www.type-driven.org.uk/edwinb/) (University of St Andrews)
+* [Ohad Kammar](http://denotational.co.uk/) (The University of Edinburgh)
+* [Stephen Gilmore](https://homepages.inf.ed.ac.uk/stg/) (The University of Edinburgh)
+
+## Thesis structure
+
+The dissertation is structured as follows.
+
+### Introduction
+
+ * Chapter 1 puts forth an argument for why effect handlers
+   matter. Following this argument it provides a basic introduction to
+   several different approaches to effectful programming through the
+   lens of the state effect. In addition, it also declares the scope
+   and contributions of the dissertation, and discusses some related
+   work.
+
+### Programming
+
+ * Chapter 2 illustrates effect handler oriented programming by
+   example by implementing a small operating system dubbed Tiny UNIX,
+   which captures some essential traits of Ritchie and Thompson's
+   UNIX. The implementation starts with a basic notion of file i/o,
+   and then, it evolves into a feature-rich operating system with full
+   file i/o, multiple user environments, multi-tasking, and more, by
+   composing ever more effect handlers.
+
+ * Chapter 3 introduces a polymorphic fine-grain call-by-value core
+   calculus, λ<sub>b</sub>, which makes key use of Rémy-style row
+   polymorphism to implement polymorphic variants, structural records,
+   and a structural effect system. The calculus distils the essence of
+   the core of the Links programming language. The chapter also
+   presents three extensions of λ<sub>b</sub>, which are λ<sub>h</sub>
+   that adds deep handlers, λ<sup>†</sup> that adds shallow handlers,
+   and λ<sup>‡</sup> that adds parameterised handlers.
+
+### Implementation
+
+ * Chapter 4 develops a higher-order continuation passing style
+   translation for effect handlers through a series of step-wise
+   refinements of an initial standard continuation passing style
+   translation for λ<sub>b</sub>. Each refinement slightly modifies
+   the notion of continuation employed by the translation. The
+   development ultimately leads to the key invention of generalised
+   continuation, which is used to give a continuation passing style
+   semantics to deep, shallow, and parameterised handlers.
+
+ * Chapter 5 demonstrates an application of generalised continuations
+   to abstract machine as we plug generalised continuations into
+   Felleisen and Friedman's CEK machine to obtain an adequate abstract
+   runtime with simultaneous support for deep, shallow, and
+   parameterised handlers.
+
+### Expressiveness
+
+ * Chapter 6 shows that deep, shallow, and parameterised notions of
+   handlers can simulate one another up to specific notions of
+   administrative reduction.
+
+ * Chapter 7 studies the fundamental efficiency of effect handlers. In
+   this chapter, we show that effect handlers enable an asymptotic
+   improvement in runtime complexity for a certain class of
+   functions. Specifically, we consider the *generic count* problem
+   using a pure PCF-like base language λ<sub>b</sub><sup>→</sup> (a
+   simply typed variation of λ<sub>b</sub>) and its extension with
+   effect handlers λ<sub>h</sub><sup>→</sup>.  We show that
+   λ<sub>h</sub><sup>→</sup> admits an asymptotically more efficient
+   implementation of generic count than any λ<sub>b</sub><sup>→</sup>
+   implementation.
+
+### Conclusions
+  * Chapter 8 concludes and discusses future work.
+
+### Appendices
+
+ * Appendix A contains a literature survey of continuations and
+   first-class control. I classify continuations according to their
+   operational behaviour and provide an overview of the various
+   first-class sequential control operators that appear in the
+   literature. The application spectrum of continuations is discussed
+   as well as implementation strategies for first-class control.
+ * Appendix B contains a proof that shows the `Get-get` equation for
+   state is redundant.
+ * Appendix C contains the proof details and gadgetry for the
+   complexity of the effectful generic count program.
+ * Appendix D provides a sample implementation of the Berger count
+   program and discusses it in more detail.
+
+## Building
 
 To build the dissertation you need the [Informatics thesis LaTeX
-class](https://github.com/dhil/inf-thesis-latex-cls).
+class](https://github.com/dhil/inf-thesis-latex-cls) with the
+University of Edinburgh crests. Invoking `make` on the command line
+ought to produce a PDF copy of the dissertation named `thesis.pdf`,
+e.g.
 
-Don't hold your breath... This thing isn't due for a while...
+```shell
+$ make
+```
+
+## Timeline
+
+I submitted my thesis on May 30, 2021. It was examined on August 13,
+2021, where I received pass with minor corrections. The revised thesis
+was submitted on December 22, 2021. It was approved on March
+14, 2022. The final revision was submitted on March 23, 2022. I
+received my PhD award letter on March 24, 2022. My graduation 
+ceremony took place in McEwan Hall on July 11, 2022.

code/State.hs

@@ -0,0 +1,124 @@
+{- A Haskell version of the companion code for "State of effectful programming".
+   Tested with GHCi 8.6.5. -}
+import Control.Monad.ST (runST)
+import Data.STRef       (newSTRef, readSTRef, writeSTRef)
+-- State monad
+newtype State s a = State { runState :: s -> (a,s) }
+
+-- | State is a functor
+instance Functor (State s) where
+  fmap f m = State (\st -> let (x, st') = runState m st in
+                           (f x, st'))
+
+-- | State is an applicative functor
+instance Applicative (State s) where
+  pure x = State (\st -> (x, st))
+  m1 <*> m2 = State (\st -> let (f, st') = runState m1 st in
+                            runState (fmap f m2) st')
+
+-- | State is a monad
+instance Monad (State s) where
+  return = pure
+  m >>= k = State (\st -> let (x, st') = runState m st in
+                          runState (k x) st')
+
+-- | State operations
+get :: () -> State s s
+get () = State (\st -> (st, st))
+
+put :: s -> State s ()
+put st = State (\st' -> ((), st))
+
+-- Continuation monad
+newtype Cont r a = Cont { runCont :: (a -> r) -> r }
+
+-- | Cont is a functor
+instance Functor (Cont r) where
+  fmap f k = Cont (\g -> runCont k (\x -> g (f x)))
+
+-- | Cont is an applicative functor
+instance Applicative (Cont r) where
+  pure x  = Cont (\k -> k x)
+  k <*> k' = Cont (\r -> runCont k
+                   (\k'' -> runCont k'
+                     (\x -> r (k'' x))))
+
+-- | Cont is a monad
+instance Monad (Cont r) where
+  return  = pure
+  m >>= k = Cont (\k' -> runCont m
+                   (\x -> runCont (k x)
+                     (\y -> k' y)))
+
+-- | State operations
+
+getk :: () -> Cont (State s a) s
+getk () = Cont (\k -> State (\st -> runState (k st) st))
+
+putk :: s -> Cont (State s a) ()
+putk st' = Cont (\k -> State (\st -> runState (k ()) st'))
+
+-- Free monad
+data Free f a = Return a
+              | Op (f (Free f a))
+
+-- | Free is a functor
+instance Functor f => Functor (Free f) where
+  fmap f (Return x) = Return (f x)
+  fmap f (Op y)     = Op (fmap (fmap f) y)
+
+-- | Free is an applicative functor
+instance Functor f => Applicative (Free f) where
+  pure  = Return
+  (Return f) <*> xs = fmap f xs
+  (Op f)     <*> xs = Op (fmap (\g -> g <*> xs) f)
+
+-- | Free is a monad
+instance Functor f => Monad (Free f) where
+  return = Return
+  (Return x) >>= k = k x
+  (Op y)     >>= k = Op (fmap (\m' -> m' >>= k) y)
+
+-- | Auxiliary function for constructing operation nodes
+do' :: Functor f => f a -> Free f a
+do' op = Op (fmap Return op)
+
+-- Instantiate Free with state
+data FreeState s r = Get (s -> r)
+                   | Put s (() -> r)
+
+-- | FreeState is a functor
+instance Functor (FreeState s) where
+  fmap f (Get k) = Get (\st -> f (k st))
+  fmap f (Put st' k) = Put st' (\() -> f (k ()))
+
+-- | State operations
+get' :: () -> Free (FreeState s) s
+get' () = do' (Get (\x -> x))
+
+put' :: s -> Free (FreeState s) ()
+put' st = do' (Put st (\() -> ()))
+
+-- | State handler
+runState' :: s -> Free (FreeState s) a -> (a, s)
+runState' st0 (Op (Get k))    = runState' st0 (k st0)
+runState' st0 (Op (Put st k)) = runState' st (k ())
+runState' st0 (Return x)      = (x, st0)
+
+-- Generic state example
+incrEven :: Monad m => (() -> m Int, Int -> m ()) -> () -> m Bool
+incrEven (get, put) () = get () >>= (\st -> put (1 + st) >>= (\() -> return (even st)))
+
+runExamples :: Int -> [(String, (Bool, Int))]
+runExamples st0 = map (\(s, f) -> (s, f st0)) examples
+  where examples = [ ("builtin state", \st -> runST $ do
+                         st' <- newSTRef st
+                         v   <- readSTRef st'
+                         writeSTRef st' (v + 1)
+                         v'  <- readSTRef st'
+                         return (even v, v'))
+                   , ("pure state passing", \st -> (even st, st + 1))
+                   , ("state monad", \st -> runState (incrEven (get, put) ()) st)
+                   , ("continuation monad", \st -> runState (runCont (incrEven (getk, putk) ())
+                                                              (\x -> State (\st -> (x, st)))) st)
+                   , ("free monad", \st -> runState' st (incrEven (get', put') ())) ]

code/state.ml

@@ -0,0 +1,396 @@
+(* Companion for "State of effectful programming"
+   Tested with OCaml 4.10.0+multicore. *)
+
+(* Generic direct-style incr_even *)
+let even : int -> bool
+  = fun n -> n mod 2 = 0
+
+let incr_even : (unit -> int) * (int -> unit) -> unit -> bool
+  = fun (get, put) () ->
+  let st = get () in
+  put (1 + st);
+  even st
+
+(* Delimited control *)
+module Prompt : sig
+  type 'a t
+  val make : unit -> 'a t
+  val reify : 'a t -> (('b -> 'a) -> 'a) -> 'b
+  val install : 'a t -> (unit -> 'a) -> 'a
+end = struct
+  type 'a t = {
+      install : (unit -> 'a) -> 'a;
+      reify : 'b. (('b -> 'a) -> 'a) -> 'b
+    }
+
+  let make (type a) () =
+    let module M = struct
+        effect Prompt : (('b -> a) -> a) -> 'b
+      end
+    in
+    let reify f = perform (M.Prompt f) in
+    let install f =
+      match f () with
+      | x -> x
+      | effect (M.Prompt f) k -> f (continue k)
+    in
+    { install; reify }
+
+  let install { install; _ } = install
+  let reify { reify; _ } = reify
+  let resume k v = continue k v
+end
+
+module type CTRL = sig
+  type ans
+  val reset : (unit -> ans) -> ans
+  val shift : (('a -> ans) -> ans) -> 'a
+end
+
+module Ctrl(R : sig type ans end) : sig
+  include CTRL with type ans = R.ans
+end = struct
+  type ans = R.ans
+
+  let p : ans Prompt.t = Prompt.make ()
+
+  let reset m =
+    Prompt.install p m
+
+  let shift f =
+    Prompt.reify p
+      (fun k ->
+        Prompt.install p
+          (fun () ->
+            f (fun x ->
+                Prompt.install p
+                  (fun () -> k x))))
+end
+
+module CtrlState
+         (S : sig type s end)
+         (R : sig type ans end): sig
+  type s = S.s
+  type ans = s -> R.ans * s
+
+  val get : unit -> s
+  val put : s -> unit
+
+  val run : (unit -> R.ans) -> ans
+end = struct
+  type s = S.s
+  type ans = s -> R.ans * s
+  module Ctrl = Ctrl(struct type nonrec ans = ans end)
+
+  let get ()  = Ctrl.shift (fun k -> fun st -> k st st)
+  let put st' = Ctrl.shift (fun k -> fun st -> k () st')
+
+  let run m =
+    Ctrl.reset
+      (fun () ->
+        let x = m () in
+        fun st -> (x, st))
+end
+
+module CtrlIntState = CtrlState(struct type s = int end)(struct type ans = bool end)
+
+(* Monadic programming *)
+module type MONAD = sig
+  type 'a t
+  val return : 'a -> 'a t
+  val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
+(** State monad **)
+module type STATE_MONAD = sig
+  type ans
+  type s
+  include MONAD
+
+  val get : unit -> s t
+  val put : s -> unit t
+  val run : (unit -> ans t) -> s -> ans * s
+end
+
+module StateMonad(S : sig type s end)(R : sig type ans end): sig
+  include STATE_MONAD with type s = S.s
+                       and type ans = R.ans
+end = struct
+  type ans = R.ans
+  type s = S.s
+  type 'a t = s -> 'a * s
+
+  let return : 'a -> 'a t
+    = fun x -> fun st -> (x, st)
+
+  let (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+    = fun m k -> fun st ->
+      let (x, st') = m st in
+      k x st'
+
+  let get : unit -> s t
+    = fun () st -> (st, st)
+
+  let put : s -> unit t
+    = fun st st' -> ((), st)
+
+  let run : (unit -> ans t) -> s -> ans * s
+    = fun m st -> m () st
+end
+
+module IntStateMonad = StateMonad(struct type s = int end)(struct type ans = bool end)
+
+(** Continuation monad **)
+module type CONTINUATION_MONAD = sig
+  type r
+  include MONAD with type 'a t = ('a -> r) -> r
+end
+
+module ContinuationMonad(R : sig type ans end): sig
+  include CONTINUATION_MONAD with type r = R.ans
+end = struct
+  type r = R.ans
+  type 'a t = ('a -> r) -> r
+
+  let return : 'a -> 'a t
+    = fun x -> fun k -> k x
+
+  let (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+    = fun m k -> fun c ->
+      m (fun x -> k x c)
+end
+
+module ContinuationStateMonad
+         (S : sig type s end)
+         (R : sig type ans end): sig
+  type s = S.s
+  type ans = R.ans
+  include CONTINUATION_MONAD with type r = s -> ans * s
+
+  val get : unit -> s t
+  val put : s -> unit t
+  val run : (unit -> ans t) -> s -> ans * s
+end = struct
+  type s = S.s
+  type ans = R.ans
+  module ContinuationMonad : CONTINUATION_MONAD with type r = s -> ans * s
+    = ContinuationMonad(struct type nonrec ans = s -> ans * s end)
+  include ContinuationMonad
+
+  let get : unit -> s t
+    = fun () -> fun k -> fun st -> k st st
+
+  let put : s -> unit t
+    = fun st' -> fun k -> fun st -> k () st'
+
+  let run : (unit -> R.ans t) -> s -> R.ans * s =
+    fun m st -> m () (fun x -> fun st -> (x, st)) st
+end
+
+module ContinuationIntStateMonad
+  = ContinuationStateMonad(struct type s = int end)(struct type ans = bool end)
+
+(** Free monad **)
+module type FUNCTOR = sig
+  type 'a t
+  val fmap : ('a -> 'b) -> 'a t -> 'b t
+end
+
+module type FREE_MONAD = sig
+  type 'a op
+  type 'a free = Return of 'a
+               | Op of 'a free op
+
+  include MONAD with type 'a t = 'a free
+
+  val do' : 'a op -> 'a free
+end
+
+module FreeMonad(F : FUNCTOR) : sig
+  include FREE_MONAD with type 'a op = 'a F.t
+end = struct
+  type 'a op = 'a F.t
+  type 'a free = Return of 'a
+               | Op of 'a free F.t
+
+  type 'a t = 'a free
+
+  let return : 'a -> 'a t
+    = fun x -> Return x
+
+  let rec (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+    = fun m k ->
+    match m with
+    | Return x -> k x
+    | Op y -> Op (F.fmap (fun m' -> m' >>= k) y)
+
+  let do' : 'a F.t -> 'a free
+    = fun op -> Op (F.fmap (fun x -> Return x) op)
+end
+
+module type FREE_STATE = sig
+  type s
+  type 'r opsig = Get of (s -> 'r)
+                | Put of s * (unit -> 'r)
+  include FUNCTOR with type 'r t = 'r opsig
+end
+
+module FreeState(S : sig type s end) = struct
+  type s = S.s
+  type 'r opsig = Get of (s -> 'r)
+                | Put of s * (unit -> 'r)
+  type 'r t = 'r opsig
+
+  let fmap : ('a -> 'b) -> 'a t -> 'b t
+    = fun f op ->
+    match op with
+    | Get k -> Get (fun st -> f (k st))
+    | Put (st', k) -> Put (st', fun st -> f (k ()))
+end
+
+module FreeIntStateMonad: sig
+  include STATE_MONAD with type s = int
+                       and type ans = bool
+end = struct
+
+  module rec FreeIntState : FREE_STATE with type s = int
+    = FreeState(struct type s = int end)
+  and FreeIntStateMonad : FREE_MONAD with type 'r op = 'r FreeIntState.opsig
+    = FreeMonad(FreeIntState)
+
+  open FreeIntState
+  include FreeIntStateMonad
+
+  type s = int
+  type ans = bool
+
+  let get : unit -> s t
+    = fun () -> do' (Get (fun st -> st))
+
+  let put : s -> unit t
+    = fun st -> do' (Put (st, fun () -> ()))
+
+  let rec run : (unit -> ans t) -> s -> ans * s
+    = fun m st ->
+    match m () with
+    | Return x          -> (x, st)
+    | Op (Get k)        -> run (fun () -> k st) st
+    | Op (Put (st', k)) -> run k st'
+end
+
+(** Monadic reflection **)
+module Reflect
+         (M : MONAD)
+         (R : sig type ans end): sig
+  type ans = R.ans
+
+  val reify : (unit -> ans) -> ans M.t
+  val reflect : 'a M.t -> 'a
+
+end = struct
+  type ans = R.ans
+  effect Reflect : 'a M.t -> 'a
+
+  let reify : (unit -> ans) -> ans M.t
+    = fun f ->
+    let open M in
+    match f () with
+    | x -> return x
+    | effect (Reflect m) k -> m >>= (continue k)
+
+  let reflect : 'a M.t -> 'a
+    = fun m ->
+    perform (Reflect m)
+end
+
+module ReflectIntStateMonad
+  = Reflect(IntStateMonad)(struct type ans = bool end)
+
+module ReflectIntState = struct
+  open ReflectIntStateMonad
+
+  let get : unit -> int
+    = fun () -> reflect (IntStateMonad.get ())
+
+  let put : int -> unit
+    = fun st -> reflect (IntStateMonad.put st)
+
+  let run : (unit -> bool) -> int -> bool * int
+    = fun m st -> IntStateMonad.run (fun () -> reify m) st
+end
+
+(* Generic monadic incr_even *)
+module MonadExample(T : STATE_MONAD with type s = int) = struct
+  let incr_even : unit -> bool T.t
+    = fun () ->
+    let open T in
+    (get ()) >>= (fun st -> put (1 + st)
+             >>= (fun () -> return (even st)))
+end
+
+(** Effect handlers **)
+module type STATE_HANDLER = sig
+  type s
+
+  val get : unit -> s
+  val put : s -> unit
+  val run : (unit -> 'a) -> s -> 'a * s
+end
+
+module StateHandler(S : sig type s end) : STATE_HANDLER with type s = S.s = struct
+  type s = S.s
+
+  effect Put : s -> unit
+  let put st = perform (Put st)
+
+  effect Get : unit -> s
+  let get () = perform (Get ())
+
+  let run
+    = fun m st ->
+    let f = match m () with
+      | x -> (fun st -> (x, st))
+      | effect (Put st') k -> (fun st -> continue k () st')
+      | effect (Get ()) k -> (fun st -> continue k st st)
+    in f st
+end
+
+module IntStateHandler = StateHandler(struct type s = int end)
+
+let run_examples () =
+  let examples = [
+      "builtin", (fun st ->
+        let st = ref st in let v = !st in st := 1 + v; (even v, !st));
+      "pure state passing", (fun st -> (even st, 1 + st));
+      "shift/reset", (fun st ->
+        CtrlIntState.run (incr_even CtrlIntState.(get, put)) st);
+      "state monad", (fun st ->
+        let module MonadStateExample = MonadExample(IntStateMonad) in
+        IntStateMonad.run MonadStateExample.incr_even st);
+      "continuation monad", (fun st ->
+        let module ContinuationMonadExample = MonadExample(ContinuationIntStateMonad) in
+        ContinuationIntStateMonad.run ContinuationMonadExample.incr_even st);
+      "free monad", (fun st ->
+        let module FreeMonadExample = MonadExample(FreeIntStateMonad) in
+        FreeIntStateMonad.run FreeMonadExample.incr_even st);
+      "monadic reflection", (fun st ->
+        ReflectIntState.run (incr_even ReflectIntState.(get, put)) st);
+      "state handler", (fun st ->
+        IntStateHandler.run (incr_even IntStateHandler.(get, put)) st) ]
+  in
+  List.map (fun (s, f) -> (s, f 4)) examples
+(* module IntStateMRefl : MREFL with type ans := bool and type 'a t = 'a IntState.t
+ *   = MRefl(struct type ans = bool end)(IntState)
+ * 
+ * let get () = IntStateMRefl.reflect (IntState.get ())
+ * let put st = IntStateMRefl.reflect (IntState.put st)
+ * let run m st = IntState.run (IntStateMRefl.reify m) st
+ * 
+ * let even : int -> bool
+ *   = fun n -> n mod 2 = 0
+ * 
+ * let incr_even : unit -> bool
+ *   = fun () ->
+ *   let st = get () in
+ *   put (1 + st);
+ *   even st *)

code/unix-plug2020.links

@@ -0,0 +1,782 @@
+## Prelude
+typename Option(a) = [|None|Some:a|];
+
+sig todo : (String) ~> a
+fun todo(s) { error("TODO: " ^^ s) }
+
+sig fail : () {Fail:Zero |_}-> a
+fun fail() { switch (do Fail) { } }
+
+sig lookup : (a, [(a, b)]) {Fail:Zero |_}~> b
+fun lookup(k, kvs) {
+  switch (kvs) {
+    case [] -> fail()
+    case (k', v) :: kvs' ->
+      if (k == k') v
+      else lookup(k, kvs')
+  }
+}
+
+sig modify : (a, b, [(a, b)]) ~> [(a, b)]
+fun modify(k, v, kvs) {
+  switch (kvs) {
+    case [] -> []
+    case (k', v') :: kvs' ->
+      if (k == k') (k, v) :: kvs'
+      else (k', v') :: modify(k, v, kvs')
+  }
+}
+
+sig remove : (a, [(a, b)]) ~> [(a, b)]
+fun remove(k, kvs) {
+  switch (kvs) {
+    case [] -> []
+    case (k', v') :: kvs' ->
+      if (k == k') kvs'
+      else (k', v') :: remove(k, kvs')
+  }
+}
+
+sig has : (a, [(a, b)]) ~> Bool
+fun has(k, kvs) {
+  switch (kvs) {
+    case [] -> false
+    case (k', _) :: kvs' ->
+      k == k' || has(k, kvs')
+  }
+}
+
+#!
+#
+#        UNIX in 50 lines of code or less
+#               Daniel Hillerström
+#  Laboratory for Foundations of Computer Science
+#          The University of Edinburgh
+#
+#                   PLUG talk
+#             University of Glasgow
+#                December 8, 2020
+#
+#           https://dhil.net/research/
+#
+#?
+
+#!
+#
+# What is an operating system? (very abstractly)
+#
+# An operating system responds to a collection of system calls
+#
+# Example tasks:
+#  - Signalling errors
+#  - Scheduling processes
+#  - Reading/writing I/O
+#?
+
+#!
+#
+# What is an effect handler? (very abstractly)
+#
+# An effect handler responds a collection of abstract operation calls
+#
+# Example tasks:
+#  - Signalling errors
+#  - Scheduling processes
+#  - Reading/writing I/O
+#
+#
+#
+#
+#
+#?
+
+#!
+#
+# What is an effect handler? (very abstractly)
+#
+# An effect handler responds a collection of abstract operation calls
+#
+# Example tasks:
+#  - Signalling errors
+#  - Scheduling processes
+#  - Reading/writing I/O
+#
+# Thus an effect handler is an operating system (credit James McKinna)
+# (Kiselyov and Shan (2007) used delimited continuations to model
+#  operating systems)
+#
+#?
+
+#!
+#
+# Objectives of this talk
+#
+# - Demonstrate the versatility of handlers
+# - Explain operating systems as the combination of
+#   + Exceptions
+#   + Dynamic binding
+#   + Nondeterminism
+#   + State
+#
+#?
+
+#
+#
+# What is UNIX?
+#
+# UNIX is an operating system designed by Ritchie and Thompson (1974)
+#
+# Components
+#  - Commands (system calls)
+#    + I/O interaction, user session management, inter-process
+#      communication, etc
+#  - Kernel   (interpreter)
+#    + Handling of I/O, managing user sessions, scheduling of
+#      processes
+#  - Development environment
+#    + Compiler tool-chains (e.g. `cc`)
+#  - Documentation
+#    + manual pages (e.g. `man`)
+#
+#
+
+#!
+#
+# Key characteristics of UNIX (Ritchie & Thompson, 1974)
+#
+# - Support for multiple user sessions
+# - Time-sharing between processes
+# - "Everything is a file"
+#
+#?
+
+#!
+#
+# Basic I/O: Performing writes
+#
+typename File = String;
+typename FileDescr = Int;
+
+sig stdout : FileDescr
+var stdout = 1;
+
+sig echo : (String) {Write:(FileDescr,String) -> () |%}-> ()
+fun echo(cs) { todo("implement echo") }
+#?
+
+#!
+#
+# Basic I/O: Handling writes
+#
+sig basicIO : ( () {Write:(FileDescr,String) -> () |%}-> a ) { |%}-> (a, File)
+fun basicIO(m) {
+   todo("implement basicIO")
+}
+#?
+
+#!
+#
+# Basic I/O: Example
+#
+sig example0 : () { |%}-> ((), File)
+fun example0() {
+  basicIO(fun() {
+        echo("Hello"); echo("World")
+  })
+}
+#?
+
+#!
+#
+# Dynamic semantics of handlers
+#
+#  (ret) handle(V) { case Return(x) -> N case ... }
+#        ~> N[V/x]
+#
+#  (op)  handle(E[do Op(V)]) { case Op(p,r) -> N case ... }
+#        ~> N[V/p
+#            ,fun(x){ handle(E[x]) { case Op(p,r) -> N case ... }}/r]
+#        (if Op \notin E)
+#
+#?
+
+#!
+#
+# Exceptions: Premature exits
+#
+sig exit : (Int) {Exit:(Int) -> Zero |%}-> a
+fun exit(n) { todo("implement exit") }
+#?
+
+#!
+#
+# Handling exits
+#
+sig status : (() {Exit:(Int) -> Zero |%}-> a) { |%}-> Int
+fun status(m) {
+  todo("implement status")
+}
+#?
+
+#!
+#
+# Handling exits: Example
+#
+sig example1 : () { |%}-> (Int, File)
+fun example1() {
+  basicIO(fun() {
+        status(fun() {
+          echo("dead"); exit(1); echo("code")
+        })
+  })
+}
+#?
+
+#!
+#
+# Dynamic binding: User-specific environments (1)
+#
+typename User = [|Alice|Bob|Root|];
+
+sig whoami : () {Ask:String |%}-> String
+fun whoami() { do Ask }
+#?
+
+#!
+#
+# Dynamic binding: User-specific environments (2)
+#
+sig env : (User, () {Ask:String |%}-> a) { |%}-> a
+fun env(user, m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Ask(resume) ->
+      switch (user) {
+        case Alice -> resume("alice")
+        case Bob   -> resume("bob")
+        case Root  -> resume("root")
+      }
+  }
+}
+
+
+sig example2 : () { |%}-> String
+fun example2() {
+  env(Root, whoami)
+}
+#?
+
+#!
+#
+# Aside: Dynamic binding with delimited continuations
+#
+# The idea of dynamic binding dates back to at least McCarthy (1960)
+#
+# Kiselyov, Shan, and Sabry (2006) demonstrated dynamic binding can be
+# simulated with delimited continuations
+#
+#?
+
+#!
+#
+# User session management
+#
+sig su : (User) {Su:(User) -> () |%}-> ()
+fun su(user) { do Su(user) }
+
+sig sessionmgr : (User, () {Ask:String, Su:(User) -> () |%}-> a) { |%}-> a
+fun sessionmgr(user, m) {
+  env(user, fun() {
+     handle(m()) {
+       case Return(x) -> x
+       case Su(user', resume) ->
+         env(user', fun() { resume(()) })
+     }
+  })
+}
+#?
+
+#!
+#
+# Multiple user sessions example
+#
+sig example3 : () { |%}-> (Int, File)
+fun example3() {
+  basicIO(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            su(Alice); echo(whoami()); echo(" ");
+            su(Bob);   echo(whoami()); echo(" ");
+            su(Root);  echo(whoami())
+          })
+        })
+  })
+}
+#?
+
+#!
+#
+# Nondeterminism: Multi-tasking (1)
+#
+# From the man pages.
+#
+# Description
+#   fork() creates a new process by duplicating the calling process.  The
+#   new process is referred to as the child process.  The calling process
+#   is referred to as the parent process.
+#
+# Return value
+#   On success, the PID of the child process is returned in the parent,
+#   and 0 is returned in the child.
+#
+#?
+
+#!
+#
+# Nondeterminism: Multi-tasking (2)
+#
+sig fork : () {Fork:Bool |_}-> Bool
+fun fork() { do Fork }
+
+sig nondet : (() {Fork:Bool |%}-> a) { |%}-> [a]
+fun nondet(m) {
+  handle(m()) {
+    case Return(ans)  -> todo("implement Return case")
+    case Fork(resume) -> todo("implement Fork case")
+  }
+}
+#?
+
+#!
+#
+# Nondeterminism: Example (1)
+#
+sig ritchie : () {Write:(FileDescr, String) -> () |%}-> ()
+fun ritchie() {
+  echo("UNIX is basically ");
+  echo("a simple operating system, ");
+  echo("but ");
+  echo("you have to be a genius to understand the simplicity.\n")
+}
+
+sig hamlet : () {Write:(FileDescr, String) -> () |%}-> ()
+fun hamlet() {
+  echo("To be, or not to be,\n");
+  echo("that is the question:\n");
+  echo("Whether 'tis nobler in the mind to suffer\n")
+}
+#?
+
+#!
+#
+# Nondeterminism: Example (2)
+#
+sig example4 : () { |%}-> ([Int], File)
+fun example4() {
+  basicIO(fun() {
+    nondet(fun() {
+      sessionmgr(Root, fun() {
+        status(fun() {
+          if (fork()) {
+            su(Alice);
+            ritchie()
+          } else {
+            su(Bob);
+            hamlet()
+          }
+        })
+      })
+    })
+  })
+}
+#?
+
+#
+#
+# Mathematically well-founded nondeterminism
+#
+# The handler `nondet` is _exactly_ the handler Plotkin and Pretnar (2013)
+# give for nondeterminism
+# It satisfies the usual (semi-lattice) equations for nondeterministic choice, i.e.
+#
+#   if (fork()) M else M                        = M
+#   if (fork()) M else N                        = if (fork()) N else M
+#   if (fork()) L else { if (fork()) M else N } = if (fork()) { if (fork()) L else M } else N
+#
+#
+
+#!
+#
+# Interrupting processes
+#
+sig interrupt : () {Interrupt:() |%}-> ()
+fun interrupt() { do Interrupt }
+
+# Process reification
+typename Pstate(a,e::Eff)
+         = forall q::Presence.
+           [|Done:a
+            |Paused:() {Interrupt{q} |e}-> Pstate(a, { |e})|];
+
+
+sig reifyProcess : (() {Interrupt:() |%}-> a) { |%}-> Pstate(a, { |%})
+fun reifyProcess(m) {
+  handle(m()) {
+    case Return(ans) -> Done(ans)
+    case Interrupt(resume) -> Paused(fun() { resume(()) })
+  }
+}
+#?
+
+#!
+#
+# Time-sharing via interrupts
+#
+sig schedule : ([Pstate(a, { Fork:Bool |%})]) { |%}~> [a]
+fun schedule(ps) {
+  fun schedule(ps, done) {
+    switch (ps) {
+      case [] -> done
+      case Done(res) :: ps' ->
+        schedule(ps', res :: done)
+      case Paused(resume) :: ps' ->
+        schedule(ps' ++ nondet(resume), done)
+    }
+  }
+  schedule(ps, [])
+}
+
+sig timeshare : (() {Fork:Bool,Interrupt:() |%}-> a) { |%}-> [a]
+fun timeshare(m) {
+  var p = Paused(fun() { reifyProcess(m) });
+  schedule([p])
+}
+#?
+
+#!
+#
+# Injecting interrupts
+#
+# First idea: external source injects interrupts (Ahman and Pretnar (2021))
+#
+# Second idea: bundle interrupts with other operations
+sig echo' : (FileDescr,String) {Interrupt:(), Write:(FileDescr,String) -> () |%}-> ()
+fun echo'(fd, cs) { interrupt(); do Write(fd, cs) }
+#
+# Third idea: overload interpretations of operations
+sig interruptWrite : (() {Write:(FileDescr,String) -> () |%}-> a)
+                              {Write:(FileDescr,String) -> () |%}-> a
+fun interruptWrite(m) {
+  handle(m()) {
+    case Return(res) -> res
+    case Write(fd, cs, resume) ->
+      interrupt(); resume(do Write(fd, cs))
+  }
+}
+#?
+
+#!
+#
+# Time-sharing example
+#
+sig example5 : () { |%}-> ([Int], File)
+fun example5() {
+  basicIO(fun() {
+    timeshare(fun() {
+      interruptWrite(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            if (fork()) {
+              su(Alice);
+              ritchie()
+            } else {
+              su(Bob);
+              hamlet()
+            }
+          })
+        })
+      })
+    })
+  })
+}
+#?
+
+#!
+#
+# State: File I/O
+#
+# Generic state handling
+sig get : () {Get:s |_}-> s
+fun get() { do Get }
+
+sig put : (s) {Put:(s) -> () |_}-> ()
+fun put(st) { do Put(st) }
+
+sig runState : (s, () {Get:() -> s,Put:(s) -> () |%}-> a) { |%}-> (a, s)
+fun runState(st0, m) {
+  var f = handle(m()) {
+    case Return(x)       -> fun(st) { (x, st) }
+    case Get(resume)     -> fun(st) { resume(st)(st) }
+    case Put(st',resume) -> fun(_)  { resume(())(st') }
+  };
+  f(st0)
+}
+#?
+
+#!
+#
+# State: Example
+#
+sig incr : () {Get:Int,Put:(Int) -> () |%}-> ()
+fun incr() { put(get() + 1) }
+
+sig example6 : () { |%}-> ((), Int)
+fun example6() {
+  runState(41, incr)
+}
+#?
+
+#!
+#
+# Basic Serial File System
+#
+#     Directory              I-List              Data region
+# +----------------+        +-------+     +--------------------------+
+# | "hamlet"       |------> |   2   |---> | "To be, or not to be..." |
+# +----------------+     /  +-------+     +--------------------------+
+# | "richtie.txt"  |------> |   1   |---> | "UNIX is basically..."   |
+# +----------------+    /   +-------+     +--------------------------+
+# | ...            |    |   |  ...  |     | ...                      |
+# +----------------+    |   +-------+     +--------------------------+
+# | "stdout"       |------> |   1   |---> | ""                       |
+# +----------------+    |   +-------+     +--------------------------+
+# | ...            |    /
+# +----------------+   /
+# | "act3"         |---
+# +----------------+
+#
+# Simplifications:
+#   - Operating directly on inode pointers
+#   - Reads and writes will be serial
+#
+#?
+
+#!
+#
+# BSFS structures
+#
+typename INode      = (loc:Int,lno:Int);
+typename IList      = [(Int, INode)];  # INode index -> INode
+typename Directory  = [(String, Int)]; # Filename -> INode index
+typename DataRegion = [(Int, File)];   # Loc -> File
+
+typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
+                                    ,lnext:Int         ,inext:Int    );
+
+sig fsys0 : FileSystem
+var fsys0 = ( dir     = [("stdout", 0)]
+            , inodes  = [(0, (loc=0, lno=1))]
+            , dregion = [(0, "")]
+            , lnext = 1, inext = 1 );
+
+
+# Utility functions
+sig lookup : (a, [(a, b)]) {Fail:Zero |%}-> b
+var lookup = lookup;
+
+sig withDefault : (a, () {Fail:Zero |%}-> a) { |%}-> a
+fun withDefault(x', m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Fail(_)   -> x'
+  }
+}
+#?
+
+sig fwrite : (Int, String, FileSystem) {Fail:Zero |%}-> FileSystem
+fun fwrite(ino, cs, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  var file  = lookup(inode.loc, fsys.dregion);
+  var file' = file ^^ cs;
+  (fsys with dregion = modify(inode.loc, file', fsys.dregion))
+}
+
+sig fread : (Int, FileSystem) {Fail:Zero |%}-> String
+fun fread(ino, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  lookup(inode.loc, fsys.dregion)
+}
+
+#!
+#
+# Handling BSFS operations: file reading and writing
+#
+sig fwrite : (FileDescr, String, FileSystem) {Fail:Zero |%}-> FileSystem
+var fwrite = fwrite;
+sig fread : (FileDescr, FileSystem) {Fail:Zero |%}-> String
+var fread = fread;
+
+sig fileRW : ( () { Read :(FileDescr) -> Option(String)
+                  , Write:(FileDescr, String) -> ()     |%}-> a )
+                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
+fun fileRW(m) {
+  handle(m()) {
+    case Return(ans) -> ans
+    case Read(fd, resume) ->
+      var cs = withDefault(None, fun() {
+                 Some(fread(fd, get()))
+      }); resume(cs)
+    case Write(fd, cs, resume) ->
+      withDefault((), fun() {
+        var fsys = fwrite(fd, cs, get());
+        put(fsys)
+      }); resume(())
+  }
+}
+#?
+
+sig fopen : (String, FileSystem) {Fail:Zero |%}-> FileDescr
+fun fopen(fname, fsys) { lookup(fname, fsys.dir) }
+
+sig fcreate : (String, FileSystem) {Fail:Zero |%}-> (FileDescr, FileSystem)
+fun fcreate(fname, fsys) {
+  if (has(fname, fsys.dir)) {
+    var ino = fopen(fname, fsys);
+    # Truncate file
+    var inode = lookup(ino, fsys.inodes);
+    var dregion = modify(inode.loc, "", fsys.dregion);
+    (ino, (fsys with =dregion))
+  } else {
+    var loc = fsys.lnext;
+    var dregion = (loc, "") :: fsys.dregion;
+
+    var ino   = fsys.inext;
+    var inode = (loc=loc,lno=1);
+    var inodes = (ino, inode) :: fsys.inodes;
+
+    var dir = (fname, ino) :: fsys.dir;
+    (ino, (=dir, =dregion, =inodes, lnext=loc+1, inext=ino+1))
+  }
+}
+
+#!
+#
+# BSFS operation: file opening and creation
+#
+sig fopen : (String, FileSystem) {Fail:Zero |%}-> FileDescr
+var fopen = fopen;
+sig fcreate : (String, FileSystem) {Fail:Zero |%}-> (FileDescr, FileSystem)
+var fcreate = fcreate;
+
+sig fileOC : ( () { Open  :(String) -> Option(FileDescr)
+                  , Create:(String) -> Option(FileDescr) |%}-> a )
+                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
+fun fileOC(m) {
+  handle(m()) {
+    case Return(ans) -> ans
+    case Open(fname, resume) ->
+      var fd = withDefault(None, fun() {
+                 Some(fopen(fname, get()))
+      }); resume(fd)
+    case Create(fname, resume) ->
+      var fd = withDefault(None, fun() {
+                 var (fd, fsys) = fcreate(fname, get());
+                 put(fsys); Some(fd)
+      }); resume(fd)
+  }
+}
+#?
+
+#!
+#
+# BSFS version 0
+#
+sig bsfs0 : ( () {  Open  :(String) -> Option(FileDescr)
+                  , Create:(String) -> Option(FileDescr)
+                  , Read :(FileDescr) -> Option(String)
+                  , Write:(FileDescr, String) -> ()     |%}-> a )
+                          {Get:FileSystem,Put:(FileSystem) -> () |%}-> a
+fun bsfs0(m) {
+  fileOC(fun() {
+    fileRW(m)
+  })
+}
+#?
+
+#!
+#
+# Stream redirection
+#
+sig >- : (() { |%}-> a, String)
+                { Create:(String) -> Option(FileDescr)
+                , Exit  : (Int) -> Zero
+                , Write :(FileDescr,String) -> ()      |%}-> a
+op f >- fname {
+  var fd = switch (do Create(fname)) {
+             case None -> exit(-1)
+             case Some(fd) -> fd
+  }; handle(f()) {
+      case Return(x) -> x
+      case Write(_, cs, resume) ->
+       resume(do Write(fd, cs))
+    }
+}
+#?
+
+#!
+#
+# Crude copy
+#
+sig ccp : (String, String) { Create:(String) -> Option(FileDescr)
+                           , Exit  :(Int) -> Zero
+                           , Read  :(FileDescr) -> Option(String)
+                           , Open  :(String) -> Option(FileDescr)
+                           , Write :(FileDescr,String) -> ()      |%}-> ()
+fun ccp(src, dst) {
+  var srcfd = switch (do Open(src)) {
+    case None -> exit(-1)
+    case Some(fd) -> fd
+  };
+  switch (do Read(srcfd)) {
+    case None -> exit(-1)
+    case Some(cs) -> fun() {echo(cs)} >- dst
+  }
+}
+#?
+
+#!
+#
+# Plugging everything together
+#
+sig example7 : () { |%}-> ([Int], FileSystem)
+fun example7() {
+  runState(fsys0, fun() {
+    bsfs0(fun() {
+      timeshare(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            if (fork()) {
+              su(Alice);
+              ritchie >- "ritchie.txt"
+            } else {
+              su(Bob);
+              hamlet >- "hamlet";
+              ccp("hamlet", "act3")
+            }
+          })
+        })
+      })
+    })
+  })
+}
+#?
+
+#!
+#
+# Conclusion
+#
+# Effect handlers are a versatile programming abstraction
+# Operating systems can be explained in terms of handlers
+# "Every problem can be solved by adding another handler"
+#
+#?

code/unix.links

@@ -45,8 +45,6 @@ module Queue {
   fun singleton(x) { enqueue(x, empty) }
 }
 
-
-
 ##
 ## Environment
 ##
@@ -106,6 +104,27 @@ fun usermgr(user, envs, m) {
 ## Basic IO
 ##
 typename FileDescr = Int;
+typename FileCursor = Int;
+
+module File {
+  typename T = [String];
+
+  sig empty : T
+  var empty = [];
+
+  sig read : (FileCursor, T) ~> Option(String)
+  fun read(start, file) {
+    switch (drop(start, file)) {
+      case []     -> None
+      case x :: _ -> Some(x)
+    }
+  }
+
+  sig write : (String, FileCursor, T) ~> T
+  fun write(contents, fptr, file) {
+    take(fptr, file) ++ [contents] ++ drop(fptr, file)
+  }
+}
 
 sig stdout : FileDescr
 var stdout = 1;
@@ -113,7 +132,7 @@ var stdout = 1;
 sig puts : (FileDescr,String) {Puts:(FileDescr,String) -> () |_}-> ()
 fun puts(fd, s) { do Puts(fd, s) }
 
-sig basicIO : (Comp(a, {Puts:(FileDescr,String) -> () |e})) {Puts{_} |e}~> [String]
+sig basicIO : (Comp(a, {Puts:(FileDescr,String) -> () |e})) {Puts{_} |e}~> File.T
 fun basicIO(m) {
   handle(m()) {
     case Return(_) -> []
@@ -121,8 +140,6 @@ fun basicIO(m) {
   }
 }
 
-# TODO: implement file space.
-
 ##
 ## Generic state handling.
 ##
@@ -153,118 +170,125 @@ var stderr = 2;
 sig eof : String
 var eof = "\x00";
 
-sig gets : (FileDescr) {Gets:(FileDescr) -> String |_}-> String
-fun gets(fd) { do Gets(fd) }
+typename Mode = [|Read|Write|];
 
-typename Mode = [|Create|Append|];
+typename FileDescr = Int;
+typename INode = (loc:Option(Int),refc:Int);
 
-sig fopen : (Mode, String) {Fopen:(Mode, String) -> FileDescr |_}-> FileDescr
-fun fopen(mode, filename) { do Fopen(mode, filename) }
+typename INodeTable = [(INode, File.T)];
+typename FileTable  = [(Mode, INode)];
+typename 
 
-sig fclose : (FileDescr) {Fclose:(FileDescr) -> () |_}-> ()
-fun fclose(fd) { do Fclose(fd) }
+# sig gets : (FileDescr) {Gets:(FileDescr) -> String |_}-> String
+# fun gets(fd) { do Gets(fd) }
 
-typename File = Queue.T(String);
+# sig fopen : (Mode, String) {Fopen:(Mode, String) -> FileDescr |_}-> FileDescr
+# fun fopen(mode, filename) { do Fopen(mode, filename) }
 
-sig emptyFile : File
-var emptyFile = Queue.empty;
+# sig fclose : (FileDescr) {Fclose:(FileDescr) -> () |_}-> ()
+# fun fclose(fd) { do Fclose(fd) }
 
-sig writeFile : (String, File) -> File
-fun writeFile(s, file) { Queue.enqueue(s, file) }
+# typename File = Queue.T(String);
 
-sig readFile : (File) ~> (String, File)
-fun readFile(file) {
-  switch (Queue.dequeue(file)) {
-    case (None, file) -> (eof, file)
-    case (Some(s), file) -> (s, file)
-  }
-}
+# sig emptyFile : File
+# var emptyFile = Queue.empty;
 
-typename FileTable = [(FileDescr, File)];
-typename FileStore = [(String, FileDescr)];
-typename FileSystem = (next:Int,ft:FileTable,fs:FileStore);
+# sig writeFile : (String, File) -> File
+# fun writeFile(s, file) { Queue.enqueue(s, file) }
 
-sig defaultFileSystem : () -> FileSystem
-fun defaultFileSystem() {
-  var defaultTable = [ (stdin , emptyFile)
-                     , (stdout, emptyFile)
-                     , (stderr, emptyFile) ];
+# sig readFile : (File) ~> (String, File)
+# fun readFile(file) {
+#   switch (Queue.dequeue(file)) {
+#     case (None, file) -> (eof, file)
+#     case (Some(s), file) -> (s, file)
+#   }
+# }
 
-  var defaultStore = [ ("stdin" , stdin)
-                     , ("stdout", stdout)
-                     , ("stderr", stderr) ];
+# typename FileTable = [(FileDescr, File)];
+# typename FileStore = [(String, FileDescr)];
+# typename FileSystem = (next:Int,ft:FileTable,fs:FileStore);
 
-  (next=3,ft=defaultTable,fs=defaultStore)
-}
+# sig defaultFileSystem : () -> FileSystem
+# fun defaultFileSystem() {
+#   var defaultTable = [ (stdin , emptyFile)
+#                      , (stdout, emptyFile)
+#                      , (stderr, emptyFile) ];
 
-sig lookupFile : (FileDescr, FileSystem) ~> File
-fun lookupFile(fd, fsys) {
-   switch (lookup(fd, fsys.ft)) {
-     case Nothing -> error("err: No such file(" ^^ intToString(fd) ^^ ")")
-     case Just(file) -> file
-   }
-}
+#   var defaultStore = [ ("stdin" , stdin)
+#                      , ("stdout", stdout)
+#                      , ("stderr", stderr) ];
 
-sig replaceFile : (FileDescr, File, FileSystem) ~> FileSystem
-fun replaceFile(fd, file, fsys) {
-  var ft = modify(fd, file, fsys.ft);
-  (fsys with ft = ft) # TODO handle nonexistent file.
-}
+#   (next=3,ft=defaultTable,fs=defaultStore)
+# }
 
-sig createFile : (String, FileSystem) -> (FileDescr, FileSystem)
-fun createFile(filename, fsys) {
-  var fd = fsys.next;
-  (fd, (next = fd + 1, fs = (filename, fd) :: fsys.fs, ft = (fd, emptyFile) :: fsys.ft))
-}
+# sig lookupFile : (FileDescr, FileSystem) ~> File
+# fun lookupFile(fd, fsys) {
+#    switch (lookup(fd, fsys.ft)) {
+#      case Nothing -> error("err: No such file(" ^^ intToString(fd) ^^ ")")
+#      case Just(file) -> file
+#    }
+# }
 
-sig openFile : (Mode, String, FileSystem) ~> (FileDescr, FileSystem)
-fun openFile(mode, filename, fsys) {
-  var (fd, fsys') = switch (lookup(filename, fsys.fs)) {
-      case Nothing -> createFile(filename, fsys)
-      case Just(fd) -> (fd, fsys)
-  };
-  switch (mode) {
-    case Create -> error("erase")
-    case Append -> (fd, fsys')
-  }
-}
+# sig replaceFile : (FileDescr, File, FileSystem) ~> FileSystem
+# fun replaceFile(fd, file, fsys) {
+#   var ft = modify(fd, file, fsys.ft);
+#   (fsys with ft = ft) # TODO handle nonexistent file.
+# }
 
-sig closeFile : (File) ~> File
-fun closeFile((=front,=rear)) {
-  (front=front ++ reverse(rear), rear=[])
-}
+# sig createFile : (String, FileSystem) -> (FileDescr, FileSystem)
+# fun createFile(filename, fsys) {
+#   var fd = fsys.next;
+#   (fd, (next = fd + 1, fs = (filename, fd) :: fsys.fs, ft = (fd, emptyFile) :: fsys.ft))
+# }
 
-sig allowState : (() {Get-,Put- |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
-fun allowState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() {Get-,Put- |e}~> a)) }
+# sig openFile : (Mode, String, FileSystem) ~> (FileDescr, FileSystem)
+# fun openFile(mode, filename, fsys) {
+#   var (fd, fsys') = switch (lookup(filename, fsys.fs)) {
+#       case Nothing -> createFile(filename, fsys)
+#       case Just(fd) -> (fd, fsys)
+#   };
+#   switch (mode) {
+#     case Create -> error("erase")
+#     case Append -> (fd, fsys')
+#   }
+# }
 
-sig fileIO : (Comp(a, {Get-,Put-,Gets:(FileDescr) -> String,Puts:(FileDescr,String) -> (),Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr |e})) {Get:() {}-> FileSystem,Put:(FileSystem) -> (),Gets{_},Puts{_},Fclose{_},Fopen{_} |e}~> a
-fun fileIO(m) {
-  handle(allowState(m)()) {
-    case Gets(fd, resume) ->
-      var fsys = get();
-      var (ch, file) = readFile(lookupFile(fd, fsys));
-      put(replaceFile(fd, file, fsys)); resume(ch)
-    case Puts(fd, ch, resume) ->
-      var fsys = get();
-      var fsys' = replaceFile(fd, writeFile(ch, lookupFile(fd, fsys)), fsys);
-      put(fsys'); resume(())
-    case Fopen(mode, filename, resume) ->
-      var fsys = get();
-      var (fd, fsys') = openFile(mode, filename, fsys);
-      put(fsys'); resume(fd)
-    case Fclose(fd, resume) ->
-      var fsys = get();
-      var fsys' = replaceFile(fd, closeFile(lookupFile(fd, fsys)), fsys);
-      put(fsys'); resume(())
-  }
-}
+# sig closeFile : (File) ~> File
+# fun closeFile((=front,=rear)) {
+#   (front=front ++ reverse(rear), rear=[])
+# }
 
-sig redirect : (Comp(a, {Puts:(FileDescr,String) -> () |e}), FileDescr) {Puts:(FileDescr,String) -> () |e}~> a
-fun redirect(m, fd) {
-  handle(m()) {
-    case Puts(_,s,resume) -> resume(puts(fd, s))
-  }
-}
+# sig allowState : (() {Get-,Put- |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
+# fun allowState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() {Get-,Put- |e}~> a)) }
+
+# sig fileIO : (Comp(a, {Get-,Put-,Gets:(FileDescr) -> String,Puts:(FileDescr,String) -> (),Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr |e})) {Get:() {}-> FileSystem,Put:(FileSystem) -> (),Gets{_},Puts{_},Fclose{_},Fopen{_} |e}~> a
+# fun fileIO(m) {
+#   handle(allowState(m)()) {
+#     case Gets(fd, resume) ->
+#       var fsys = get();
+#       var (ch, file) = readFile(lookupFile(fd, fsys));
+#       put(replaceFile(fd, file, fsys)); resume(ch)
+#     case Puts(fd, ch, resume) ->
+#       var fsys = get();
+#       var fsys' = replaceFile(fd, writeFile(ch, lookupFile(fd, fsys)), fsys);
+#       put(fsys'); resume(())
+#     case Fopen(mode, filename, resume) ->
+#       var fsys = get();
+#       var (fd, fsys') = openFile(mode, filename, fsys);
+#       put(fsys'); resume(fd)
+#     case Fclose(fd, resume) ->
+#       var fsys = get();
+#       var fsys' = replaceFile(fd, closeFile(lookupFile(fd, fsys)), fsys);
+#       put(fsys'); resume(())
+#   }
+# }
+
+# sig redirect : (Comp(a, {Puts:(FileDescr,String) -> () |e}), FileDescr) {Puts:(FileDescr,String) -> () |e}~> a
+# fun redirect(m, fd) {
+#   handle(m()) {
+#     case Puts(_,s,resume) -> resume(puts(fd, s))
+#   }
+# }
 
 ##
 ## Processes
@@ -331,70 +355,70 @@ fun whoami() { getenv("USER") }
 ##
 
 # Tags puts with the name of the current user.
-sig provenance : (Comp(a, {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e})) {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e}~> a
-fun provenance(m) {
-  handle(m()) {
-    case Puts(fd, s, resume) ->
-      var user = whoami();
-      resume(do Puts(fd, user ^^ "> " ^^ s))
-  }
-}
+# sig provenance : (Comp(a, {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e})) {Getenv:(String) -> String,Puts:(FileDescr,String) -> () |e}~> a
+# fun provenance(m) {
+#   handle(m()) {
+#     case Puts(fd, s, resume) ->
+#       var user = whoami();
+#       resume(do Puts(fd, user ^^ "> " ^^ s))
+#   }
+# }
 
-# An example of everything plugged together: a time-shared 'Hello World'.
-sig example : () {Fork:Bool,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
-fun example() {
-  var pid = fork();
-  var () = {
-    if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
-    else if (fork()) su(Alice)
-    else su(Bob)
-  };
-  var user = whoami();
-  puts(stdout, "Hello World!");
-  var uid = getenv("UID");
-  echo("My UID is " ^^ uid);
-  (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
-  echo("My home dir is /home/" ^^ user)
-}
+# # An example of everything plugged together: a time-shared 'Hello World'.
+# sig example : () {Fork:Bool,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
+# fun example() {
+#   var pid = fork();
+#   var () = {
+#     if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
+#     else if (fork()) su(Alice)
+#     else su(Bob)
+#   };
+#   var user = whoami();
+#   puts(stdout, "Hello World!");
+#   var uid = getenv("UID");
+#   echo("My UID is " ^^ uid);
+#   (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
+#   echo("My home dir is /home/" ^^ user)
+# }
 
-# Wiring of handlers.
-sig init : () {Fork{_},Getenv{_},Su{_},Puts{_},Yield{_} |_}~> [String]
-fun init() {
-  basicIO(fun() {
-    schedule(fun() {
-      usermgr(Root, envs, fun() {
-        provenance(example)
-      })
-    })
-  })
-}
+# # Wiring of handlers.
+# sig init : () {Fork{_},Getenv{_},Su{_},Puts{_},Yield{_} |_}~> [String]
+# fun init() {
+#   basicIO(fun() {
+#     schedule(fun() {
+#       usermgr(Root, envs, fun() {
+#         provenance(example)
+#       })
+#     })
+#   })
+# }
 
-sig example' : () {Fork:Bool,Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
-fun example'() {
-  var pid = fork();
-  var () = {
-    if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
-    else if (fork()) su(Alice)
-    else su(Bob)
-  };
-  var user = whoami();
-  var fd = fopen(Append, user ^^ ".txt");
-  puts(fd, "Hello World!");
-  var uid = getenv("UID");
-  echo("My UID is " ^^ uid);
-  (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
-  echo("My home dir is /home/" ^^ user);
-  fclose(fd)
-}
+# sig example' : () {Fork:Bool,Fclose:(FileDescr) -> (),Fopen:(Mode,String) -> FileDescr,Getenv:(String) -> String,Su:(User) -> (),Puts:(FileDescr,String) -> (),Yield:() |_}~> ()
+# fun example'() {
+#   var pid = fork();
+#   var () = {
+#     if (pid) redirect(fun(){puts(stdout, "dummy")}, stderr)
+#     else if (fork()) su(Alice)
+#     else su(Bob)
+#   };
+#   var user = whoami();
+#   var fd = fopen(Append, user ^^ ".txt");
+#   puts(fd, "Hello World!");
+#   var uid = getenv("UID");
+#   echo("My UID is " ^^ uid);
+#   (if (amiroot()) { yield(); echo(user ^^ " is running as root.") } else ());
+#   echo("My home dir is /home/" ^^ user);
+#   fclose(fd)
+# }
 
 
-sig init' : (FileSystem) {Fclose{_},Fopen{_},Fork{_},Get{_},Getenv{_},Gets{_},Put{_},Puts{_},Su{_},Yield{_}|_}~> ((), FileSystem)
-fun init'(fsys) {
-  runState(fsys, fun() {
-    fileIO(fun() {
-      schedule(fun() {
-        usermgr(Root, envs, example')
-      })
-    })
-  })
-}
+# sig init' : (FileSystem) {Fclose{_},Fopen{_},Fork{_},Get{_},Getenv{_},Gets{_},Put{_},Puts{_},Su{_},Yield{_}|_}~> ((), FileSystem)
+# fun init'(fsys) {
+#   runState(fsys, fun() {
+#     fileIO(fun() {
+#       schedule(fun() {
+#         usermgr(Root, envs, example')
+#       })
+#     })
+#   })
+# }

code/unix2.links

@@ -0,0 +1,697 @@
+# Tiny UNIX revision 2.
+
+typename Option(a) = [|None|Some:a|];
+
+sig fail : () {Fail:Zero |_}-> a
+fun fail() { switch (do Fail) {} }
+
+sig optionalise : (Comp(a, {Fail:Zero |e})) {Fail{_} |e}~> Option(a)
+fun optionalise(m) {
+  handle(m()) {
+    case Return(x) -> Some(x)
+    case Fail(_)   -> None
+  }
+}
+
+sig withDefault : (a, Comp(a, {Fail:Zero |e})) {Fail{_} |e}~> a
+fun withDefault(x', m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Fail(_)   -> x'
+  }
+}
+
+sig lookup : (a, [(a, b)]) {Fail:Zero |_}~> b
+fun lookup(k, kvs) {
+  switch (kvs) {
+    case [] -> fail()
+    case (k', v) :: kvs' ->
+      if (k == k') v
+      else lookup(k, kvs')
+  }
+}
+
+sig modify : (a, b, [(a, b)]) ~> [(a, b)]
+fun modify(k, v, kvs) {
+  switch (kvs) {
+    case [] -> []
+    case (k', v') :: kvs' ->
+      if (k == k') (k, v) :: kvs'
+      else (k', v') :: modify(k, v, kvs')
+  }
+}
+
+sig remove : (a, [(a, b)]) ~> [(a, b)]
+fun remove(k, kvs) {
+  switch (kvs) {
+    case [] -> []
+    case (k', v') :: kvs' ->
+      if (k == k') kvs'
+      else (k', v') :: remove(k, kvs')
+  }
+}
+
+sig has : (a, [(a, b)]) ~> Bool
+fun has(k, kvs) {
+  switch (kvs) {
+    case [] -> false
+    case (k', _) :: kvs' ->
+      k == k' || has(k, kvs')
+  }
+}
+
+##
+## Basic i/o
+##
+typename File = String;
+typename FileDescr = Int;
+
+sig stdout : FileDescr
+var stdout = 1;
+
+sig basicIO : (Comp(a, {Write:(FileDescr,String) -> () |e})) {Write{_} |e}~> (a, File)
+fun basicIO(m) {
+  handle(m()) {
+    case Return(res) -> (res, "")
+    case Write(_, s, resume) ->
+      var (res, file) = resume(());
+      (res, s ^^ file)
+  }
+}
+
+sig echo : (String) {Write:(FileDescr,String) -> () |_}~> ()
+fun echo(cs) { do Write(stdout,cs) }
+
+fun example0() {
+  basicIO(fun() {
+        echo("Hello"); echo("World")
+  })
+}
+
+##
+## Exceptions: non-local exits
+##
+sig exit : (Int) {Exit:(Int) -> Zero |_}-> a
+fun exit(n) { switch(do Exit(n)) {} }
+
+sig status : (Comp(a, {Exit:(Int) -> Zero |e})) {Exit{_} |e}~> Int
+fun status(m) {
+  handle(m()) {
+    case Return(_) -> 0
+    case Exit(n, _) -> n
+  }
+}
+
+fun example1() {
+  basicIO(fun() {
+        status(fun() {
+          echo("dead"); exit(1); echo("code")
+        })
+  })
+}
+
+##
+## Dynamic binding: user-specific environments.
+##
+typename User = [|Alice|Bob|Root|];
+
+sig whoami : () {Ask:String |_}-> String
+fun whoami() { do Ask }
+
+sig env : (User, Comp(a, {Ask:String |e})) {Ask{_} |e}~> a
+fun env(user, m) {
+  handle(m()) {
+    case Return(x) -> x
+    case Ask(resume) ->
+      switch (user) {
+        case Alice -> resume("alice")
+        case Bob   -> resume("bob")
+        case Root  -> resume("root")
+      }
+  }
+}
+
+fun example2() {
+  env(Root, whoami)
+}
+
+###
+### Session management.
+###
+sig su : (User) {Su:(User) -> () |_}-> ()
+fun su(user) { do Su(user) }
+
+sig sessionmgr : (User, Comp(a, {Ask:String,Su:(User) -> () |e})) {Ask{_},Su{_} |e}~> a
+fun sessionmgr(user, m) {
+  env(user, fun() {
+     handle(m()) {
+       case Return(x) -> x
+       case Su(user', resume) ->
+         env(user', fun() { resume(()) })
+     }
+  })
+}
+
+fun example3() {
+  basicIO(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            su(Alice); echo(whoami()); echo(" ");
+            su(Bob);   echo(whoami()); echo(" ");
+            su(Root);  echo(whoami())
+          })
+        })
+  })
+}
+
+##
+## Nondeterminism: time sharing.
+##
+sig fork : () {Fork:Bool |_}-> Bool
+fun fork() { do Fork }
+
+sig nondet : (Comp(a, {Fork:Bool |e})) {Fork{_} |e}~> [a]
+fun nondet(m) {
+  handle(m()) {
+    case Return(res) -> [res]
+    case Fork(resume) -> resume(true) ++ resume(false)
+  }
+}
+
+sig interrupt : () {Interrupt:() |_}-> ()
+fun interrupt() { do Interrupt }
+
+typename Pstate(a,e::Eff) = forall q::Presence.
+                            [|Done:a
+                             |Paused:() {Interrupt{q} |e}~> Pstate(a, { |e})|];
+
+sig slice : (Comp(a, {Interrupt:() |e})) {Interrupt{_} |e}~> Pstate(a, { |e})
+fun slice(m) {
+  handle(m()) {
+    case Return(res) -> Done(res)
+    case Interrupt(resume) -> Paused(fun() { resume(()) })
+  }
+}
+
+sig schedule : ([Pstate(a, { Fork:Bool |e})]) {Fork{_},Interrupt{_} |e}~> [a]
+fun schedule(ps) {
+  # sig run : (Pstate (a, { Fork:() {}-> Bool|e })) {Fork{_},Interrupt{_} |e}~> [a]
+  # fun run(p) {
+  #   switch(p) {
+  #     case Done(res) -> [res]
+  #     case Paused(resume) -> runNext(nondet(resume))
+  #   }
+  # }
+  # concatMap(run, ps)
+  fun schedule(ps, done) {
+    switch (ps) {
+      case [] -> done
+      case Done(res) :: ps' ->
+        schedule(ps', res :: done)
+      case Paused(resume) :: ps' ->
+        schedule(ps' ++ nondet(resume), done)
+    }
+  }
+  schedule(ps, [])
+}
+
+sig timeshare : (Comp(a, {Fork:Bool,Interrupt:() |e})) {Fork{_},Interrupt{_} |e}~> [a]
+fun timeshare(m) {
+  var p = Paused(fun() { slice(m) });
+  schedule([p])
+}
+
+fun example4() {
+  basicIO(fun() {
+     timeshare(fun() {
+        sessionmgr(Root, fun() {
+           status(fun() {
+             var parent = fork();
+             (if (parent) su(Alice) else su(Bob));
+             echo(whoami() ^^ "> Hello ");
+             interrupt();
+             echo(whoami() ^^ "> Bye ");
+             interrupt();
+             if (parent) exit(0)
+             else {
+               var parent = fork();
+               interrupt();
+               (if (parent) su(Root)
+                else {
+                 echo(whoami() ^^ "> oops ");
+                 exit(1)
+               });
+               echo(whoami() ^^ "> !! ")
+             }
+           })
+        })
+     })
+  })
+}
+
+fun forktest(n) {
+  fun loop(i, n) {
+    if (i >= n) (-1)
+    else {
+      var x = fork();
+      println("< x = " ^^ (if (x) "true" else "false") ^^ ", i = " ^^ intToString(i));
+      ignore(loop(i+1,n));
+      println("> x = " ^^ (if (x) "true" else "false") ^^ ", i = " ^^ intToString(i));
+      exit(i)
+    }
+  }
+  loop(0, n)
+}
+
+fun test(i) {
+  if (i == 2) ()
+  else {
+    println("< i = " ^^ intToString(i));
+    var x = fork();
+    test(i+1);
+    println("> i = " ^^ intToString(i))
+  }
+}
+
+fun ritchie() {
+  echo("UNIX is basically ");
+  echo("a simple operating system, ");
+  echo("but ");
+  echo("you have to be a genius to understand the simplicity.\n")
+}
+
+fun hamlet() {
+  echo("To be, or not to be,\n");
+  echo("that is the question:\n");
+  echo("Whether 'tis nobler in the mind to suffer\n")
+}
+
+fun example5() {
+  basicIO(fun() {
+    nondet(fun() {
+      sessionmgr(Root, fun() {
+        status(fun() {
+          if (fork()) {
+            su(Alice);
+            ritchie()
+          } else {
+            su(Bob);
+            hamlet()
+          }
+        })
+      })
+    })
+  })
+}
+
+fun interruptWrite(m) {
+  handle(m()) {
+    case Return(res) -> res
+    case Write(fd, cs, resume) ->
+      interrupt(); resume(do Write(fd, cs))
+  }
+}
+
+fun example5'() {
+  basicIO(fun() {
+    timeshare(fun() {
+      interruptWrite(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            if (fork()) {
+              su(Alice);
+              ritchie()
+            } else {
+              su(Bob);
+              hamlet()
+            }
+          })
+        })
+      })
+    })
+  })
+}
+
+##
+## Generic state handling
+##
+sig get : () {Get:s |_}-> s
+fun get() { do Get }
+
+sig put : (s) {Put:(s) -> () |_}-> ()
+fun put(st) { do Put(st) }
+
+sig runState : (s, Comp(a, {Get:() -> s,Put:(s) -> () |e})) {Get{_},Put{_} |e}~> (a, s)
+fun runState(st0, m) {
+  var f = handle(m()) {
+    case Return(x) -> fun(st) { (x, st) }
+    case Get(resume) -> fun(st) { resume(st)(st) }
+    case Put(st,resume) -> fun(_) { resume(())(st) }
+  };
+  f(st0)
+}
+
+fun example6() {
+  runState(0, fun() {
+    var x = 3;
+    put(x);
+    assert(x == get(), "Put;Get");
+    var y = get();
+    var z = get();
+    assert(y == z, "Get;Get");
+    put(x+1);
+    put(x+2);
+    assert(get() == x + 2, "Put;Put")
+  })
+}
+
+##
+## State: file i/o
+##
+typename FilePtr    = Option(FileDescr);
+
+typename INode      = (loc:Int,lno:Int);
+typename IList      = [(Int, INode)];  # INode index -> INode
+typename Directory  = [(String, Int)]; # Filename -> INode index
+typename DataRegion = [(Int, File)];   # Loc -> File
+
+typename FileSystem = (dir:Directory,dregion:DataRegion,inodes:IList
+                                    ,lnext:Int         ,inext:Int    );
+
+sig fsys0 : FileSystem
+var fsys0 = (dir = [("stdout", 0)], inodes = [(0, (loc=0, lno=1))], dregion = [(0, "")], lnext = 1, inext = 1);
+
+sig fopen : (String, FileSystem) {Fail:Zero |_}~> (Int, FileSystem)
+fun fopen(fname, fsys) { (lookup(fname, fsys.dir), fsys) }
+
+sig ftruncate : (Int, FileSystem) {Fail:Zero |_}~> FileSystem
+fun ftruncate(ino, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  var dregion = modify(inode.loc, "", fsys.dregion);
+  (fsys with =dregion)
+}
+
+sig fcreate : (String, FileSystem) {Fail:Zero |_}~> (Int, FileSystem)
+fun fcreate(fname, fsys) {
+  if (has(fname, fsys.dir)) {
+    var (ino, fsys) = fopen(fname, fsys);
+    (ino, ftruncate(ino, fsys))
+  } else {
+    var loc = fsys.lnext;
+    var dregion = (loc, "") :: fsys.dregion;
+
+    var ino   = fsys.inext;
+    var inode = (loc=loc,lno=1);
+    var inodes = (ino, inode) :: fsys.inodes;
+
+    var dir = (fname, ino) :: fsys.dir;
+    (ino, (=dir, =dregion, =inodes, lnext=loc+1, inext=ino+1))
+  }
+}
+
+sig ftruncate : (Int, FileSystem) {Fail:Zero |_}~> FileSystem
+fun ftruncate(ino, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  var dregion = modify(inode.loc, "", fsys.dregion);
+  (fsys with =dregion)
+}
+
+sig fopen : (String, FileSystem) {Fail:Zero |_}~> Int
+fun fopen(fname, fsys) { lookup(fname, fsys.dir) }
+
+sig fclose : (Int, FileSystem) ~> FileSystem
+fun fclose(_, fsys) { fsys }
+
+sig fwrite : (Int, String, FileSystem) {Fail:Zero |_}~> FileSystem
+fun fwrite(ino, cs, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  var file = lookup(inode.loc, fsys.dregion);
+  var file' = file ^^ cs;
+  (fsys with dregion = modify(inode.loc, file', fsys.dregion))
+}
+
+sig fread : (Int, FileSystem) {Fail:Zero |_}~> String
+fun fread(ino, fsys) {
+  var inode = lookup(ino, fsys.inodes);
+  lookup(inode.loc, fsys.dregion)
+}
+
+sig flink : (String, String, FileSystem) {Fail:Zero |_}~> FileSystem
+fun flink(src, dest, fsys) {
+  var ino    = lookup(dest, fsys.dir);
+  var inode  = lookup(ino, fsys.inodes);
+  var inode'  = (inode with lno = inode.lno + 1);
+  var inodes = modify(ino, inode', fsys.inodes);
+
+  var dir    = (src, ino) :: fsys.dir;
+  (fsys with inodes = inodes, dir = dir)
+}
+
+sig funlink : (String, FileSystem) {Fail:Zero |_}~> FileSystem
+fun funlink(fname, fsys) {
+  var i = lookup(fname, fsys.dir);
+  var dir = remove(fname, fsys.dir);
+
+  var inode  = lookup(i, fsys.inodes);
+  var inode'  = (inode with lno = inode.lno - 1);
+
+  if (inode'.lno > 0) {
+    var inodes = modify(i, inode', fsys.inodes);
+    (fsys with inodes = inodes, dir = dir)
+  } else {
+    var dregion = remove(inode'.loc, fsys.dregion);
+    var inodes = remove(i, fsys.inodes);
+    (fsys with inodes = inodes, dir = dir, dregion = dregion)
+  }
+}
+
+sig create : (String) {Create:(String) -> FileDescr |_}-> FileDescr
+fun create(fname) { do Create(fname) }
+
+sig truncate : (FileDescr) {Truncate:(FileDescr) -> () |_}-> ()
+fun truncate(fd) { do Truncate(fd) }
+
+sig open' : (String) {Open:(String) -> Option(FileDescr) |_}-> Option(FileDescr)
+fun open'(fname) { do Open(fname) }
+
+sig close : (FileDescr) {Close:(FileDescr) -> () |_}-> ()
+fun close(fd) { do Close(fd) }
+
+sig write : (FileDescr, String) {Write:(FileDescr, String) -> () |_}-> ()
+fun write(fd, cs) { do Write(fd, cs) }
+
+sig read : (FileDescr) {Read:(FileDescr) -> Option(String) |_}-> Option(String)
+fun read(fd) { do Read(fd) }
+
+sig link : (String, String) {Link:(String, String) -> () |_}-> ()
+fun link(src, dest) { do Link(src, dest) }
+
+sig unlink : (String) {Unlink:(String) -> () |_}-> ()
+fun unlink(fname) { do Unlink(fname) }
+
+sig injectState : (() { |e}~> a) -> () {Get:s,Put:(s) -> () |e}~> a
+fun injectState(f) { (f : (() {Get:s,Put:(s) -> () |e}~> a) <- (() { |e}~> a)) }
+
+sig fileIO : (Comp(a, { #Close:(FileDescr) -> ()
+                        Create:(String) -> FileDescr
+                      , Read:(FileDescr) -> Option(String)
+                      , Open:(String) -> Option(FileDescr)
+                      , Truncate:(FileDescr) -> ()
+                      , Write:(FileDescr, String) -> ()
+                      , Fail{p}|e}))
+              {Create{_},Read{_},Open{_},Truncate{_},Write{_},Get:FileSystem,Put:(FileSystem) -> (),Fail{p} |e}~> a
+fun fileIO(m) {
+  handle(injectState(m)()) {
+    case Return(x) -> x
+    case Create(fname, resume) ->
+      var ino = withDefault(-1, fun() {
+        var (ino, fsys) = fcreate(fname, get());
+        put(fsys); ino
+      }); resume(ino)
+    case Read(ino, resume) ->
+      var contents = optionalise(fun() { fread(ino, get()) });
+      resume(contents)
+    case Open(fname, resume) ->
+      var ino = optionalise(fun() { fopen(fname, get()) });
+      resume(ino)
+    case Truncate(ino, resume) ->
+      withDefault((), fun() {
+        var fsys = ftruncate(ino, get());
+        put(fsys)
+      }); resume(())
+    case Write(ino, cs, resume) ->
+      withDefault((), fun() {
+        var fsys = fwrite(ino, cs, get());
+        put(fsys)
+      }); resume(())
+  }
+}
+
+fun init(fsys, main) {
+  runState(fsys, fun() {
+    fileIO(fun() {
+      timeshare(fun() {
+        sessionmgr(Root, fun() {
+          status(fun() {
+            if(fork()) exit(0) else main()
+          })
+        })
+      })
+    })
+  })
+}
+
+###
+### Stream redirection
+###
+sig >> : (Comp(a, { Create: (String) -> FileDescr
+                  , Write:(FileDescr, String) -> () |e}), String)
+             { Create:(String) -> FileDescr
+             , Write:(FileDescr, String) -> ()      |e}~> a
+op f >> fname {
+  var fd = create(fname);
+  handle(f()) {
+    case Return(x) -> x
+    case Write(_, cs, resume) ->
+      resume(write(fd, cs))
+  }
+}
+
+sig >>> : (Comp(a, { Create: (String) -> FileDescr
+                   , Open: (String)   -> Option (FileDescr)
+                   , Write:(FileDescr, String) -> () |e}), String)
+             { Create:(String) -> FileDescr
+             , Open:(String) -> Option (FileDescr)
+             , Write:(FileDescr, String) -> ()      |e}~> ()
+op f >>> fname {
+  var fd = switch (open'(fname)) {
+      case None -> create(fname)
+      case Some(fd) -> fd
+  };
+  handle(f()) {
+    case Return(_) -> ()
+    case Write(_, cs, resume) ->
+      resume(write(fd, cs))
+  }
+}
+
+fun example7() {
+  if (fork()) {
+    su(Alice);
+    ritchie >> "ritchie.txt"
+  } else {
+    su(Bob);
+    hamlet >> "hamlet"
+  }
+}
+
+###
+### TCP threeway handshake
+###
+
+sig strsplit : (Char, String) ~> [String]
+fun strsplit(c, str) {
+  fun loop(c, str, i, j) {
+    if (i >= strlen(str)) [strsub(str, j, i - j)]
+    else if (charAt(str, i) == c)
+      strsub(str, j, i - j) :: loop(c, str, i+1, i+1)
+    else
+      loop(c,str, i+1, j)
+  }
+  loop(c, str, 0, 0)
+}
+
+sig read1 : (FileDescr) {Read:(FileDescr) -> Option(String) |e}-> Option(String)
+fun read1(fd) {
+  switch (read(fd)) {
+    case Some("") -> None
+    case x    -> x
+  }
+}
+
+sig truncread : (FileDescr) {Read:(FileDescr) -> Option(String),Truncate:(FileDescr) -> () |_}-> Option(String)
+fun truncread(fd) {
+  var cs = read1(fd);
+  truncate(fd); cs
+}
+
+sig synced : (Comp(Option(a), {Interrupt:() |e})) {Interrupt:() |e}~> a
+fun synced(f) {
+  switch (f()) {
+    case None -> interrupt(); synced(f)
+    case Some(x)  -> x
+  }
+}
+
+sig fail : () {Fail:Zero |_}-> a
+fun fail() { switch(do Fail) {} }
+
+fun tcpclient(seq, inp, out) {
+  write(out, "SYN " ^^ intToString(seq));
+  var resp = synced(fun() { truncread(inp) });
+  var [syn, ack] = strsplit(';', resp);
+  var seqn = stringToInt(strsub(syn, 4, strlen(syn) - 4));
+  var ackn = stringToInt(strsub(ack, 4, strlen(ack) - 4));
+  if (ackn <> seq + 1) fail()
+  else write(out, "ACK " ^^ intToString(seqn + 1))
+}
+
+fun tcpserver(seq, inp, out) {
+  var req = synced(fun() { truncread(inp) });
+  var reqn = stringToInt(strsub(req, 4, strlen(req) - 4));
+  var resp = "SYN " ^^ intToString(seq) ^^ ";ACK " ^^ intToString(reqn + 1);
+  write(out, resp);
+  var resp' = synced(fun() { truncread(inp) });
+  var ackn = stringToInt(strsub(resp', 4, strlen(resp') - 4));
+  if (ackn <> seq + 1) fail()
+  else ()
+}
+
+fun performTCP(tcpf, seq, inp, out) {
+  var fd = create(whoami() ^^ ".log");
+  handle(tcpf(seq, inp, out)) {
+    case Return(_) -> write(fd, "Handshake completed.")
+    case Fail(_) -> write(fd, "Handshake failed.")
+   }
+}
+
+fun tcphandshake() {
+  var (cfd, sfd) = (create("client.sock"), create("server.sock"));
+  if (fork()) {
+    su(Alice);
+    performTCP(tcpclient, 42, cfd, sfd)
+  } else {
+    su(Bob);
+    performTCP(tcpserver, 84, sfd, cfd)
+  }
+}
+
+fun tcphandshakeFail() {
+  var (cfd, sfd) = (create("client.sock"), create("server.sock"));
+  if (fork()) {
+    su(Alice);
+    handle(performTCP(tcpclient, 42, cfd, sfd)) {
+      case Write(fd, cs, resume) ->
+        resume(if (strsub(cs, 0, 3) == "ACK") write(fd, "ACK 0")
+               else write(fd, cs))
+    }
+  } else {
+    su(Bob);
+    performTCP(tcpserver, 84, sfd, cfd)
+  }
+}
+
+#
+# Grep
+#
+#sig grep : (String) {Await:Char,Yield:(Char) -> () |_}~> ()
+fun grep(str) {
+  var cs = explode(str);
+  fun match(c,cs) {
+    switch (cs) {
+      case c' :: cs' ->
+        if (c == '\n') fail()
+        if (c == c') 
+    }
+  }
+}

macros.tex

@@ -1,3 +1,41 @@
+%%
+%% Defined-as equality
+%%
+\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
+\newcommand{\defnas}[0]{\mathrel{:=}}
+\newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
+\newcommand{\adef}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny{\text{$\alpha$-def}}}}}{\simeq}}}
+
+%%
+%% Some useful maths abbreviations
+%%
+\newcommand{\C}{\ensuremath{\mathbb{C}}}
+\newcommand{\N}{\ensuremath{\mathbb{N}}}
+\newcommand{\R}{\ensuremath{\mathbb{R}}}
+\newcommand{\Z}{\ensuremath{\mathbb{Z}}}
+\newcommand{\B}{\ensuremath{\mathbb{B}}}
+\newcommand{\BB}[1]{\ensuremath{\mathbf{#1}}}
+\newcommand{\CC}{\keyw{ctrl}}
+% \newcommand{\Delim}[1]{\ensuremath{\langle\!\!\mkern-1.5mu\langle#1\rangle\!\!\mkern-1.5mu\rangle}}
+\newcommand{\Delim}[1]{\ensuremath{\keyw{del}.#1}}
+\newcommand{\sembr}[1]{\ensuremath{\llbracket #1 \rrbracket}}
+\newcommand{\BigO}{\ensuremath{\mathcal{O}}}
+\newcommand{\SC}{\ensuremath{\mathsf{S}}}
+\newcommand{\ST}{\ensuremath{\mathsf{T}}}
+\newcommand{\ar}{\ensuremath{\mathsf{ar}}}
+\newcommand{\Tm}{\ensuremath{\mathsf{Tm}}}
+\newcommand{\Ty}{\ensuremath{\mathsf{Ty}}}
+
+%%
+%% Partiality
+%%
+\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}
+
+%%
+%% Operation arrows
+%%
+\newcommand{\opto}[0]{\ensuremath{\twoheadrightarrow}}
+
 %%
 %% Calculi names.
 %%
@@ -10,6 +48,10 @@
 \newcommand{\HSCalc}{\ensuremath{\lambda_{\mathsf{h^\delta}}}\xspace}
 \newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace}
 \newcommand{\UCalc}{\ensuremath{\lambda_{\mathsf{u}}}\xspace}
+\newcommand{\param}{\ensuremath{\ddagger}}
+\newcommand{\HPCalc}{\ensuremath{\lambda_{\mathsf{h^\param}}}\xspace}
+\newcommand{\HPCF}{\ensuremath{\lambda^\rightarrow_{\mathsf{h}}}\xspace}
+\newcommand{\BPCF}{\ensuremath{\lambda^\rightarrow_{\mathsf{b}}}\xspace}
 
 %%
 %% Calculi terms and types type-setting.
@@ -19,6 +61,7 @@
 \newcommand{\dec}[1]{\mathsf{#1}}
 \newcommand{\keyw}[1]{\mathbf{#1}}
 \newcommand{\Handle}{\keyw{handle}}
+\newcommand{\ParamHandle}{\Handle^\param}
 \newcommand{\ShallowHandle}{\ensuremath{\keyw{handle}^\dagger}}
 \newcommand{\With}{\keyw{with}}
 \newcommand{\Let}{\keyw{let}}
@@ -33,10 +76,16 @@
 \newcommand{\Else}{\keyw{else}}
 \newcommand{\Absurd}{\keyw{absurd}}
 \newcommand{\Record}[1]{\ensuremath{\langle #1 \rangle}}
+\newcommand{\Op}[1]{\ensuremath{\langle\!\!\langle #1 \rangle\!\!\rangle}}
+%\newcommand{\Op}[1]{\ensuremath{\{#1\}}}
+\newcommand{\OpCase}[3]{\Op{#1~#2 \opto #3}}
+\newcommand{\ExnCase}[2]{\Op{#1~#2}}
 \newcommand{\Unit}{\Record{}}
 \newcommand{\Inl}{\keyw{inl}}
 \newcommand{\Inr}{\keyw{inr}}
 \newcommand{\Thunk}{\lambda \Unit.}
+\newcommand{\PCFRef}{\dec{Ref}}
+\newcommand{\refv}{\keyw{ref}}
 
 \newcommand{\Pre}[1]{\mathsf{Pre}(#1)}
 \newcommand{\Abs}{\mathsf{Abs}}
@@ -69,6 +118,8 @@
 \newcommand{\Fail}{\dec{Fail}}
 \newcommand{\Read}{\dec{Read}}
 \newcommand{\Write}{\dec{Write}}
+\newcommand{\Char}{\dec{Char}}
+\newcommand{\String}{\dec{String}}
 
 \newcommand{\True}{\mathsf{true}}
 \newcommand{\False}{\mathsf{false}}
@@ -94,6 +145,10 @@
 
 \newcommand{\Res}{\keyw{res}}
 
+\newcommand{\Cong}{\mathrm{cong}}
+
+\newcommand{\AlgTheory}{\ensuremath{\mathcal{T}}}
+
 %% Handler projections.
 \newcommand{\mret}{\mathrm{ret}}
 \newcommand{\mops}{\mathrm{ops}}
@@ -102,6 +157,7 @@
 \newcommand{\hops}{H^{\mops}}
 %\newcommand{\hex}{H^{\mathrm{ex}}}
 \newcommand{\hell}{H^{\ell}}
+\newcommand{\gell}{\theta^{\ell}}
 
 \newcommand{\depth}{\delta}
 
@@ -112,7 +168,7 @@
 %%
 %% Labels
 %%
-\newcommand{\slab}[1]{\textrm{#1}}
+\newcommand{\slab}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}}
 \newcommand{\klab}[1]{\rulelabel{K}{#1}}
 \newcommand{\semlab}[1]{\rulelabel{S}{#1}}
@@ -150,6 +206,14 @@
 \newcommand{\EvalCat}{\CatName{Cont}}
 \newcommand{\UEvalCat}{\CatName{UCont}}
 \newcommand{\HandlerCat}{\CatName{HDef}}
+\newcommand{\MConfCat}{\CatName{Conf}}
+\newcommand{\MEnvCat}{\CatName{Env}}
+\newcommand{\MValCat}{\CatName{Mval}}
+\newcommand{\MGContCat}{\CatName{GenCont}}
+\newcommand{\MGFrameCat}{\CatName{GenFrame}}
+\newcommand{\MPContCat}{\CatName{PureCont}}
+\newcommand{\MPFrameCat}{\CatName{PureFrame}}
+\newcommand{\MHCloCat}{\CatName{HClo}}
 
 %%
 %% Lindley's array stuff.
@@ -176,23 +240,6 @@
 
 \newenvironment{smathpar}{\vspace{-3ex}\small\begin{mathpar}}{\end{mathpar}\normalsize\ignorespacesafterend}
 
-%%
-%% Defined-as equality
-%%
-\newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
-\newcommand{\defnas}[0]{\mathrel{:=}}
-\newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
-
-%%
-%% Partiality
-%%
-\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}
-
-%%
-%% Operation arrows
-%%
-\newcommand{\opto}[0]{\ensuremath{\twoheadrightarrow}}
-
 %%
 %% Lists
 %%
@@ -201,6 +248,7 @@
 
 \newcommand{\concat}{\mathbin{+\!\!+}}
 \newcommand{\revconcat}{\mathbin{\widehat{\concat}}}
+\newcommand{\snoc}[2]{\ensuremath{#1 \concat [#2]}}
 
 %%
 %% CPS notation
@@ -284,8 +332,9 @@
 % Canonical variables for handler components
 \newcommand{\vhret}{h^{\mret}}
 \newcommand{\vhops}{h^{\mops}}
-\newcommand{\svhret}{\chi^{\mret}}
-\newcommand{\svhops}{\chi^{\mops}}
+\newcommand{\sv}{\chi}
+\newcommand{\svhret}{\sv^{\mret}}
+\newcommand{\svhops}{\sv^{\mops}}
 
 % \newcommand{\dk}{\dRecord{fs,\dRecord{\vhret,\vhops}}}
 \newcommand{\dk}{k}
@@ -305,12 +354,26 @@
 \newcommand{\Option}{\dec{Option}}
 \newcommand{\Some}{\dec{Some}}
 \newcommand{\None}{\dec{None}}
+\newcommand{\Toss}{\dec{Toss}}
+\newcommand{\toss}{\dec{toss}}
+\newcommand{\Heads}{\dec{Heads}}
+\newcommand{\Tails}{\dec{Tails}}
 \newcommand{\Exn}{\dec{Exn}}
 \newcommand{\fail}{\dec{fail}}
 \newcommand{\optionalise}{\dec{optionalise}}
 \newcommand{\bind}{\ensuremath{\gg\!=}}
-\newcommand{\return}{\dec{return}}
+\newcommand{\return}{\dec{Return}}
 \newcommand{\faild}{\dec{withDefault}}
+\newcommand{\Free}{\dec{Free}}
+\newcommand{\FreeState}{\dec{FreeState}}
+\newcommand{\OpF}{\dec{Op}}
+\newcommand{\DoF}{\dec{do}}
+\newcommand{\getF}{\dec{get}}
+\newcommand{\putF}{\dec{put}}
+\newcommand{\fmap}{\dec{fmap}}
+\newcommand{\toggle}{\dec{toggle}}
+\newcommand{\incrEven}{\dec{incrEven}}
+\newcommand{\even}{\dec{even}}
 
 % Abstract machine
 \newcommand{\cek}[1]{\ensuremath{\langle #1 \rangle}}
@@ -325,3 +388,464 @@
 
 % configurations
 \newcommand{\conf}{\mathcal{C}}
+
+% effect sugar
+\newcommand{\inward}[1]{\mathcal{I}\sembr{#1}}
+\newcommand{\outward}[1]{\mathcal{O}\sembr{#1}}
+\newcommand{\xcomp}[1]{\outward{#1}}
+\newcommand{\xval}[1]{\outward{#1}}
+\newcommand{\xpre}[1]{\outward{#1}}
+\newcommand{\xrow}[1]{\outward{#1}}
+\newcommand{\xeff}[1]{\outward{#1}}
+\newcommand{\pcomp}[1]{\inward{#1}}
+\newcommand{\pval}[1]{\inward{#1}}
+\newcommand{\ppre}[1]{\inward{#1}}
+\newcommand{\prow}[1]{\inward{#1}}
+\newcommand{\peff}[1]{\inward{#1}}
+\newcommand{\eamb}{\ensuremath{E_{\mathsf{amb}}}}
+\newcommand{\trval}[1]{\mathcal{T}\sembr{#1}}
+
+% UNIX example
+\newcommand{\UNIX}{UNIX}
+\newcommand{\OSname}[0]{Tiny UNIX}
+\newcommand{\exit}{\dec{exit}}
+\newcommand{\Exit}{\dec{Exit}}
+\newcommand{\Status}{\dec{Status}}
+\newcommand{\status}{\dec{status}}
+\newcommand{\basicIO}{\dec{basicIO}}
+\newcommand{\Putc}{\dec{Putc}}
+\newcommand{\putc}{\dec{putc}}
+\newcommand{\UFile}{\dec{File}}
+\newcommand{\UFD}{\dec{FileDescr}}
+\newcommand{\fwrite}{\dec{fwrite}}
+\newcommand{\iter}{\dec{iter}}
+\newcommand{\map}{\dec{map}}
+\newcommand{\stdout}{\dec{stdout}}
+\newcommand{\IO}{\dec{IO}}
+\newcommand{\BIO}{\dec{BIO}}
+\newcommand{\Alice}{\dec{Alice}}
+\newcommand{\Bob}{\dec{Bob}}
+\newcommand{\Root}{\dec{Root}}
+\newcommand{\User}{\dec{User}}
+\newcommand{\environment}{\dec{env}}
+\newcommand{\EnvE}{\dec{Session}}
+\newcommand{\Ask}{\dec{Ask}}
+\newcommand{\whoami}{\dec{whoami}}
+\newcommand{\Su}{\dec{Su}}
+\newcommand{\su}{\dec{su}}
+\newcommand{\sessionmgr}{\dec{sessionmgr}}
+\newcommand{\echo}{\dec{echo}}
+\newcommand{\strlit}[1]{\texttt{"#1"}}
+\newcommand{\nondet}{\dec{nondet}}
+\newcommand{\Fork}{\dec{Fork}}
+\newcommand{\fork}{\dec{fork}}
+\newcommand{\Interrupt}{\dec{Interrupt}}
+\newcommand{\interrupt}{\dec{interrupt}}
+\newcommand{\Pstate}{\dec{Pstate}}
+\newcommand{\Done}{\dec{Done}}
+\newcommand{\Suspended}{\dec{Paused}}
+\newcommand{\slice}{\dec{slice}}
+\newcommand{\reifyP}{\dec{reifyProcess}}
+\newcommand{\timeshare}{\dec{timeshare}}
+\newcommand{\runNext}{\dec{runNext}}
+\newcommand{\concatMap}{\dec{concatMap}}
+\newcommand{\State}{\dec{State}}
+\newcommand{\runState}{\dec{runState}}
+\newcommand{\Uget}{\dec{get}}
+\newcommand{\Uput}{\dec{put}}
+\newcommand{\nl}{\textbackslash{}n}
+\newcommand{\quoteRitchie}{\dec{ritchie}}
+\newcommand{\quoteHamlet}{\dec{hamlet}}
+\newcommand{\Proc}{\dec{Proc}}
+\newcommand{\schedule}{\dec{schedule}}
+\newcommand{\fsname}{BSFS}
+\newcommand{\FileSystem}{\dec{FileSystem}}
+\newcommand{\Directory}{\dec{Directory}}
+\newcommand{\DataRegion}{\dec{DataRegion}}
+\newcommand{\INode}{\dec{INode}}
+\newcommand{\IList}{\dec{IList}}
+\newcommand{\fileRW}{\dec{fileRW}}
+\newcommand{\fileAlloc}{\dec{fileCO}}
+\newcommand{\URead}{\dec{Read}}
+\newcommand{\UWrite}{\dec{Write}}
+\newcommand{\UCreate}{\dec{Create}}
+\newcommand{\UOpen}{\dec{Open}}
+\newcommand{\fread}{\dec{fread}}
+\newcommand{\fcreate}{\dec{fcreate}}
+\newcommand{\Ucreate}{\dec{create}}
+\newcommand{\redirect}{\texttt{>}}
+\newcommand{\fopen}{\dec{fopen}}
+\newcommand{\lookup}{\dec{lookup}}
+\newcommand{\modify}{\dec{modify}}
+\newcommand{\fileIO}{\dec{fileIO}}
+\newcommand{\ULink}{\dec{Link}}
+\newcommand{\UUnlink}{\dec{Unlink}}
+\newcommand{\flink}{\dec{flink}}
+\newcommand{\funlink}{\dec{funlink}}
+\newcommand{\remove}{\dec{remove}}
+\newcommand{\FileLU}{\dec{FileLU}}
+\newcommand{\fileLU}{\dec{fileLU}}
+\newcommand{\FileIO}{\dec{FileIO}}
+\newcommand{\FileRW}{\dec{FileRW}}
+\newcommand{\FileCO}{\dec{FileCO}}
+\newcommand{\cat}{\dec{cat}}
+\newcommand{\head}{\dec{head}}
+\newcommand{\grep}{\dec{grep}}
+\newcommand{\match}{\dec{match}}
+\newcommand{\wc}{\dec{wc}}
+\newcommand{\forever}{\dec{forever}}
+\newcommand{\textnil}{\textbackslash{}0}
+\newcommand{\charlit}[1]{\texttt{'#1'}}
+\newcommand{\where}{\keyw{where}}
+\newcommand{\intToString}{\dec{intToString}}
+\newcommand{\freq}{\dec{freq}}
+\newcommand{\paste}{\dec{paste}}
+\newcommand{\sed}{\dec{sed}}
+\newcommand{\printTable}{\dec{renderTable}}
+\newcommand{\timesharee}{\dec{timeshare2}}
+\newcommand{\Co}{\dec{Co}}
+\newcommand{\UFork}{\dec{UFork}}
+\newcommand{\ufork}{\dec{ufork}}
+\newcommand{\Wait}{\dec{Wait}}
+\newcommand{\scheduler}{\dec{scheduler}}
+\newcommand{\Sstate}{\dec{Sstate}}
+\newcommand{\Ready}{\dec{Ready}}
+\newcommand{\Blocked}{\dec{Blocked}}
+\newcommand{\init}{\dec{init}}
+\newcommand{\Reader}{\dec{Reader}}
+\newcommand{\Other}{\dec{Other}}
+
+%%
+%% Some control operators
+%%
+\newcommand{\Cupto}{\keyw{cupto}}
+\newcommand{\Set}{\keyw{set}}
+\newcommand{\newPrompt}{\keyw{newPrompt}}
+\newcommand{\Callcc}{\keyw{callcc}}
+\newcommand{\Callcomc}{\ensuremath{\keyw{callcomp}}}
+\newcommand{\textCallcomc}{callcomp}
+\newcommand{\Throw}{\keyw{throw}}
+\newcommand{\Continue}{\keyw{resume}}
+\newcommand{\Catch}{\keyw{catch}}
+\newcommand{\Catchcont}{\keyw{catchcont}}
+\newcommand{\Control}{\keyw{control}}
+\newcommand{\Prompt}{\#}
+\newcommand{\Controlz}{\ensuremath{\keyw{control_0}}}
+\newcommand{\Spawn}{\keyw{spawn}}
+\newcommand{\Promptz}{\ensuremath{\#_0}}
+\newcommand{\Escape}{\keyw{escape}}
+\newcommand{\shift}{\keyw{shift}}
+\newcommand{\shiftz}{\ensuremath{\keyw{shift_0}}}
+\newcommand{\CCpp}{\ensuremath{+\CC+}}
+\newcommand{\CCpm}{\ensuremath{+\CC-}}
+\newcommand{\CCmp}{\ensuremath{-\CC+}}
+\newcommand{\CCmm}{\ensuremath{-\CC-}}
+\def\sigh#1{%
+\pmb{\left\langle\vphantom{#1}\right.}%
+#1%
+\pmb{\left.\vphantom{#1}\right\rangle}}
+\newcommand{\llambda}{\ensuremath{\pmb{\lambda}}}
+\newcommand{\reset}[1]{\pmb{\langle} #1 \pmb{\rangle}}
+\newcommand{\resetz}[1]{\pmb{\langle} #1 \pmb{\rangle}_0}
+\newcommand{\dollarz}[2]{\ensuremath{\reset{#2 \mid #1}}}
+\newcommand{\dollarzh}[2]{\ensuremath{#1\,\$_0#2}}
+\newcommand{\fcontrol}{\keyw{fcontrol}}
+\newcommand{\fprompt}{\%}
+\newcommand{\splitter}{\keyw{splitter}}
+\newcommand{\abort}{\keyw{abort}}
+\newcommand{\calldc}{\keyw{calldc}}
+\newcommand{\J}{\keyw{J}}
+\newcommand{\JI}{\keyw{J}\,\keyw{I}}
+\newcommand{\FelleisenC}{\ensuremath{\keyw{C}}}
+\newcommand{\FelleisenF}{\ensuremath{\keyw{F}}}
+\newcommand{\cont}{\keyw{cont}}
+\newcommand{\Cont}{\dec{Cont}}
+\newcommand{\Algol}{Algol~60}
+\newcommand{\qq}[1]{\ensuremath{\ulcorner #1 \urcorner}}
+\newcommand{\prompttype}{\dec{Prompt}}
+\newcommand{\async}{\keyw{async}}
+\newcommand{\await}{\keyw{await}}
+
+% Language macros
+\newcommand{\Frank}{Frank}
+\newcommand{\SML}{SML}
+\newcommand{\SMLNJ}{\SML{}/NJ}
+\newcommand{\OCaml}{OCaml}
+
+
+%%
+%% Asymptotic improvement macros
+%%
+\newcommand{\LLL}{\ensuremath{\mathcal L}}
+\newcommand{\naive}{naïve\xspace}
+\newcommand{\naively}{naïvely\xspace}
+\newcommand{\Naive}{Naïve\xspace}
+\newcommand{\sem}[1]{\ensuremath{\pi_{#1}}}
+\newcommand{\Iff}{\Leftrightarrow}
+\newcommand{\Implies}{\Rightarrow}
+\newcommand{\BCalcS}{\ensuremath{\lambda_{\textrm{\normalfont s}}\xspace}}
+\newcommand{\BCalcE}{\ensuremath{\lambda_{\textrm{\normalfont e}}\xspace}}
+\newcommand{\BCalcSE}{\ensuremath{\lambda_{\textrm{\normalfont se}}\xspace}}
+\newcommand{\BSPCF}{\ensuremath{\lambda^\rightarrow_{\textrm{\normalfont s}}\xspace}}
+\newcommand{\BEPCF}{\ensuremath{\lambda^\rightarrow_{\textrm{\normalfont e}}\xspace}}
+\newcommand{\BSEPCF}{\ensuremath{\lambda^\rightarrow_{\textrm{\normalfont se}}\xspace}}
+\newcommand{\IfZero}{\keyw{ifzero}}
+\newcommand{\Superpoint}{\lambda\_.\Do\;\Branch~\Unit}
+\newcommand{\ECount}{\dec{effcount}}
+\newcommand{\Countprog}{K}
+\newcommand{\Plus}{\mathsf{Plus}}
+\newcommand{\Minus}{\mathsf{Minus}}
+\newcommand{\Eq}{\mathsf{Eq}}
+\newcommand{\BList}{\mathbb{B}^\ast}
+
+\newcommand{\CtxCat}{\CatName{Ctx}}
+\newcommand{\PureCont}{\mathsf{PureCont}}
+
+\newcommand{\Addr}{\mathsf{Addr}}
+\newcommand{\Lab}{\mathsf{Lab}}
+\newcommand{\Env}{\mathsf{Env}}
+
+\newcommand{\Time}{\dec{DTIME}}
+\newcommand{\query}{\mathord{?}}
+\newcommand{\ans}{\mathord{!}}
+\newcommand{\labs}{\mathsf{labs}}
+\newcommand{\steps}{\mathsf{steps}}
+
+\newcommand{\tree}{\tau}
+\newcommand{\tl}{\labs(\tree)}
+\newcommand{\ts}{\steps(\tree)}
+\newcommand{\T}[1]{\ensuremath{\mathcal{T}_{#1}}}
+\newcommand{\Config}{\dec{Config}}
+\newcommand{\cekl}{\langle}
+\newcommand{\cekr}{\rangle}
+
+\newcommand{\const}[1]{\ulcorner #1 \urcorner}
+\newcommand{\HC}{\ensuremath{\mathcal{H}}}
+
+\newcommand{\tr}{\mathcal{T}}
+\newcommand{\tru}{\mathcal{U}}
+\newcommand{\Tree}{\dec{Tree}}
+\newcommand{\TimedTree}{\dec{TimedTree}}
+\newcommand{\denotep}[1]{\ensuremath{\mathbb{P}\llbracket #1 \rrbracket}}
+
+\newcommand\ttTwoTree{
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 4cm/##1,
+  level distance = 2.0cm}]
+\node (root) [opnode] {Branch}
+  child { node [opnode] {Branch}
+    child { node [leaf] {$\True$}
+      edge from parent node[above left] {$\True$}
+    }
+    child { node [leaf] {$\True$}
+      edge from parent node[above right] {$\False$}
+    }
+    edge from parent node[above left] {$\True$}
+  }
+  child { node [opnode] {Branch}
+    child { node [leaf] {$\True$}
+      edge from parent node[above left] {$\True$}
+    }
+    child { node [leaf] {$\True$}
+      edge from parent node[above right] {$\False$}
+    }
+    edge from parent node[above right] {$\False$}
+  }
+;
+\end{tikzpicture}}
+
+
+\newcommand{\tossTree}{
+  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1,
+      level distance = 1.0cm}]
+\node (root) [opnode] {$\dec{Branch}$}
+  child { node [leaf] {$\dec{Heads}$}
+    edge from parent node[above left] {$\True$}
+  }
+  child { node [leaf] {$\dec{Tails}$}
+    edge from parent node[above right] {$\False$}
+  }
+;
+\end{tikzpicture}}
+
+\newenvironment{twoeqs}{\ba[t]{@{}r@{~}c@{~}l@{~}c@{~}r@{~}c@{~}l@{}}}{\ea}
+
+\newcommand{\compTreeEx}{
+  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.0cm/##1,
+      level distance = 2.0cm}]
+\node (root) [opnode] {$\getF$}
+    child { node [yshift=15] {$\dots$}
+    edge from parent {}
+    }
+    child { node [opnode] {$\putF$}
+      child { node {$\True$}
+         edge from parent node[left] {$\Unit$}
+      }
+    edge from parent node[yshift=5,left] {$-2$}
+    }
+    child { node [opnode] {$\putF$}
+      child { node {$\False$}
+         edge from parent node[left] {$\Unit$}
+      }
+    edge from parent node[yshift=2,left] {$-1$}
+    }
+    child { node [opnode] {$\putF$}
+      child { node {$\True$}
+         edge from parent node[left] {$\Unit$}
+      }
+    edge from parent node[left] {$0$}
+    }
+    child { node [opnode] {$\putF$}
+      child { node {$\False$}
+         edge from parent node[right] {$\Unit$}
+      }
+    edge from parent node[yshift=2,right] {$1$}
+    }
+    child { node [opnode] {$\putF$}
+      child { node {$\True$}
+         edge from parent node[right] {$\Unit$}
+      }
+    edge from parent node[yshift=5,right] {$2$}
+    }
+    child { node [yshift=15] {$\dots$}
+    edge from parent {}
+    }
+;
+\end{tikzpicture}}
+
+\newcommand{\smath}[1]{\ensuremath{{\scriptstyle #1}}}
+
+\newcommand{\InfiniteModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.0cm/##1,
+    level distance = 1.0cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 0}$}
+      child { node [draw=none,rotate=165] {$\vdots$}
+        edge from parent node { }
+      }
+      child { node[leaf] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [leaf] {$\smath{\ans\False}$}
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+\newcommand{\ShortConjModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.5cm/##1,
+    level distance = 1.0cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 0}$}
+      child { node [treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [treenode] {$\smath{\ans\False}$}
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+
+\newcommand{\TTTwoModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 8cm/##1,
+    level distance = 1.5cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+\newcommand{\XORTwoModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 5.5cm/##1,
+    level distance = 1cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+\newcommand{\SXORTwoModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1,
+    level distance = 1cm}]
+\node (root) [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+;
+\end{tikzpicture}}
+%
+\newcommand{\TTZeroModel}{%
+  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 1cm/##1,
+    level distance = 1cm}]
+  \node (root) [draw=none] { }
+  child { node [treenode] {$\smath{\ans\True}$}
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}%

slides/Makefile

@@ -0,0 +1,32 @@
+TEXC=pdflatex
+CFLAGS=-interaction=nonstopmode -halt-on-error -file-line-error
+BIBC=bibtex
+PAPER=viva
+BIBLIO=$(PAPER)
+LATEST_COMMIT=$(shell git log --format="%h" -n 1)
+
+all: $(PAPER).pdf
+draft: $(PAPER).pdf-draft
+
+$(PAPER).aux: $(PAPER).tex
+	$(TEXC) $(CFLAGS) $(PAPER)
+
+$(BIBLIO).bbl: $(PAPER).aux $(BIBLIO).bib
+	$(BIBC) $(PAPER)
+
+$(PAPER).pdf: $(PAPER).aux $(BIBLIO).bbl
+	$(TEXC) $(CFLAGS) $(PAPER)
+	$(TEXC) $(CFLAGS) $(PAPER)
+
+$(PAPER).pdf-draft: CFLAGS:=$(CFLAGS) "\def\DRAFT{$(LATEST_COMMIT)}\input{$(PAPER)}"
+$(PAPER).pdf-draft: all
+	mv $(PAPER).pdf $(PAPER)-draft.pdf
+	tar cf thesis-draft.tar.gz $(PAPER)-draft.pdf
+
+clean:
+	rm -f *.log *.aux *.toc *.out
+	rm -f *.bbl *.blg *.fls *.xml
+	rm -f *.nav *.snm
+	rm -f *.fdb_latexmk *.vtc *.cut
+	rm -f $(PAPER).pdf camera-ready.pdf submission.pdf
+	rm -f *.o *.cmx *.cmo

slides/viva.bib

@@ -0,0 +1,82 @@
+@inproceedings{HillerstromL16,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley},
+  title     = {Liberating effects with rows and handlers},
+  booktitle = {TyDe@ICFP},
+  pages     = {15--27},
+  publisher = {{ACM}},
+  year      = {2016}
+}
+
+@inproceedings{HillerstromLAS17,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               Robert Atkey and
+               {KC} Sivaramakrishnan},
+  title     = {Continuation Passing Style for Effect Handlers},
+  booktitle = {{FSCD}},
+  series    = {LIPIcs},
+  volume    = {84},
+  pages     = {18:1--18:19},
+  OPTpublisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
+  year      = {2017}
+}
+
+@inproceedings{HillerstromL18,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley},
+  title     = {Shallow Effect Handlers},
+  booktitle = {{APLAS}},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
+  volume    = {11275},
+  pages     = {415--435},
+  publisher = {Springer},
+  year      = {2018}
+}
+
+@article{HillerstromLA20,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               Robert Atkey},
+  title     = {Effect handlers via generalised continuations},
+  journal   = {J. Funct. Program.},
+  volume    = {30},
+  pages     = {e5},
+  year      = {2020}
+}
+
+@article{HillerstromLL20,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               John Longley},
+  title     = {Effects for Efficiency: Asymptotic Speedup with First-Class Control},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {4},
+  number    = {{ICFP}},
+  pages     = {100:1--100:29},
+  year      = {2020}
+}
+
+# Unix
+@article{RitchieT74,
+  author    = {Dennis Ritchie and
+               Ken Thompson},
+  title     = {The {UNIX} Time-Sharing System},
+  journal   = {Commun. {ACM}},
+  volume    = {17},
+  number    = {7},
+  pages     = {365--375},
+  year      = {1974}
+}
+
+# CEK & C
+@InProceedings{FelleisenF86,
+  title={Control Operators, the {SECD}-machine, and the $\lambda$-Calculus},
+  author={Felleisen, Matthias and Friedman, Daniel P.},
+  year=1987,
+  booktitle = {Formal Description of Programming Concepts III},
+  OPTbooktitle = {The Proceedings of the Conference on Formal Description of Programming Concepts III, Ebberup, Denmark},
+  pages     = {193--217},
+  OPTpublisher={North Holland}
+}

slides/viva.tex

@@ -0,0 +1,201 @@
+\documentclass[169,10pt,compress,dvipsnames]{beamer}
+%%
+%% Slides layout
+%%
+\beamertemplatenavigationsymbolsempty  % hides navigation buttons
+\usetheme{Madrid}                      % standard Madrid theme
+\setbeamertemplate{footline}{}         % renders the footer empty
+%
+\setbeamertemplate{bibliography item}{ % this is a hack to prevent Madrid theme + biblatex
+  \hspace{-0.4cm}\lower3pt\hbox{       % from causing bibliography entries to run over
+    \pgfuseimage{beamericonarticle}    % the slide margins
+}}
+
+%%
+%% Packages
+%%
+\usepackage[utf8]{inputenc}               % enable UTF-8 compatible typing
+\usepackage{hyperref}                     % interactive PDF
+\usepackage[sort&compress,square,numbers]{natbib}    % Bibliography
+\usepackage{bibentry}         % Print bibliography entries inline.
+\makeatletter                 % Redefine bibentry to omit hyperrefs
+\renewcommand\bibentry[1]{\nocite{#1}{\frenchspacing
+     \@nameuse{BR@r@#1\@extra@b@citeb}}}
+\makeatother
+\nobibliography*              % use the bibliographic data from the standard BibTeX setup.
+\usepackage{amsmath,amssymb,mathtools}    % maths typesetting
+\usepackage{../pkgs/mathpartir}           % Inference rules
+\usepackage{../pkgs/mathwidth}            % renders character sequences nicely in math mode
+\usepackage{stmaryrd}                     % semantic brackets
+\usepackage{xspace}                       % proper spacing for macros in text
+
+\usepackage[T1]{fontenc}                  % 8-bit font encoding
+                                          % native support for accented characters.
+\usepackage[scaled=0.85]{beramono}        % smoother typewriter font
+\newcommand*{\Scale}[2][4]{\scalebox{#1}{\ensuremath{#2}}}%
+
+\input{../macros.tex}
+
+%%
+%% Meta information
+%%
+\author{Daniel Hillerström}
+\title{Foundations for Programming and Implementing Effect Handlers}
+\institute{The University of Edinburgh, Scotland UK}
+\subtitle{PhD viva}
+\date{August 13, 2021}
+
+%%
+%% Slides
+%%
+\begin{document}
+
+%
+% Title slide
+%
+\begin{frame}
+  \maketitle
+\end{frame}
+
+% Dissertation overview
+\begin{frame}
+  \frametitle{My dissertation at glance}
+
+  Three main strands of work
+
+  \begin{description}
+  \item[Programming] Language design and applications of effect handlers.
+  \item[Implementation] Canonical implementation strategies for effect handlers.
+  \item[Expressiveness] Exploration of the computational expressiveness of effect handlers.
+  \end{description}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Calculi for deep, shallow, and parameterised handlers}
+
+  The calculi capture key aspects of the implementation of effect
+  handlers in Links.
+
+  \begin{itemize}
+    \item $\HCalc$ ordinary deep handlers (fold).
+    \item $\SCalc$ shallow handlers (case-split).
+    \item $\HPCalc$ parameterised deep handlers (fold+state).
+  \end{itemize}
+
+  The actual implementation is the union of the three calculi.\\[2em]
+
+  \textbf{Relevant papers} TyDe'16~\cite{HillerstromL16},
+  APLAS'18~\cite{HillerstromL18}, JFP'20~\cite{HillerstromLA20}.
+\end{frame}
+
+% UNIX
+\begin{frame}
+  \frametitle{Effect handlers as composable operating systems}
+
+  An interpretation of \citeauthor{RitchieT74}'s
+  UNIX~\cite{RitchieT74} in terms of effect handlers.\\[2em]
+
+  \[
+    \bl
+    \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\textbf{Basic idea}
+      \ba[m]{@{\qquad}r@{~}c@{~}l}
+        \text{\emph{system call}} &\approx& \text{\emph{operation invocation}}\\
+        \text{\emph{system call implementation}} &\approx& \text{\emph{operation interpretation}}
+      \ea
+    \el
+  \]\hfill\\[2em]
+
+  \textbf{Key point} Legacy code is modularly retrofitted with functionality.
+\end{frame}
+
+% CPS translation
+\begin{frame}
+  \frametitle{CPS transforms for effect handlers}
+
+  A higher-order CPS transform for effect handlers with generalised
+  continuations.\\[1em]
+
+  \textbf{Generalised continuation} Structured representation of
+  delimited continuations.\\[0.5em]
+
+  \[
+    \Scale[1.8]{\kappa = \overline{(\sigma, (\hret,\hops))}}
+  \]\\[1em]
+
+  \textbf{Key point} Separate the \emph{doing} layer ($\sigma$) from the \emph{being} layer ($H$).\\[2em]
+
+  \textbf{Relevant papers} FSCD'17~\cite{HillerstromLAS17},
+  APLAS'18~\cite{HillerstromL18}, JFP'20~\cite{HillerstromLA20}.
+\end{frame}
+
+% Abstract machine
+\begin{frame}
+  \frametitle{Abstract machine semantics for effect handlers}
+
+  Plugging generalised continuations into \citeauthor{FelleisenF86}'s
+  CEK machine~\cite{FelleisenF86} yields a runtime for effect
+  handlers.\\[2em]
+
+  \[
+    \Scale[2]{\cek{C \mid E \mid K = \overline{(\sigma, (H,E))}}}
+  \]\\[2em]
+
+  \textbf{Relevant papers} TyDe'16~\cite{HillerstromL16},
+  JFP'20~\cite{HillerstromLA20}.
+
+\end{frame}
+
+% Interdefinability of handlers
+\begin{frame}
+  \frametitle{Interdefinability of effect handlers}
+
+  Deep, shallow, and parameterised handlers are interdefinable
+  w.r.t. to typability-preserving macro-expressiveness.
+
+  \begin{itemize}
+    \item Deep as shallow, $\mathcal{D}\llbracket - \rrbracket$, image is computationally lightweight.
+    \item Shallow as deep, $\mathcal{S}\llbracket - \rrbracket$, image is computationally expensive.
+    \item Parameterised as deep, $\mathcal{P}\llbracket - \rrbracket$,
+      image uses explicit state-passing.
+    \end{itemize}
+    ~\\[1em]
+    \textbf{Relevant papers} APLAS'18~\cite{HillerstromL18},
+    JFP'20~\cite{HillerstromLA20}.
+
+\end{frame}
+
+% Asymptotic speed up with first-class control
+\begin{frame}
+  \frametitle{Asymptotic speed up with effect handlers}
+
+  Effect handlers can make some programs faster!
+
+  \[
+    \Count_n : ((\Nat_n \to \Bool) \to \Bool) \to \Nat
+  \]\\[1em]
+  %
+  Using type-respecting expressiveness
+  \begin{itemize}
+  \item There \textbf{exists} an implementation of $\Count_n \in \HPCF$ with
+    effect handlers such that the runtime for every $n$-standard predicate $P$ is
+    $\Count_n~P = \BigO(2^n)$.
+  \item \textbf{Forall} implementations of $\Count_n \in \BPCF$ the runtime for every $n$-standard predicate $P$ is $\Count_n~P = \Omega(n2^n)$
+  \end{itemize}
+  ~\\[1em]
+  \textbf{Relevant paper} ICFP'20~\cite{HillerstromLL20}.
+\end{frame}
+
+% Background
+% \begin{frame}
+%   \frametitle{Continuations literature review}
+% \end{frame}
+
+%
+% References
+%
+\begin{frame}%[allowframebreaks]
+  \frametitle{References}
+  \bibliographystyle{plainnat}
+  \bibliography{\jobname}
+\end{frame}
+\end{document}