diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index fdc031054..e72d2c245 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -4,7 +4,6 @@ Contributing to Idris 2
 Contributions are welcome! The most important things needed at this stage,
 beyond work on the language core, are (in no particular order):
 
-* CI integration.
 * Documentation string support (at the REPL and IDE mode).
 * Generating HTML documentation from documentation strings (and possibly other
   formations)
@@ -22,8 +21,6 @@ beyond work on the language core, are (in no particular order):
   - (Not really part of Idris 2, but an editing mode for vim would be lovely!)
 * Some parts of the Idris 1 Prelude are not yet implemented and should be
   added to base/
-* Partial evaluation, especially for specialisation of interface 
-  implementations.
 * The lexer and parser are quite slow, new and faster versions with better
   errors would be good.
   - In particular, large sections commented out with {- -} can take a while
@@ -47,8 +44,6 @@ notably:
   - This will necessarily be slightly different from Idris 1 since the
     elaborator works differently. It would also be nice to extend it with
     libraries and perhaps syntax for deriving implementations of interfaces.
-* `%default` directives, since coverage and totality checking have not been well
-  tested yet.
 
 Other contributions are also welcome, but I (@edwinb) will need to be
 confident that I'll be able to maintain them!
@@ -74,11 +69,6 @@ behaviour might be useful in a proof (so very small definitions) are
 Syntax
 ------
 
-Some syntax that hasn't yet been implemented but will be:
-
-* Idiom brackets
-* !-notation [needs some thought about the exact rules]
-
 Some things from Idris 1 definitely won't be implemented:
 
 * `%access` directives, because it's too easy to export things by accident
diff --git a/docs/source/app/exceptionsstate.rst b/docs/source/app/exceptionsstate.rst
new file mode 100644
index 000000000..d95bf0014
--- /dev/null
+++ b/docs/source/app/exceptionsstate.rst
@@ -0,0 +1,88 @@
+Exceptions and State
+====================
+
+``Control.App`` is primarily intended to make it easier to manage the common
+cases of applications with exceptions and state. We can throw and catch
+exceptions listed in the environment (the ``e`` parameter to ``App``) and
+introduce new global state.
+
+Exceptions
+----------
+
+The ``Environment`` is a list of error types, usable via the
+``Exception`` interface defined in ``Control.App``:
+
+.. code-block:: idris
+
+    interface Exception err e where
+      throw : err -> App e a
+      catch : App e a -> (err -> App e a) -> App e a
+
+We can use ``throw`` and ``catch`` for some exception type
+``err`` as long as the exception type exists in the environment. This is
+checked with the ``HasErr`` predicate, also defined in ``Control.App``:
+
+.. code-block:: idris
+
+    data HasErr : Type -> Environment -> Type where
+         Here : HasErr e (e :: es)
+         There : HasErr e es -> HasErr e (e' :: es)
+
+    HasErr err e => Exception err e where ...
+
+Note the ``HasErr`` constraint on ``Exception``: this is one place
+where it is notationally convenient that the ``auto`` implicit mechanism
+and the interface resolution mechanism are identical in Idris 2.
+Finally, we can introduce new exception types via ``handle``, which runs a
+block of code which might throw, handling any exceptions:
+
+.. code-block:: idris
+
+    handle : App (err :: e) a -> (onok : a -> App e b) ->
+             (onerr : err -> App e b) -> App e b
+
+Adding State
+------------
+
+Applications will typically need to keep track of state, and we support
+this primitively in ``App`` using a ``State`` type, defined in
+``Control.App``:
+
+.. code-block:: idris
+
+    data State : (tag : a) -> Type -> Environment -> Type
+
+The ``tag`` is used purely to distinguish between different states,
+and is not required at run-time, as explicitly stated in the types of
+``get`` and ``put``, which are used to access and update a state:
+
+.. code-block:: idris
+
+    get : (0 tag : a) -> State tag t e => App {l} e t
+    put : (0 tag : a) -> State tag t e => t -> App {l} e ()
+
+These use an ``auto``-implicit to pass around
+a ``State`` with the relevant ``tag`` implicitly, so we refer
+to states by tag alone. In ``helloCount`` earlier, we used an empty type
+\texttt{Counter} as the tag:
+
+.. code-block:: idris
+
+    data Counter : Type where -- complete definition
+
+The environment ``e`` is used to ensure that
+states are only usable in the environment in which they are introduced.
+States are introduced using ``new``:
+
+.. code-block:: idris
+
+    new : t -> (1 p : State tag t e => App {l} e a) -> App {l} e a
+
+Note that the type tells us ``new`` runs the program with the state
+exactly once.
+Rather than using ``State`` and ``Exception`` directly, however,
+we typically use interfaces to constrain the operations which are allowed
+in an environment. Internally, ``State`` is implemented via an
+``IORef``, primarily for performance reasons.
+
+
diff --git a/docs/source/app/index.rst b/docs/source/app/index.rst
index 190e7ccd6..f24b8765d 100644
--- a/docs/source/app/index.rst
+++ b/docs/source/app/index.rst
@@ -46,4 +46,11 @@ We begin by introducing ``App``, with some small example
 programs, then show how to extend it with exceptions, state, and other
 interfaces.
 
-[To be continued...]
+.. toctree::
+   :maxdepth: 1
+
+   introapp
+   exceptionsstate
+   interfaces
+   linear
+
diff --git a/docs/source/app/interfaces.rst b/docs/source/app/interfaces.rst
new file mode 100644
index 000000000..1c1fba248
--- /dev/null
+++ b/docs/source/app/interfaces.rst
@@ -0,0 +1,148 @@
+Defining Interfaces
+===================
+
+The only way provided by ``Control.App`` to run an ``App`` is
+via the ``run`` function, which takes a concrete environment
+``Init``.
+All concrete extensions to this environment are via either ``handle``,
+to introduce a new exception, or ``new``, to introduce a new state.
+In order to compose ``App`` programs effectively, rather than
+introducing concrete exceptions and state in general, we define interfaces for
+collections of operations which work in a specific environment.
+
+Example: Console I/O
+--------------------
+
+We have seen an initial example using the ``Console`` interface,
+which is declared as follows, in ``Control.App.Console``:
+
+.. code-block:: idris
+
+    interface Console e where
+      putStr : String -> App {l} e ()
+      getStr : App {l} e String
+
+It provides primitives for writing to and reading from the console, and
+generalising the path parameter to ``l`` means that neither can
+throw an exception, because they have to work in both the ``NoThrow``
+and ``MayThrow`` contexts.
+
+To implement this for use in a top level ``IO``
+program, we need access to primitive ``IO`` operations.
+The ``Control.App`` library defines a primitive interface for this:
+
+.. code-block:: idris
+
+    interface PrimIO e where
+      primIO : IO a -> App {l} e a
+      fork : (forall e' . PrimIO e' => App {l} e' ()) -> App e ()
+
+We use ``primIO`` to invoke an ``IO`` function. We also have a ``fork``
+primitive, which starts a new thread in a new environment supporting
+``PrimIO``.  Note that ``fork`` starts a new environment ``e'`` so that states
+are only available in a single thread.
+
+There is an implementation of ``PrimIO`` for an environment which can
+throw the empty type as an exception. This means that if ``PrimIO``
+is the only interface available, we cannot throw an exception, which is
+consistent with the definition of ``IO``. This also allows us to
+use ``PrimIO`` in the initial environment ``Init``.
+
+.. code-block:: idris
+
+    HasErr Void e => PrimIO e where ...
+
+Given this, we can implement \texttt{Console} and run our \texttt{hello}
+program in ``IO``. It is implemented as follows in ``Control.App.Console``:
+
+.. code-block:: idris
+
+    PrimIO e => Console e where
+      putStr str = primIO $ putStr str
+      getStr = primIO $ getLine
+
+Example: File I/O
+-----------------
+
+Console I/O can be implemented directly, but most I/O operations can fail.
+For example, opening a file can fail for several reasons: the file does not
+exist; the user has the wrong permissions, etc. In Idris, the ``IO``
+primitive reflects this in its type:
+
+.. code-block:: idris
+
+    openFile : String -> Mode -> IO (Either FileError File)
+
+While precise, this becomes unwieldy when there are long sequences of
+``IO`` operations. Using ``App``, we can provide an interface
+which throws an exception when an operation fails, and guarantee that any 
+exceptions are handled at the top level using ``handle``.
+We begin by defining the ``FileIO`` interface, in ``Control.App.FileIO``:
+
+.. code-block:: idris
+
+    interface Has [Exception IOError] e => FileIO e where
+      withFile : String -> Mode ->  (onError : IOError -> App e a) ->
+                 (onOpen : File -> App e a) -> App e a
+      fGetStr : File -> App e String
+      fPutStr : File -> String -> App e ()
+      fEOF : File -> App e Bool
+
+We use resource bracketing - passing a function to ``withFile`` for working
+with the opened file - rather than an explicit ``open`` operation,
+to open a file, to ensure that the file handle is cleaned up on 
+completion.
+
+One could also imagine an interface using a linear resource for the file, which
+might be appropriate in some safety critical contexts, but for most programming
+tasks, exceptions should suffice.
+All of the operations can fail, and the interface makes this explicit by
+saying we can only implement ``FileIO`` if the environment supports
+throwing and catching the ``IOError`` exception. ``IOError`` is defined
+in ``Control.App``.
+
+For example, we can use this interface to implement ``readFile``, throwing
+an exception if opening the file fails in ``withFile``:
+
+.. code-block:: idris
+
+    readFile : FileIO e => String -> App e String
+    readFile f = withFile f Read throw $ \h =>
+                   do content <- read [] h
+                      pure (concat content)
+    where
+      read : List String -> File -> App e (List String)
+      read acc h = do eof <- fEOF h
+                      if eof then pure (reverse acc)
+                             else do str <- fGetStr h
+                                     read (str :: acc) h
+
+Again, this is defined in ``Control.App.FileIO``.
+
+To implement ``FileIO``, we need access to the primitive operations
+via ``PrimIO``, and the ability to throw exceptions if any of the
+operations fail. With this, we can implement ``withFile`` as follows,
+for example:
+
+.. code-block:: idris
+
+    Has [PrimIO, Exception IOError] e => FileIO e where
+      withFile fname m onError proc
+          = do Right h <- primIO $ openFile fname m
+                  | Left err => onError (FileErr (toFileEx err))
+               res <- catch (proc h) onError
+               pure res
+      ...
+
+Given this implementation of ``FileIO``, we can run ``readFile``,
+provided that we wrap it in a top level ``handle`` function to deal
+with any errors thrown by ``readFile``:
+
+.. code-block:: idris
+
+    readMain : String -> App Init ()
+    readMain fname = handle (readFile fname)
+           (\str => putStrLn $ "Success:\n" ++ show str)
+           (\err : IOError => putStrLn $ "Error: " ++ show err)
+
+
diff --git a/docs/source/app/introapp.rst b/docs/source/app/introapp.rst
new file mode 100644
index 000000000..0e1c3f2aa
--- /dev/null
+++ b/docs/source/app/introapp.rst
@@ -0,0 +1,108 @@
+Introducing App
+===============
+
+``App`` is declared as below, in a module ``Control.App``, which is part of
+the ``base`` libraries.
+It is parameterised by an implicit
+``Path`` (which states whether the program's execution path
+is linear or might throw
+exceptions), which has a ``default`` value that the program
+might throw, and an ``Environment``
+(which gives a list of exception types which can be thrown, and is
+a synonym for ``List Type``):
+
+.. code-block:: idris
+
+    data App : {default MayThrow l : Path} ->
+               (e : Environment) -> Type -> Type
+
+It serves the same purpose as ``IO``, but supports throwing and catching
+exceptions, and allows us to define more constrained interfaces parameterised
+by the environment ``e``. 
+e.g. a program which supports console IO:
+
+.. code-block:: idris
+
+    hello : Console e => App e ()
+    hello = putStrLn "Hello, App world!"
+
+We can use this in a complete program as follows:
+
+.. code-block:: idris
+
+    module Main
+
+    import Control.App
+    import Control.App.Console
+
+    hello : Console e => App e ()
+    hello = putStrLn "Hello, App world!"
+
+    main : IO ()
+    main = run hello
+
+Or, a program which supports console IO and carries an ``Int`` state,
+labelled ``Counter``:
+
+.. code-block:: idris
+
+    data Counter : Type where
+
+    helloCount : (Console e, State Counter Int e) => App e ()
+    helloCount = do c <- get Counter
+                    put Counter (c + 1)
+                    putStrLn "Hello, counting world"
+                    c <- get Counter
+                    putStrLn ("Counter " ++ show c)
+
+To run this as part of a complete program, we need to initialise the state.
+
+.. code-block:: idris
+
+    main : IO ()
+    main = run (new 93 helloCount)
+
+For convenience, we can list multiple interfaces in one go, using a function
+``Has``, defined in ``Control.App``, to compute the interface constraints:
+
+.. code-block:: idris
+
+    helloCount : Has [Console, State Counter Int] e => App e ()
+
+    0 Has : List (a -> Type) -> a -> Type
+    Has [] es = ()
+    Has (e :: es') es = (e es, Has es' es)
+
+The purpose of ``Path`` is to state whether a program can throw
+exceptions, so that we can know where it is safe to reference linear
+resources. It is declared as follows:
+
+.. code-block:: idris
+
+    data Path = MayThrow | NoThrow
+
+The type of ``App`` states that ``MayThrow`` is the default.
+We expect this to be the most
+common case. After all, realistically, most operations have possible failure
+modes, especially those which interact with the outside world.
+
+The ``0`` on the declaration of ``Has`` indicates that it can only
+be run in an erased context, so it will never be run at run-time.
+To run an ``App`` inside ``IO``, we use an initial
+environment ``Init`` (recall that an ``Environment`` is a
+``List Type``):
+
+.. code-block:: idris
+
+    Init : Environment
+    Init = [Void]
+
+    run : App {l} Init a -> IO a
+
+Generalising the ``Path`` parameter with ``l``
+means that we can invoke ``run`` for any application, whether the ``Path``
+is ``NoThrow`` or ``MayThrow``. But, in practice, all applications
+given to ``run`` will not throw at the top level, because the only
+exception type available is the empty type ``Void``. Any exceptions
+will have been introduced and handled inside the ``App``.
+
diff --git a/docs/source/app/linear.rst b/docs/source/app/linear.rst
new file mode 100644
index 000000000..c222155fe
--- /dev/null
+++ b/docs/source/app/linear.rst
@@ -0,0 +1,253 @@
+Linear Resources
+================
+
+We have introduced ``App`` for writing 
+interactive programs, using interfaces to constrain which operations are
+permitted, but have not yet seen the ``Path`` parameter in action.
+Its purpose is to constrain when programs can throw exceptions,
+to know where linear resource usage is allowed. The bind operator
+for ``App`` is defined as follows (not via ``Monad``):
+
+.. code-block:: idris
+
+    data SafeBind : Path -> (l' : Path) -> Type where
+         SafeSame : SafeBind l l
+         SafeToThrow : SafeBind NoThrow MayThrow
+
+    (>>=) : SafeBind l l' =>
+            App {l} e a -> (a -> App {l=l'} e b) -> App {l=l'} e b
+
+The intuition behind this type is that, when sequencing two ``App``
+programs:
+
+* if the first action might throw an exception, then the whole program might
+  throw.
+* if the first action cannot throw an exception, the second action can still
+  throw, and the program as a whole can throw.
+* if neither action can throw an exception, the program as a whole cannot
+  throw.
+
+The reason for the detail in the type is that it is useful to be able to
+sequence programs with a different ``Path``, but in doing so, we must
+calculate the resulting ``Path`` accurately.
+Then, if we want to sequence subprograms with linear variables,
+we can use an alternative bind operator which guarantees to run the
+continuation exactly once:
+
+.. code-block:: idris
+
+    bindL : App {l=NoThrow} e a -> 
+            (1 k : a -> App {l} e b) -> App {l} e b
+
+To illustrate the need for ``bindL``, we can try writing a program which
+tracks the state of a secure data store, which requires logging in before
+reading the data.
+
+Example: a data store requiring a login
+---------------------------------------
+
+Many software components rely on some form of state, and there may be
+operations which are only valid in specific states. For example, consider
+a secure data store in which a user must log in before getting access to
+some secret data. This system can be in one of two states:
+
+* ``LoggedIn``, in which the user is allowed to read the secret
+* ``LoggedOut``, in which the user has no access to the secret
+
+We can provide commands to log in, log out, and read the data, as illustrated
+in the following diagram:
+
+|login|
+
+The ``login`` command, if it succeeds, moves the overall system state from
+``LoggedOut`` to ``LoggedIn``. The ``logout`` command moves the state from
+``LoggedIn`` to ``LoggedOut``. Most importantly, the ``readSecret`` command
+is only valid when the system is in the ``LoggedIn`` state.
+
+We can represent the state transitions using functions with linear types.
+To begin, we define an interface for connecting to and disconnecting from
+a store:
+
+.. code-block:: idris
+
+    interface StoreI e where
+        connect : (1 prog : (1 d : Store LoggedOut) ->
+                  App {l} e ()) -> App {l} e ()
+        disconnect : (1 d : Store LoggedOut) -> App {l} e ()
+
+Neither ``connect`` nor ``disconnect`` throw, as shown by
+generalising over ``l``. Once we
+have a connection, we can use the following functions to
+access the resource directly:
+
+.. code-block:: idris
+
+    data Res : (a : Type) -> (a -> Type) -> Type where
+         (@@) : (val : a) -> (1 resource : r val) -> Res a r
+
+    login : (1 s : Store LoggedOut) -> (password : String) ->
+            Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut))
+    logout : (1 s : Store LoggedIn) -> Store LoggedOut
+    readSecret : (1 s : Store LoggedIn) -> 
+                 Res String (const (Store LoggedIn))
+
+``Res`` is defined in ``Control.App`` since it is commonly useful.  It is a
+dependent pair type, which associates a value with a linear resource.
+We'll leave the other definitions abstract, for the purposes of this
+introductory example.
+
+The following listing shows a complete program accessing the store, which
+reads a password, accesses the store if the password is correct and prints the
+secret data. It uses ``let (>>=) = bindL`` to redefine
+``do``-notation locally.
+
+.. code-block:: idris
+
+    storeProg : Has [Console, StoreI] e => App e ()
+    storeProg = let (>>=) = bindL in
+          do putStr "Password: "
+             password <- getStr
+             connect $ \s =>
+               do let True @@ s = login s password
+                    | False @@ s => do putStrLn "Wrong password"
+                                       disconnect s
+                  let str @@ s = readSecret s
+                  putStrLn $ "Secret: " ++ show str
+                  let s = logout s
+                  disconnect s
+
+If we omit the ``let (>>=) = bindL``, it will use the default
+``(>>=)`` operator, which allows the continuation to be run multiple
+times, which would mean that ``s`` is not guaranteed to be accessed
+linearly, and ``storeProg`` would not type check.
+We can safely use ``getStr`` and ``putStr`` because they
+are guaranteed not to throw by the ``Path`` parameter in their types.
+
+.. |login| image:: ../image/login.png
+                   :width: 500px
+
+App1: Linear Interfaces
+-----------------------
+
+Adding the ``bindL`` function to allow locally rebinding the
+``(>>=)`` operator allows us to combine existing linear resource
+programs with operations in ``App`` - at least, those that don't throw.
+It would nevertheless be nice to interoperate more directly with ``App``.
+One advantage of defining interfaces is that we can provide multiple
+implementations for different contexts, but our implementation of the
+data store uses primitive functions (which we left undefined in any case)
+to access the store.
+
+To allow control over linear resources, ``Control.App`` provides an alternative
+parameterised type ``App1``:
+
+.. code-block:: idris
+
+    data App1 : {default One u : Usage} ->
+                (e : Environment) -> Type -> Type
+
+There is no need for a ``Path`` argument, since linear programs can
+never throw. The ``Usage`` argument states whether the value
+returned is to be used once, or has unrestricted usage, with
+the default in ``App1`` being to use once:
+
+.. code-block:: idris
+
+    data Usage = One | Any
+
+The main difference from ``App`` is the ``(>>=)`` operator, which
+has a different multiplicity for the variable bound by the continuation
+depending on the usage of the first action:
+
+.. code-block:: idris
+
+    Cont1Type : Usage -> Type -> Usage -> Environment -> 
+                Type -> Type
+    Cont1Type One a u e b = (1 x : a) -> App1 {u} e b
+    Cont1Type Any a u e b = (x : a) -> App1 {u} e b
+
+    (>>=) : {u : _} -> (1 act : App1 {u} e a) ->
+            (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b
+
+``Cont1Type`` returns a continuation which uses the argument linearly,
+if the first ``App1`` program has usage ``One``, otherwise it
+returns a continuation where argument usage is unrestricted. Either way,
+because there may be linear resources in scope, the continuation is
+run exactly once and there can be no exceptions thrown.
+
+Using ``App1``, we can define all of the data store operations in a
+single interface, as shown in the following listing.
+Each operation other than ``disconnect`` returns a `linear` resource.
+
+.. code-block:: idris
+
+    interface StoreI e where
+      connect : App1 e (Store LoggedOut)
+      login : (1 d : Store LoggedOut) -> (password : String) ->
+              App1 e (Res Bool (\ok => Store (if ok then LoggedIn 
+                                                    else LoggedOut))
+      logout : (1 d : Store LoggedIn) -> App1 e (Store LoggedOut)
+      readSecret : (1 d : Store LoggedIn) ->
+                   App1 e (Res String (const (Store LoggedIn)))
+      disconnect : (1 d : Store LoggedOut) -> App {l} e ()
+
+We can explicitly move between ``App`` and ``App1``:
+
+.. code-block:: idris
+
+    app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a
+    app1 : (1 p : App1 {u=Any} e a) -> App {l} e a
+
+We can run an ``App`` program using ``app``, inside ``App1``,
+provided that it is guaranteed not to throw. Similarly, we can run an
+``App1`` program using ``app1``, inside ``App``, provided that
+the value it returns has unrestricted usage. So, for example, we can
+write:
+
+.. code-block:: idris
+
+    storeProg : Has [Console, StoreI] e => App e ()
+    storeProg = app1 $ do
+         store <- connect
+         app $ putStr "Password: "
+         ?what_next
+
+This uses ``app1`` to state that the body of the program is linear,
+then ``app`` to state that the ``putStr`` operation is in
+``App``. We can see that ``connect`` returns a linear resource
+by inspecting the hole ``what_next``, which also shows that we are
+running inside ``App1``:
+
+.. code-block:: idris
+
+     0 e : List Type
+     1 store : Store LoggedOut
+    -------------------------------------
+    what_next : App1 e ()
+
+For completeness, one way to implement the interface is as follows, with
+hard coded password and internal data:
+
+.. code-block:: idris
+
+    Has [Console] e => StoreI e where
+      connect
+          = do app $ putStrLn "Connect"
+               pure1 (MkStore "xyzzy")
+
+      login (MkStore str) pwd
+          = if pwd == "Mornington Crescent"
+               then pure1 (True @@ MkStore str)
+               else pure1 (False @@ MkStore str)
+      logout (MkStore str) = pure1 (MkStore str)
+      readSecret (MkStore str) = pure1 (str @@ MkStore str)
+
+      disconnect (MkStore _)
+          = putStrLn "Door destroyed"
+
+Then we can run it in ``main``:
+
+.. code-block:: idris
+
+    main : IO ()
+    main = run storeProg
diff --git a/docs/source/image/login.png b/docs/source/image/login.png
new file mode 100644
index 000000000..a9447e1f6
Binary files /dev/null and b/docs/source/image/login.png differ