diff --git a/Control/Concurrent/SimpleSession/Examples/Implicit.lhs b/Control/Concurrent/SimpleSession/Examples/Implicit.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/Examples/Implicit.lhs
@@ -0,0 +1,119 @@
+\subsection{Implicit Channel Examples}
+\label{sec:examples:implicit}
+\ignore{
+
+> {-# OPTIONS -F -pgmF ixdopp #-}
+> module Control.Concurrent.SimpleSession.Examples.Implicit where
+>
+> import Control.Concurrent (forkIO)
+>
+> import Control.Concurrent.SimpleSession.Implicit
+
+}
+
+In these examples, we use |ixdo| notation for indexed monads,
+analogous to |do| notation for monads.  This syntax is implemented by a
+preprocessor.
+
+\paragraph{A print server.}
+
+As an example, we implement a simple print server.
+The client side of the print server protocol is:
+\begin{enumerate}
+  \item Choose either to finish or to continue.
+  \item Send a string.
+  \item Go to step 1.
+\end{enumerate}
+
+We first implement the server.
+
+> server = enter >>>= \_ -> loop where
+>   loop = offer close
+>                (ixdo
+>                   s <- recv
+>                   io (putStrLn s)
+>                   zero
+>                   loop)
+
+GHC's type checker can infer that |server|'s
+session type is |Rec (Eps :&: (String :?: Var Z))|.
+
+%include fig-operationtypes.tex
+
+The client reads user input, which it sends to the server for printing.
+When the user tells the client to quit, it sends one more string to the
+server, tells the server to quit, and closes the channel.
+
+> client = enter >>>= \_ -> loop 0 where
+>   loop count = ixdo
+>     s <- io getLine
+>     case s of
+>       "q" -> ixdo
+>                sel2
+>                send (show count ++ " lines sent")
+>                zero; sel1; close
+>       _   -> ixdo
+>                sel2; send s
+>                zero; loop (count + 1)
+
+GHC infers the session type
+|Rec (Eps :+: (String :!: Var Z))| for
+|client|, which is clearly dual to the type inferred for |server| above.
+
+We run a session by creating a new |Rendezvous|, having the server
+accept in a new thread, and having the client request in the main thread.
+
+> runPrintSession = do
+>   rv <- newRendezvous
+>   forkIO (accept rv server)
+>   request rv client
+
+\paragraph{An example of subtyping.}
+\label{sec:subtyping}
+
+Our implementation provides a form of protocol subtyping.
+Consider a reimplementation of Gay and Hole's \citeyearpar{r:gay99}
+arithmetic server, which provides two services, addition and negation:
+
+> server1 = offer
+>   (ixdo a <- recv
+>         b <- recv
+>         send (a + b)
+>         close)
+>   (ixdo a <- recv
+>         send (-a)
+>         close)
+
+The full protocol for |server1| is inferred:
+
+< (Integer :?: Integer :?: Integer :!: Eps) :&:
+< (Integer :?: Integer :!: Eps)
+
+A second server implements only the negation service:
+
+> server2 = offer
+>   close
+>   (ixdo a <- recv
+>         send (-a)
+>         close)
+
+Its protocol is inferred as well:
+
+< Eps :&: (Integer :?: Integer :!: Eps)
+
+A particular client may avail itself of only
+one of the offered services:
+
+> client' x = ixdo sel2; send x; y <- recv; close; ireturn y
+
+The client's protocol is inferred as |r :+: (a :!: b :?: Eps)|, which
+unifies with the duals of both servers' protocols.  Without the
+functional dependencies in |Dual|, however, attempting to connect the
+client with |server2| leads the type checker to complain that there
+is no instance of |Dual| for |r| and |Eps|; connecting |client| with
+|server1| also fails to type check.  The functional dependency nudges
+the type checker towards attempting to unify |r| with the corresponding
+part of either server's type, which then succeeds.  As a result, the
+|client| may be composed with both servers in the same program and
+never notices the difference.
+
diff --git a/Control/Concurrent/SimpleSession/Examples/Positional.lhs b/Control/Concurrent/SimpleSession/Examples/Positional.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/Examples/Positional.lhs
@@ -0,0 +1,220 @@
+\ignore{
+
+> {-# OPTIONS -F -pgmF ixdopp #-}
+> {-# LANGUAGE TypeOperators #-}
+> module Control.Concurrent.SimpleSession.Examples.Positional where
+>
+> import Control.Concurrent (threadDelay)
+> import Random
+>
+> import Control.Concurrent.SimpleSession.Positional
+
+}
+
+\subsection{An Example with Multiple Channels}
+\label{sec:example:multiple}
+
+As an example, we give an implementation of the Sutherland-Hodgman
+\citeyearpar{Sutherland1974Reentrant} reentrant polygon clipping algorithm,
+which takes a plane and a series of points representing the
+vertices of a polygon,
+and produces vertices for the polygon restricted to one side of the plane.
+\Citet{Shivers2006Continuations}
+present a stream transducer implementation, which we follow.  Each
+transducer takes one plane to clip by, and two |Rendezvous| objects for
+the same protocol.  It connects on both, and then receives original points
+on one channel and sends clipped points on the other.
+
+We assume that we have types |Plane| and |Point|, a predicate
+|above| that indicates whether a given point is on the visible side
+of a given plane, and a partial function |intersection| that computes
+where the line segment between two points intersects a plane.
+
+GHC infers all the types in this example.
+
+< type SendList a = Rec (Eps :+: (a :!: Var Z))
+<
+< clipper :: Plane -> Rendezvous (SendList Point)
+<            -> Rendezvous (SendList Point)
+<            -> Session x x ()
+< clipper plane inrv outrv =
+<   accept outrv $ \oc ->
+<   request inrv $ \ic -> ixdo
+<   let shutdown = ixdo close ic; sel1 oc; close oc
+<       put pt   = dig $ ixdo
+<         sel2 oc; send oc pt; zero oc
+<       -- Attempt to get a point; pass it to yes, or
+<       -- call no if there are no more:
+<       get no yes = offer ic no $ ixdo
+<         pt <- recv ic; zero ic; yes pt
+<       -- If the line crosses the plane, send the intersection point:
+<       putCross line =
+<         maybe (ireturn ()) put (line `intersect` plane)
+<       putIfVisible pt   =
+<         if pt `above` plane then put pt else ireturn ()
+<   dig (enter oc)
+<   enter ic
+<   get shutdown $ \pt0 ->
+<     let loop pt = ixdo
+<           putIfVisible pt
+<           get (putcross (pt, pt0) >>>= \_ -> shutdown)
+<               (\pt' -> ixdo putcross (pt,pt')
+<                             loop pt')
+<      in loop pt0
+
+\par
+We use |sendlist| to send a list of points to the first
+transducer in the pipeline, and we use |recvlist| to accumulate
+points produced by the last transducer.
+
+< sendlist :: [a] -> Rendezvous (SendList a)
+<          -> Session x x ()
+< sendlist xs rv = accept rv start where
+<   start oc = enter oc >>>= \_ -> loop xs where
+<     loop []     = ixdo sel1 oc; close oc
+<     loop (x:xs) = ixdo sel2 oc; send oc x
+<                        zero oc; loop xs
+<
+< recvlist :: Rendezvous (SendList a) -> Session x x [a]
+< recvlist rv = request rv start where
+<   start ic = enter ic >>>= \_ -> loop [] where
+<     loop acc = offer ic
+<       (close ic >>>= \_ -> ireturn (reverse acc))
+<       (recv ic >>>= \x -> zero ic >>>= \_ -> loop (x : acc))
+
+\par
+Given a list of planes and a list of points, |clipMany| starts a |clipper|
+for each plane in a separate thread.  It starts |sendlist| a new thread,
+giving it the list of points and connecting it to the first |clipper|.
+It then runs |recvlist| in the main thread to gather up the result.
+
+< clipMany :: [Plane] -> [Point] -> IO [Point]
+< clipMany planes points = runSession $ ixdo
+<     rv <- io newRendezvous
+<     forkSession (sendlist points rv)
+<     let loop []     rv = recvlist rv
+<         loop (p:ps) rv = ixdo
+<           rv' <- io newRendezvous
+<           forkSession (clipper p rv rv')
+<           loop ps rv'
+<     loop planes rv
+
+\ignore{
+
+< bench n m = do
+<   g1 <- getStdRandom split
+<   g2 <- getStdRandom split
+<   let groupPoints (x:y:z:r) = Point x y z   : groupPoints r
+<       groupPlanes (a:b:c:r) = Plane a b c 0 : groupPlanes r
+<       points = groupPoints [ 10 * (x - 0.5) | x <- randoms g1 ]
+<       planes = groupPlanes [ 10 * (x - 0.5) | x <- randoms g2 ]
+<   points <- clipMany (take m planes) (take n points)
+<   print (length points)
+<
+< data Point = Point !Double !Double !Double
+< data Plane = Plane !Double !Double !Double !Double
+<
+< instance Show Point where
+<   showsPrec _ (Point x y z) =
+<     ('(':) . shows x . (", "++) . shows y . (", "++) . shows z . (')':)
+<
+< instance Show Plane where
+<   showsPrec _ (Plane a b c d) =
+<     shows a . ("x + "++) . shows b . ("y + "++) .
+<     shows c . ("z + "++) . shows d . (" = 0"++)
+< 
+< above :: Point -> Plane -> Bool
+< above (Point x y z) (Plane a b c d)
+<        = (a * x + b * y + c * z + d) / sqrt (a * a + b * b + c * c) > 0
+< 
+< intersect :: (Point, Point) -> Plane -> Maybe Point
+< intersect (p1@(Point x1 y1 z1), p2@(Point x2 y2 z2)) plane@(Plane a b c d)
+<            = if above p1 plane == above p2 plane
+<              then Nothing
+<              else Just (Point x y z) where
+<                x = x1 + (x2 - x1) * t
+<                y = y1 + (y2 - y1) * t
+<                z = z1 + (z2 - z1) * t
+<                t = (a * x1 + b * y1 + c * z1 + d) /
+<                    (a * (x1 - x2) + b * (y1 - y2) + c * (z1 - z2))
+
+> newPrinter = do
+>   spec <- newRendezvous
+>   let printer = ixdo
+>         clet c = accept spec
+>         offer c
+>           (recv c >>>= io . putStrLn >>>= \_ -> close c >>>= \_ -> printer)
+>           (close c)
+>   let say s    = runSession $
+>                    clet c = request spec in
+>                      ixdo sel1 c; send c s; close c
+>   let shutdown = runSession $
+>                    clet c = request spec in
+>                      sel2 c >>>= \_ -> close c
+>   runSession (forkSession printer)
+>   return (say, shutdown)
+>
+> logger say c = enter c >>>= \_ -> loop where
+>   loop =
+>     offer c
+>       (ixdo
+>          msg <- recv c
+>          io (say ("logger: " ++ msg))
+>          zero c
+>          loop)
+>       (ixdo
+>          io (say "logger: exiting")
+>          send c ()
+>          close c)
+>
+> echoServer espec lspec = ixdo
+>   clet lc = request lspec
+>   enter lc
+>   let loop = ixdo
+>         clet ec = accept espec
+>         offer ec
+>           (ixdo
+>            swap
+>            sel1 lc; send lc "echo server forking"
+>            zero lc
+>            dig (forkSession (recv ec >>>= send ec >>>= \_ -> close ec))
+>            loop)
+>           (ixdo
+>            dig $ ixdo
+>              sel1 lc; send lc "echo server exiting"
+>              zero lc
+>              sel2 lc; recv lc
+>              close lc
+>            send ec ()
+>            close ec)
+>   loop
+>
+> client delay say espec = ixdo
+>   clet c = request espec
+>   s <- io getLine
+>   case s of
+>     "q" -> ixdo
+>       sel2 c
+>       recv c
+>       close c
+>     _   -> ixdo
+>       forkSession $ ixdo
+>         sel1 c
+>         io (threadDelay $ round $ 1000000 * delay)
+>         send c s
+>         str <- recv c
+>         io (say str)
+>         close c
+>       client delay say espec
+>
+> go delay = do
+>   espec <- newRendezvous
+>   lspec <- newRendezvous
+>   (say, shutdown) <- newPrinter
+>   runSession $
+>     forkSession (accept lspec $ logger say) >>>= \_ ->
+>     forkSession (echoServer espec lspec) >>>= \_ ->
+>     client delay say espec
+>   shutdown
+
+}
diff --git a/Control/Concurrent/SimpleSession/Implicit.lhs b/Control/Concurrent/SimpleSession/Implicit.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/Implicit.lhs
@@ -0,0 +1,283 @@
+\section{Take 1: One Implicit Channel}
+\label{sec:implicit}
+
+\ignore{
+
+> {-# LANGUAGE TypeOperators,
+>              EmptyDataDecls,
+>              MultiParamTypeClasses,
+>              FunctionalDependencies,
+>              FlexibleInstances,
+>              FlexibleContexts,
+>              UndecidableInstances #-}
+>
+> module Control.Concurrent.SimpleSession.Implicit (
+>   module Control.Concurrent.SimpleSession.SessionTypes,
+>   module Control.Monad.Indexed,
+>   Session, Cap,
+>   io,
+>   send, recv, close, sel1, sel2, offer,
+>   enter, zero, suc, Pop(pop),
+>   Rendezvous, newRendezvous,
+>   accept, request
+> ) where
+> 
+> import Control.Concurrent.SimpleSession.TChan
+> import Control.Concurrent.SimpleSession.UChan
+> import Control.Monad.Indexed
+> import Control.Concurrent.SimpleSession.SessionTypes
+
+}
+
+Encoding protocols in Haskell is not enough.  We cannot merely provide
+channels parameterized by session types and call it a day.  For example,
+consider a hypothetical |send| operation:
+
+< send :: Channel (a :!: r) -> a -> IO (Channel r)
+
+While this |send| returns the correct channel for the rest of the
+session, it fails to prevent reuse of the |a :!: r| channel,
+which would violate the protocol.  One way to avoid this problem is to
+require that channels (or at least their sessions) be treated linearly.
+In this section, we show how this is done for
+processes having access to only one channel, which is left implicit in the
+environment; in the next section, we implement multiple
+concurrent channels.
+
+We assume a substrate of synchronous channels in both typed and
+untyped varieties:
+
+< writeTChan       :: TChan a -> a -> IO ()
+< readTChan        :: TChan a -> IO a
+<
+< unsafeWriteUChan :: UChan -> a -> IO ()
+< unsafeReadUChan  :: UChan -> IO a
+
+These channels have dynamic semantics similar to Concurrent ML's
+\citep{Reppy1991CML} synchronous channels.  While |TChan|s transmit
+only a single type, |UChan|s are indiscriminating about what
+they send and receive.  In our implementation, they use |unsafeCoerce#|,
+which can lead to undefined
+behavior if sent and received types differ.  We must somehow impose our
+own type discipline.
+
+We define an abstract type |Session s s' a|, which represents a computation that
+evolves a session from state |s| to state |s'| while producing a value of
+type |a|.  |Session|'s constructor is not
+exported to client code, so that clients of the library
+cannot arbitrarily modify the session state.
+|Session| is implemented as the composition of the IO monad with
+a reader monad carrying a untyped channel.
+
+> newtype Session s s' a =
+>   Session { unSession :: UChan -> IO a }
+
+The phantom parameters |s| and |s'| must track more information than
+just the current session.  We define a type constructor |Cap| to hold
+not only the current session |r|, but another type |e|, which represents
+a session type environment:
+
+> data Cap e r
+
+The type |Cap e r| represents the capability to run the protocol |r|.
+The session type environment |e| provides context for any
+free variables |Var v| in |r|; that is, |r| must be closed in |e|.
+We discuss |e| in more detail when we
+explain recursion, and the other operations merely thread it through.
+
+We can now give |send| a type and definition that will work:
+
+> send  :: a -> Session (Cap e (a :!: r)) (Cap e r) ()
+> send x = Session (\c -> unsafeWriteUChan c x)
+
+Given an |a|, |send| evolves the session from
+|a :!: r| to |r|.
+In its implementation, |unsafeWriteUChan|
+indiscriminately transmits values of any type over an untyped channel.
+Thus, if we fail to ensure that the receiving process expects a value of
+type |a|, things can go very wrong.  In \Section\ref{sec:theory}, we
+argue that this cannot happen.
+
+Predictably, |recv| requires the capability to receive an |a|, which it
+then produces:
+
+> recv  :: Session (Cap e (a :?: r)) (Cap e r) a
+> recv   = Session unsafeReadUChan
+
+We use |close| to discard an exhausted capability, replacing it
+with |()|.
+In this implementation, |close| is a run-time no-op.
+
+> close :: Session (Cap e Eps) () ()
+> close  = Session (\_ -> return ())
+
+\paragraph{Composing computations.}
+
+We also need a way to compose |Session| computations.  Composing a
+session from state $s_1$ to $s_2$ with a session from state $t_1$ to
+$t_2$ should be permitted only if $s_2 = t_1$.  This is precisely the
+situation that \emph{indexed monads} capture.
+
+%include IxMonad.lhs
+
+The |IxMonad| instance for |Session| is then straightforward.  It
+threads the implicit channel through and runs the underlying
+computations in the |IO| monad.
+
+> instance IxFunctor Session where
+>   imap f = undefined
+>
+> instance IxPointed Session where
+>   ireturn = undefined
+>
+> instance IxApplicative Session where
+>   iap = undefined
+>
+> instance IxMonad Session where
+>   ibind = undefined
+
+< instance IxMonad Session where
+<   ret a    = Session (\_ -> return a)
+<   m >>>= k = Session (\c -> do a <- unSession m c
+<                                unSession (k a) c)
+
+We use |io| to lift an arbitrary |IO| computation into |Session|:
+
+> io    :: IO a -> Session s s a
+> io m   = Session (\_ -> m)
+
+Because of |io|, this implementation is actually not linear but affine:
+an |IO| action may raise an exception and terminate the |Session|
+computation.  Provided that exceptions cannot be caught within a
+|Session|, this does not jeopardize safety in the sense that any
+messages received will still have the expected representation.  Some
+formulations of session types guarantee that a session, once initiated,
+will run to completion, but this seems unrealistic for real-world
+programs.  Handling exceptions from within a session remains an open
+problem.
+
+\paragraph{Alternation.}
+
+The session actions |sel1|, |sel2|, and |offer| implement alternation.
+Action |sel1| selects the left side of an ``internal choice'',
+thereby replacing a session |r :+: s| with the session |r|; |sel2|
+selects the right side.  On the other side of the channel, |offer| combines a
+|Session| computation for |r| with a computation for |s| into a
+computation that can handle |r :&: s|.  Dynamically, |sel1| sends |True|
+over the channel, whereas |sel2| sends |False|, and |offer| dispatches
+on the boolean value received.
+
+> sel1  :: Session (Cap e (r :+: s)) (Cap e r) ()
+> sel1   = Session (\c -> unsafeWriteUChan c True)
+> 
+> sel2  :: Session (Cap e (r :+: s)) (Cap e s) ()
+> sel2   = Session (\c -> unsafeWriteUChan c False)
+> 
+> offer :: Session (Cap e r) u a ->
+>          Session (Cap e s) u a ->
+>          Session (Cap e (r :&: s)) u a
+> offer (Session m1) (Session m2)
+>        = Session (\c -> do b <- unsafeReadUChan c
+>                            if b then m1 c else m2 c)
+
+\paragraph{Recursion.}
+
+Session actions |enter|, |zero|, and |suc| implement recursion.
+Consider the recursive session type
+
+< Request :!: Rec ((Response :?: Var Z) :&: Eps)
+
+from above.  After sending a |Request|, we need some way to enter the
+body of the |Rec|, and upon reaching |Var Z|, we need some way to repeat
+the body of the |Rec|.  We accomplish the former with |enter|, which
+strips the |Rec| constructor from |r| and pushes |r| onto the stack |e|:
+
+> enter :: Session (Cap e (Rec r)) (Cap (r, e) r) ()
+> enter  = Session (\_ -> return ())
+
+In |e|, we maintain a stack of session types for the body of each enclosing
+|Rec|, representing an environment that closes over |r|.  Upon
+encountering a variable occurence |Var |$n$, where $n$ is a Peano
+numeral, we restore the
+$n$th session type from the stack and return the stack to its former
+state, using $n$ expressed with |zero| and |suc|:
+
+> zero  :: Session (Cap (r, e) (Var Z))
+>                  (Cap (r, e) r) ()
+> zero   = Session (\_ -> return ())
+>
+> suc   :: Session (Cap (r, e) (Var (S v)))
+>                  (Cap e (Var v)) ()
+> suc    = Session (\_ -> return ())
+
+For example, if the current session is |Var (S (S Z))|, then the operation
+
+< suc >>> suc >>> zero
+
+pops two elements from the stack and
+replaces the current session with the body of the third enclosing |Rec|.
+
+It is worth remarking that this duplication of type and code to pop the
+stack is not strictly necessary.  If we explicitly
+write |suc >>> suc >>> zero|, Haskell's type checker can infer |S (S Z)|.  If,
+on the other hand, the type is already known, then a type class can do
+the work:\footnote{Note that the definition of the method |pop| is the
+same for both instances of |Pop|, which suggests that it could
+be provided as a default method.  This would introduce a subtle bug,
+however, as it would enable defining new instances of |Pop| with
+arbitrary effect.}
+
+> class Pop s s' | s -> s' where pop :: Session s s' ()
+> 
+> instance Pop (Cap (r, e) (Var Z)) (Cap (r, e) r)
+>   where pop = Session (\_ -> return ())
+>
+> instance Pop (Cap e (Var v)) (Cap e' r') =>
+>          Pop (Cap (r, e) (Var (S v))) (Cap e' r')
+>   where pop = Session (\_ -> return ())
+
+\paragraph{Putting it all together.}
+
+Finally, we need a way to connect and run sessions.
+
+A |Rendezvous| is a synchronization object that connects the types of
+two processes at compile time, and then enables their connection by a
+channel at run time.  The |Rendezvous| carries a phantom parameter
+indicating the protocol to be spoken on the shared implicit channel,
+and is represented by a
+homogeneous, typed channel on which the untyped channel for a particular
+session will later be exchanged.  Creating a |Rendezvous| is as simple
+as creating a new typed channel and wrapping it.
+
+> newtype Rendezvous r = Rendezvous (TChan UChan)
+> 
+> newRendezvous :: IO (Rendezvous r)
+> newRendezvous  = newTChan >>= return . Rendezvous
+
+\par
+To accept a connection request, we need a |Rendezvous| object,
+and a |Session| computation whose starting session type matches that of
+the |Rendezvous|.  The computation must deplete and close its channel.
+At run time, |accept| creates a new untyped channel on which
+the communication will take place and sends it over the |Rendezvous|
+channel.  It then runs the session computation on the new channel.
+
+> accept :: Rendezvous r ->
+>           Session (Cap () r) () a -> IO a
+> accept (Rendezvous c) (Session f) = do
+>   nc <- newUChan
+>   writeTChan c nc
+>   f nc
+
+\par
+To request a connection, the session type of the |Session| computation
+must be dual to that of the given |Rendezvous|.  At run time,
+|request| receives a new, untyped channel from |accept| over the
+|Rendezvous| channel and then runs the computation using the channel.
+
+> request :: Dual r r' => Rendezvous r ->
+>            Session (Cap () r') () a -> IO a
+> request (Rendezvous c) (Session f)
+>          = readTChan c >>= f
+
+%include ImplicitExample.lhs
diff --git a/Control/Concurrent/SimpleSession/Positional.lhs b/Control/Concurrent/SimpleSession/Positional.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/Positional.lhs
@@ -0,0 +1,236 @@
+\section{Take $n$: Multiple Channels}
+\label{sec:positional}
+
+\ignore{
+
+> {-# LANGUAGE TypeOperators,
+>              EmptyDataDecls,
+>              Rank2Types #-}
+>
+> module Control.Concurrent.SimpleSession.Positional (
+>   module Control.Concurrent.SimpleSession.SessionTypes,
+>   module Control.Monad.Indexed,
+>   Session, Cap, Channel,
+>   io,
+>   send, recv, close, sel1, sel2, offer,
+>   enter, zero, suc,
+>   dig, swap, forkSession,
+>   Rendezvous, newRendezvous,
+>   accept, request, runSession
+> ) where
+>
+> import Control.Concurrent (forkIO)
+>
+> import Control.Concurrent.SimpleSession.UChan
+> import Control.Concurrent.SimpleSession.TChan
+> import Control.Monad.Indexed
+> import Control.Concurrent.SimpleSession.SessionTypes
+>
+> newtype Rendezvous r = Rendezvous (TChan UChan)
+>
+> newRendezvous :: IO (Rendezvous r)
+> newRendezvous  = newTChan >>= return . Rendezvous
+> 
+> recv  :: Channel t -> Session (Cap t e (a :?: r), x) (Cap t e r, x) a
+> close :: Channel t -> Session (Cap t e Eps, x) x ()
+> sel1  :: Channel t -> Session (Cap t e (r :+: s), x) (Cap t e r, x) ()
+> sel2  :: Channel t -> Session (Cap t e (r :+: s), x) (Cap t e s, x) ()
+> offer :: Channel t -> Session (Cap t e r, x) u a -> Session (Cap t e s, x) u a -> Session (Cap t e (r:&:s), x) u a
+> enter :: Channel t -> Session (Cap t e (Rec r), x) (Cap t (r, e) r, x) ()
+> zero  :: Channel t -> Session (Cap t (r, e) (Var Z), x) (Cap t (r, e) r, x) ()
+> suc   :: Session (Cap t (r, e) (Var (S v)), x) (Cap t e (Var v), x) ()
+>
+> _cast = Session . unSession
+> recv (Channel c) = Session (unsafeReadUChan c)
+> sel1 c  = _cast (send c True)
+> sel2 c  = _cast (send c False)
+> offer c l r = _cast (recv c) >>>= \choice ->
+>               if choice
+>                 then _cast l
+>                 else _cast r
+> close _ = _cast (ireturn ())
+> enter _ = _cast (ireturn ())
+> zero  _ = _cast (ireturn ())
+> suc     = _cast (ireturn ())
+
+}
+
+Rather than limit ourselves to one implicit channel at a time, it might
+be more flexible to work with several channels at once.  To extend |Session| to
+handle multiple channels, our first step is to separate the channel
+itself from the capability to use it for a particular session:
+
+> newtype Channel t = Channel UChan
+> data Cap t e r
+
+The parameter |t| is a unique tag that ties a given channel to the
+capability to use it.  A |Channel t| is an actual value at run time,
+while the corresponding |Cap t e r| is relevant only during type-checking.
+We allow |Channel t| to be aliased freely because
+a channel is unusable without its capability, and we treat capabilities
+linearly.  As before, the capability also contains a session type
+environment |e| and a session type |r| that is closed in |e|.
+
+We now index |Session| by a \emph{stack} of capabilities, while
+underneath the hood, it is just the |IO| monad.  |Session| is no longer
+responsible for maintaining the run-time representation of channels, but
+instead it keeps track of the compile-time representation of
+capabilities.
+
+> newtype Session s s' a = Session { unSession :: IO a }
+>
+> instance IxFunctor Session where
+>   imap = undefined
+> instance IxPointed Session where
+>   ireturn = undefined
+> instance IxApplicative Session where
+>   iap = undefined
+> instance IxMonad Session where
+>   ibind = undefined
+>
+> io :: IO a -> Session s s a
+> io  = Session
+
+< instance IxMonad Session where
+<   ret      = Session . return
+<   m >>>= k = Session (unSession m >>= unSession . k)
+
+\par
+A |Session| computation now carries a stack of capability types, and
+communication operations manipulate only the top capability on the
+stack, leaving the rest of the stack unchanged.
+The |send| operation takes a channel
+as an argument rather than obtaining it implicitly, and the tag |t| on
+the channel must match the tag in the capability.
+
+> send :: Channel t -> a ->
+>         Session (Cap t e (a :!: r), x)
+>                 (Cap t e r, x) ()
+> send (Channel c) a = Session (unsafeWriteUChan c a)
+
+In the type above, |Cap t e (a :!: r)| is the capability on the top
+of the stack before the |send|, and |Cap t e r| is the capability
+after the |send|.  Type variable |x| represents the rest of the
+capability stack, which is unaffected by this operation.
+
+The implementations of the remaining operations are similarly unsurprising.
+Each differs from the previous section only in obtaining a channel
+explicitly from its argument rather than implicitly from the indexed
+monad.  Their types may be found in Figure~\ref{fig:operationtypes}.
+Note that |close| now has the effect of popping the capability for the
+closed channel from the top of the stack.
+
+\paragraph{Stack manipulation.}
+
+Channel operations act on the top of the capability stack.  Because the
+capability for the particular channel we wish to use may not be on the
+top of the stack, we may need to use other capabilities than the top
+one.  The |dig| combinator suffices to
+select any capability on the stack.  Given a |Session| computation that
+transforms a stack |x| to a stack |x'|, |dig| lifts it to a computation
+that transforms |(r, x)| to |(r, x')| for any |r|; thus, $n$
+applications of |dig| will select the $n$th capability on the stack.
+Note that |dig| has no run-time effect, but merely unwraps and rewraps 
+a |Session| to change the phantom type parameters.
+
+> dig  :: Session x x' a -> Session (r, x) (r, x') a
+> dig   = Session . unSession
+
+In combination with |swap|, we may generate any desired stack permutation.
+Since |swap| exchanges the top two capabilities on the stack, |dig| and
+|swap| may be combined to exchange any two adjacent capabilities.
+
+> swap :: Session (r, (s, x)) (s, (r, x)) ()
+> swap  = Session (return ())
+
+\par
+One reason we may want to rearrange the stack is to support |forkSession|,
+which runs a |Session| computation in a new thread, giving to it
+the entire \emph{visible} stack.  Thus, to partition the stack
+between the current thread and a new thread, we use |dig| and |swap|
+until all the capabilities for the new thread are below all the
+capabilities for the current thread.  Then we call |forkSession|
+under sufficiently many |dig|s so that it takes only the desired capabilities
+with it.
+
+> forkSession :: Session x () () -> Session x () ()
+> forkSession (Session c)
+>              = Session (forkIO c >> return ())
+
+For example, to keep the top two capabilities on the stack
+for the current thread and assign the rest to a new thread |m|, we
+would use |dig (dig (forkSession m))|.
+
+\paragraph{Making a connection.}
+
+In the implicit channel case, each |accept| or |request| starts
+a single |Session| computation that runs to completion.
+Because we now have multiple channels, we may need
+to use |accept| and |request| to start new communication
+sessions during an ongoing |Session| computation.
+Given a |Rendezvous| and a continuation
+of matching session type, |accept|
+creates a new channel/capability pair.  It calls the continuation with
+the channel, pushing the corresponding capability on the top of its
+stack.  The \mbox{rank-2} type in |accept| ensures that the new |Channel t|
+and |Cap t () r| cannot be used with any other capability or channel.
+In \Section\ref{sec:discussion} we discuss an alternate formulation that
+does not require higher-rank polymorphism, but this version here seems
+more elegant.
+
+> accept :: Rendezvous r ->
+>           (forall t. Channel t ->
+>             Session (Cap t () r, x) y a) ->
+>           Session x y a
+> accept (Rendezvous c) f = Session (do
+>   nc <- newUChan
+>   writeTChan c nc
+>   unSession (f (Channel nc)))
+
+The |request| function behaves similarly, but as before, it
+uses the dual session type.
+
+> request :: Dual r r' =>
+>            Rendezvous r ->
+>            (forall t. Channel t ->
+>              Session (Cap t () r', x) y a) ->
+>            Session x y a
+> request (Rendezvous c) f = Session (do
+>   nc <- readTChan c
+>   unSession (f (Channel nc)))
+
+We may start a |Session| computation from within the IO monad.  The type
+of |runSession| ensures that the computation both begins and ends with
+no capabilities in the stack.
+
+> runSession :: Session () () a -> IO a
+> runSession  = unSession
+
+\paragraph{Sending capabilities.}
+
+Now that we have multiple channels, we might wonder whether we can send
+capabilities themselves over a channel.  Certainly, but since we do
+not allow direct access to capabilities, this requires a specialized
+pair of functions.
+
+> send_cap :: Channel t ->
+>             Session (Cap t e (Cap t' e' r' :!: r),
+>                      (Cap t' e' r', x))
+>                     (Cap t e r, x) ()
+> send_cap (Channel c)
+>           = Session (unsafeWriteUChan c ())
+>
+> recv_cap :: Channel t ->
+>             Session (Cap t e (Cap t' e' r' :?: r), x)
+>                     (Cap t e r, (Cap t' e' r', x)) ()
+> recv_cap (Channel c) = Session (unsafeReadUChan c)
+
+Observe that because capabilities have no run-time existence, the actual
+value sent over the channel is |()|.  This provides synchronization so
+that the receiving process does not perform channel operations
+with the capability before the sending process has finished its part.
+The phantom type parameters to |Session| change to reflect the
+transmission of the capability.
+
+%include PositionalExample.lhs
+
diff --git a/Control/Concurrent/SimpleSession/SessionTypes.lhs b/Control/Concurrent/SimpleSession/SessionTypes.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/SessionTypes.lhs
@@ -0,0 +1,116 @@
+\section{Session Types in Haskell}
+\label{sec:session}
+
+\ignore{
+
+> {-# LANGUAGE TypeOperators,
+>              EmptyDataDecls,
+>              MultiParamTypeClasses,
+>              FunctionalDependencies,
+>              UndecidableInstances #-}
+> module Control.Concurrent.SimpleSession.SessionTypes (
+>   Z, S,
+>   Eps, (:!:), (:?:), (:+:), (:&:), Rec, Var,
+>   Dual
+> ) where
+> 
+> infixr 3 :!:, :?:
+> infix 2 :+:, :&:
+>
+> data Z
+> data S n
+
+}
+
+The central idea of session types \citep{r:gay99} is to parameterize a
+channel with some type that represents a protocol, which the type system
+then enforces.  In Haskell, we may encode a protocol using ordinary
+datatypes:
+
+> data (:!:) a r
+> data (:?:) a r
+> data Eps
+
+These datatypes require no constructors because they will have no
+run-time representation.
+
+If |a| is any type, and |r| is a protocol, then
+we interpret |a :!: r| as the protocol, ``first send an |a|, and
+then continue with |r|.''  Similarly, we interpret |a :?: r| as
+the protocol, ``receive
+an |a|, and then continue with |r|.''  The type |Eps| represents the empty
+protocol of a depleted channel that is not yet closed.
+
+For example, the type |Int :!: Bool :?: Eps| represents the protocol,
+``send an |Int|, receive a |Bool|, and close the
+channel.''\thinspace\footnote{The type constructors |(:!:)| and
+|(:?:)| are declared right associative and with higher precedence than
+|(:+:)| and |(:&:)|.}
+
+If the process on one end of a channel speaks a particular protocol,
+its correspondant at the other end of the channel must be prepared to
+understand it.  For example, if one process speaks |Int :!: Bool :?: Eps|,
+the other process must implement the dual protocol
+|Int :?: Bool :!: Eps|.  We encode the duality relation using a type
+class with multiple parameters and functional dependencies
+\citep{Jones1997Type,Jones2000Type}.
+
+> class Dual r s | r -> s, s -> r
+
+The functional dependencies indicate that duality
+is bijective, which helps Haskell to infer
+protocols and enables a form of subtyping.  Sending and receiving are
+dual:  if |r| is dual to |s|, then |a :!: r| is dual to |a :?: s|.  The
+empty session is dual to itself.
+
+> instance Dual r s => Dual (a :!: r) (a :?: s)
+> instance Dual r s => Dual (a :?: r) (a :!: s)
+> instance Dual Eps Eps
+
+\par
+Our session types also represent alternation and recursion.  If |r|
+and |s| are protocols, then |r :+: s| represents an active choice
+between following |r| or |s|.  The type |r :&: s| represents
+an offer to follow either |r| or |s|, as chosen by the other
+process.
+
+> data (:+:) r s
+> data (:&:) r s
+
+The two alternation operators are dual:
+
+> instance (Dual r1 s1, Dual r2 s2) =>
+>                    Dual (r1 :+: r2) (s1 :&: s2)
+> instance (Dual r1 s1, Dual r2 s2) =>
+>                    Dual (r1 :&: r2) (s1 :+: s2)
+
+\par
+Recursion turns out to be slightly more difficult.  It is tempting to
+use a fixed-point combinator, but this would require constructing a
+type of kind $\star \to \star$ for any desired loop body, which
+is not generally possible.  We need
+some other way for a recursive type to refer to itself, so we represent
+this binding using de~Bruijn indices.
+
+> data Rec r
+> data Var v
+> 
+> instance Dual r s => Dual (Rec r) (Rec s)
+> instance Dual (Var v) (Var v)
+
+The type |Rec r| adds a binding for |r| inside |r|; that is, it
+implicitly defines a variable bound to the whole of |r| that can be used
+\emph{within} |r|.  We use |Var v| to refer to the variable bound by
+the |v|th |Rec|, counting outward, where |v| is a Peano numeral
+written with type constructors |Z| and |S|
+(\emph{e.g.,} |Z| or |S (S Z)|).  For example, the protocol
+
+< Request :!: Rec (Response :?: (Var Z :&: Eps))
+
+says to send a request and then be prepared to receive one or more
+responses.  By contrast, a process implementing the protocol
+
+< Request :!: Rec ((Response :?: Var Z) :&: Eps)
+
+must send a request and be prepared to accept any number of responses.
+
diff --git a/Control/Concurrent/SimpleSession/TChan.lhs b/Control/Concurrent/SimpleSession/TChan.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/TChan.lhs
@@ -0,0 +1,38 @@
+
+\ignore{
+
+> module Control.Concurrent.SimpleSession.TChan (
+>   TChan, newTChan, writeTChan, readTChan
+> ) where
+> 
+> import Control.Concurrent.MVar
+
+}
+
+An |TChan a| is a monomorphic, synchronous channel that can transmit
+values of type |a|:
+
+> newtype TChan a
+
+\ignore{
+
+>   = CC (MVar (MVar a))
+> 
+> newTChan = newEmptyMVar >>= return . CC
+> 
+> writeTChan (CC cc) v = do
+>   mv <- takeMVar cc
+>   putMVar mv v
+> 
+> readTChan (CC cc) = do
+>   mv <- newEmptyMVar
+>   putMVar cc mv
+>   takeMVar mv
+
+}
+
+|TChan| has three operations:
+
+> newTChan   :: IO (TChan a)
+> writeTChan :: TChan a -> a -> IO ()
+> readTChan  :: TChan a -> IO a
diff --git a/Control/Concurrent/SimpleSession/UChan.lhs b/Control/Concurrent/SimpleSession/UChan.lhs
new file mode 100644
--- /dev/null
+++ b/Control/Concurrent/SimpleSession/UChan.lhs
@@ -0,0 +1,38 @@
+\ignore{
+
+> {-# LANGUAGE MagicHash #-}
+> module Control.Concurrent.SimpleSession.UChan (
+>   UChan, newUChan, unsafeReadUChan, unsafeWriteUChan
+> ) where
+> 
+> import GHC.Exts
+> import Control.Concurrent.SimpleSession.TChan
+
+}
+
+On top of |TChan| we have implemented |UChan|, an untyped,
+synchronous channel:
+
+> newtype UChan
+
+\ignore{
+
+>   = CC (TChan Int)
+> 
+> unUChan (CC c) = unsafeCoerce# c
+> 
+> newUChan         = newTChan >>= return . CC
+> unsafeWriteUChan = writeTChan . unUChan
+> unsafeReadUChan  = readTChan . unUChan
+
+}
+
+Like |TChan|, |UChan| has three operations:
+
+> newUChan         :: IO UChan
+> unsafeWriteUChan :: UChan -> a -> IO ()
+> unsafeReadUChan  :: UChan -> IO a
+
+Note that since |UChan| is willing to send or receive a value of \emph{any}
+type, it's unsafe unless we find some other way to restrict it.
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+Redistributions of source code must retain the above copyright
+notice, this list of conditions and the following disclaimer.
+
+Redistributions in binary form must reproduce the above copyright
+notice, this list of conditions and the following disclaimer in the
+documentation and/or other materials provided with the distribution.
+
+Neither the name of the Northeastern University; nor the names of its
+contributors may be used to endorse or promote products derived from
+this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+#!/usr/bin/env runhaskell
+
+import Distribution.Simple
+main = defaultMain
diff --git a/TODO b/TODO
new file mode 100644
--- /dev/null
+++ b/TODO
@@ -0,0 +1,2 @@
+Haddock.
+Name-based capability access.
diff --git a/simple-sessions.cabal b/simple-sessions.cabal
new file mode 100644
--- /dev/null
+++ b/simple-sessions.cabal
@@ -0,0 +1,32 @@
+Name:           simple-sessions
+Version:        0.1
+Cabal-Version:  >= 1.2
+License:        BSD3
+License-File:   LICENSE
+Stability:      experimental
+Author:         Jesse A. Tov <tov@ccs.neu.edu>
+Maintainer:     tov@ccs.neu.edu
+Homepage:       http://www.ccs.neu.edu/~tov/session-types
+Category:       Control
+Synopsis:       A simple implementation of session types
+Build-type:     Simple
+Description:
+        This library is based on the session types implementation
+        from "Haskell Session Types with Almost No Class," from the 2008
+        Haskell Symposium.  For a full-featured session types library,
+        see the sessions package.
+
+Extra-Source-Files:
+    TODO
+    Control/Concurrent/SimpleSession/Examples/Implicit.lhs
+    Control/Concurrent/SimpleSession/Examples/Positional.lhs
+
+Library
+  Build-Depends:        base, category-extras
+  Exposed-modules:
+    Control.Concurrent.SimpleSession.SessionTypes,
+    Control.Concurrent.SimpleSession.Implicit,
+    Control.Concurrent.SimpleSession.Positional
+  Other-modules:
+    Control.Concurrent.SimpleSession.TChan,
+    Control.Concurrent.SimpleSession.UChan