diff --git a/Makefile b/Makefile
index af9de9a..43d336a 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 include .rc.make
 
-subdirs := src/ src/Examples/ unused/ src/Selective/ src/Selective/Examples/
+subdirs := src/ src/Examples/ src/Libraries/ src/Selective/ src/Selective/Libraries/ src/Selective/Examples/
 agda-objects := $(wildcard $(subdirs:%=%*.agdai))
 executables := $(wildcard $(subdirs:%=%*.exe))
 malonzo := $(wildcard $(subdirs:%=%MAlonzo/))
diff --git a/latex.make b/latex.make
index c2fd338..c66033a 100644
--- a/latex.make
+++ b/latex.make
@@ -1,6 +1,6 @@
 include .rc.make
 
-subdirs := src/ src/Examples/ src/Selective/ src/Selective/Examples/
+subdirs := src/ src/Examples/ src/Libraries/ src/Selective/ src/Selective/Libraries/ src/Selective/Examples/
 sources := $(wildcard $(subdirs:%=%*.lagda.tex))
 renamed := $(sources:%.lagda.tex=%.tex)
 moved   := $(renamed:src/%=$(LATEX-OUTPUT-DIR)%)
diff --git a/src/Examples/Main-template.agda b/src/Examples/Main-template.agda
index dd70fb0..e0d3816 100644
--- a/src/Examples/Main-template.agda
+++ b/src/Examples/Main-template.agda
@@ -1,8 +1,8 @@
 module Examples.Main-generated where
 import Examples.PingPong as PingPong
 import Examples.InfiniteBind as InfiniteBind
-import Examples.SelectiveReceive as SelectiveReceive
-import Examples.Call as Call
+import Examples.TestSelectiveReceive as SelectiveReceive
+import Examples.TestCall as Call
 open import Runtime
 open import SimulationEnvironment
 open import ActorMonad
diff --git a/src/Examples/TestCall.agda b/src/Examples/TestCall.agda
new file mode 100644
index 0000000..72ca908
--- /dev/null
+++ b/src/Examples/TestCall.agda
@@ -0,0 +1,46 @@
+module Examples.TestCall where
+
+open import Prelude
+open import Libraries.SelectiveReceive
+open import Libraries.Call
+
+open SelRec
+
+AddReplyMessage : MessageType
+AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
+
+AddReply : InboxShape
+AddReply = [ AddReplyMessage ]ˡ
+
+AddMessage : MessageType
+AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
+
+Calculator : InboxShape
+Calculator = [ AddMessage ]ˡ
+
+calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
+calculatorActor = loop
+  where
+    loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → [])
+    loop .force = receive ∞>>= λ {
+      (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
+        Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
+        strengthen []
+        loop
+      ; (Msg (S ()) _) }
+
+TestBox : InboxShape
+TestBox = AddReply
+
+calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+calltestActor .force = spawn∞ calculatorActor ∞>> do
+    x ← call [] Z Z 0
+         ((lift 10) ∷ [ lift 32 ]ᵃ)
+         ⊆-refl Z
+    strengthen []
+    return-result x
+  where
+    return-result : SelRec TestBox (call-select 0 ⊆-refl Z) →
+                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
+    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
diff --git a/src/Examples/TestSelectiveReceive.agda b/src/Examples/TestSelectiveReceive.agda
new file mode 100644
index 0000000..aa17046
--- /dev/null
+++ b/src/Examples/TestSelectiveReceive.agda
@@ -0,0 +1,32 @@
+module Examples.TestSelectiveReceive where
+
+open import Prelude
+open import Libraries.SelectiveReceive
+
+open SelRec
+
+BoolMessage = [ ValueType Bool ]ˡ
+SelectiveTestBox : InboxShape
+SelectiveTestBox = [ BoolMessage ]ˡ
+
+testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → [])
+testActor = selective-receive [] only-true ∞>>= after-receive
+  where
+    only-true : Message SelectiveTestBox → Bool
+    only-true (Msg Z (b ∷ [])) = b
+    only-true (Msg (S ()) x₁)
+    after-receive : ∀ {i}
+                    (x : SelRec SelectiveTestBox only-true) →
+                    ∞ActorM i SelectiveTestBox (Lift Bool)
+                      (add-references [] (msg x) ++ waiting-refs (waiting x))
+                      (λ _ → [])
+    after-receive record { msg = (Msg Z (.true ∷ [])) ; msg-ok = refl } =
+      strengthen [] >>
+      return true
+    after-receive record { msg = (Msg (S ()) _) }
+
+spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
+spawner = begin do
+  spawn testActor
+  Z ![t: Z ] [ lift true ]ᵃ
+  strengthen []
diff --git a/src/Examples/Call.lagda.tex b/src/Libraries/Call.lagda.tex
similarity index 62%
rename from src/Examples/Call.lagda.tex
rename to src/Libraries/Call.lagda.tex
index b6d4abf..40939c8 100644
--- a/src/Examples/Call.lagda.tex
+++ b/src/Libraries/Call.lagda.tex
@@ -1,9 +1,9 @@
 \begin{code}
-module Examples.Call where
+module Libraries.Call where
 
 open import ActorMonad public
 open import Prelude
-open import Examples.SelectiveReceive using (
+open import Libraries.SelectiveReceive using (
             selective-receive ; SelRec ; waiting-refs
             ; add-references++)
 open SelRec
@@ -59,44 +59,4 @@
       px ∷ translate-fields ps
     translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ ps) =
       ([ (S (∈-inc Γ (waiting-refs q) _ p)) ]>: v) ∷ (translate-fields ps)
-
-AddReplyMessage : MessageType
-AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
-
-AddReply : InboxShape
-AddReply = [ AddReplyMessage ]ˡ
-
-AddMessage : MessageType
-AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
-
-Calculator : InboxShape
-Calculator = [ AddMessage ]ˡ
-
-calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
-calculatorActor = loop
-  where
-    loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → [])
-    loop .force = receive ∞>>= λ {
-      (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
-        Z ![t: Z ] ((lift tag) ∷ [ lift (n + m) ]ᵃ )
-        strengthen []
-        loop
-      ; (Msg (S ()) _) }
-
-TestBox : InboxShape
-TestBox = AddReply
-
-calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calltestActor .force = spawn∞ calculatorActor ∞>> do
-    x ← call [] Z Z 0
-         ((lift 10) ∷ [ lift 32 ]ᵃ)
-         ⊆-refl Z
-    strengthen []
-    return-result x
-  where
-    return-result : SelRec TestBox (call-select 0 ⊆-refl Z) →
-                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
-    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
-
 \end{code}
diff --git a/src/Examples/SelectiveReceive.lagda.tex b/src/Libraries/SelectiveReceive.lagda.tex
similarity index 88%
rename from src/Examples/SelectiveReceive.lagda.tex
rename to src/Libraries/SelectiveReceive.lagda.tex
index 4f0db24..41aeaea 100644
--- a/src/Examples/SelectiveReceive.lagda.tex
+++ b/src/Libraries/SelectiveReceive.lagda.tex
@@ -1,6 +1,6 @@
 \begin{code}
 
-module Examples.SelectiveReceive where
+module Libraries.SelectiveReceive where
 
 open import ActorMonad public
 open import Prelude
@@ -230,32 +230,3 @@
             ret-v : SelRec IS f
             ret-v = record { msg = x ; msg-ok = p ; waiting = q }
 \end{code}
-
-\begin{code}
-
-BoolMessage = [ ValueType Bool ]ˡ
-SelectiveTestBox : InboxShape
-SelectiveTestBox = [ BoolMessage ]ˡ
-
-testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → [])
-testActor = selective-receive [] only-true ∞>>= after-receive
-  where
-    only-true : Message SelectiveTestBox → Bool
-    only-true (Msg Z (b ∷ [])) = b
-    only-true (Msg (S ()) x₁)
-    after-receive : ∀ {i}
-                    (x : SelRec SelectiveTestBox only-true) →
-                    ∞ActorM i SelectiveTestBox (Lift Bool)
-                      (add-references [] (msg x) ++ waiting-refs (waiting x))
-                      (λ _ → [])
-    after-receive record { msg = (Msg Z (.true ∷ [])) ; msg-ok = refl } =
-      strengthen [] >>
-      return true
-    after-receive record { msg = (Msg (S ()) _) }
-
-spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
-spawner = begin do
-  spawn testActor
-  Z ![t: Z ] [ lift true ]ᵃ
-  strengthen []
-\end{code}
diff --git a/src/Selective/Examples/ActiveObjects.agda b/src/Selective/Examples/ActiveObjects.agda
deleted file mode 100644
index d32e211..0000000
--- a/src/Selective/Examples/ActiveObjects.agda
+++ /dev/null
@@ -1,168 +0,0 @@
-module Selective.Examples.ActiveObjects where
-
-open import Selective.ActorMonad
-open import Selective.Examples.Channel
-open import Selective.Examples.Call2
-open import Prelude
-open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax)
-
-open ChannelType
-open ChannelInitiation
-
-
-active-request-type : ChannelInitiation → InboxShape
-active-request-type record { request = .[] ; response = response ; request-tagged = [] } = []
-active-request-type record { request = .(_ ∷ _) ; response = response ; request-tagged = (px ∷ pxs) } =
-  let rec = active-request-type (record { request = _ ; response = response ; request-tagged = pxs })
-  in extra-fields-shape px ∷ rec
-
-state-vars : ∀ {ci} {st : Set₁} → (st → TypingContext) → Message ci → InboxShape → st → TypingContext
-state-vars f input caller state = caller ∷ add-references (f state) input
-
-
-active-reply-needed-fields : ∀ mt → IsChannelMessage mt → MessageType
-active-reply-needed-fields _ (HasTag MT) = MT
-
-active-reply-type : ChannelType → InboxShape
-active-reply-type record { channel-shape = [] } = []
-active-reply-type record { channel-shape = (x ∷ xs) ; all-tagged = (px ∷ pxs) } =
-  let rec = active-reply-type (record { channel-shape = xs ; all-tagged = pxs })
-  in active-reply-needed-fields x px ∷ rec
-
-record ActiveReply (ci : ChannelInitiation) (state-type : Set₁) (var-f : state-type → TypingContext) (input : Message (active-request-type ci)) (caller : InboxShape) : Set₁ where
-  field
-    new-state : state-type
-    reply : SendMessage (active-reply-type (ci .response)) (state-vars var-f input caller new-state)
-
-reply-vars : ∀ {st ci var-f input} → (st → TypingContext) → Message (active-request-type ci) → (caller : InboxShape) → ActiveReply ci st var-f input caller → TypingContext
-reply-vars f input caller ar = state-vars f input caller (ActiveReply.new-state ar)
-
-active-method : InboxShape → (state-type : Set₁) → (state-type → TypingContext) → ChannelInitiation → Set₂
-active-method IS st var-f ci =
-  let input-type = Message (active-request-type ci)
-  in {i : Size} →
-     {caller : InboxShape} →
-     (input : input-type) →
-     (state : st) →
-     ∞ActorM i IS
-       (ActiveReply ci st var-f input caller)
-       (caller ∷ add-references (var-f state) input)
-       (reply-vars var-f input caller)
-
-active-inbox-shape : List ChannelInitiation → InboxShape
-active-inbox-shape [] = []
-active-inbox-shape (x ∷ lci) =
-  let rec = active-inbox-shape lci
-  in x .request ++ rec
-
-record ActiveObject : Set₂ where
-  field
-    state-type : Set₁
-    vars : state-type → TypingContext
-    methods : List ChannelInitiation
-    handlers : All (active-method (active-inbox-shape methods) state-type vars) methods
-
-open ActiveObject
-
-active-caller : (methods : List ChannelInitiation) →
-                Message (active-inbox-shape methods) →
-                InboxShape
-active-caller methods (Msg x f) = active-caller' methods x
-  where
-    active-caller' : {MT : MessageType} →
-                     (methods : List ChannelInitiation) →
-                     MT ∈ active-inbox-shape methods →
-                     InboxShape
-    active-caller' [] ()
-    active-caller' (record { request = [] } ∷ methods) p = active-caller' methods p
-    active-caller' (record { request = x ∷ _ ; response = response } ∷ _) Z = response .channel-shape
-    active-caller' (record { request = _ ∷ xs ; response = response ; request-tagged = _ ∷ pxs } ∷ methods) (S p) =
-      active-caller' (record { request = xs ; response = response ; request-tagged = pxs } ∷ methods) p
-
-forget-message : ∀ {i Γ} →
-                 {IS IS' : InboxShape} →
-                 (m : Message IS) →
-                 ∞ActorM i IS' ⊤₁ (add-references Γ m) (λ _ → Γ)
-forget-message (Msg x x₁) = strengthen (⊆++-l-refl _ _)
-
-data InEither {a} {A : Set a} (v : A) (xs ys : List A) : Set a where
-  Left : (v ∈ xs) → InEither v xs ys
-  Right : (v ∈ ys) → InEither v xs ys
-
-∈++ : ∀ {a} {A : Set a} {v : A} → (xs ys : List A) → (v ∈ (xs ++ ys)) → InEither v xs ys
-∈++ [] ys p = Right p
-∈++ (x ∷ xs) ys Z = Left Z
-∈++ (x ∷ xs) ys (S p) with (∈++ xs ys p)
-... | Left q = Left (S q)
-... | Right q = Right q
-
-invoke-active-method : {i : Size} →
-                       (ac : ActiveObject) →
-                       (input : Message (active-inbox-shape (ac .methods))) →
-                       (state : ac .state-type) →
-                       ∞ActorM i (active-inbox-shape (ac .methods))
-                         (ac .state-type) (add-references (ac .vars state) input) (λ x → add-references (ac .vars x) input)
-invoke-active-method ac (Msg x f) state = invoke f (ac .methods) (ac .handlers) x
-  where
-    translate-invoke-pointer : {ci : ChannelInitiation} →
-                               {MT : MessageType} →
-                               (ValueType UniqueTag ∷ ReferenceType (ci .response .channel-shape) ∷ MT) ∈ ci .request →
-                               MT ∈ active-request-type ci
-    translate-invoke-pointer {record { request-tagged = HasTag+Ref MT ∷ _ }} Z = Z
-    translate-invoke-pointer {record { response = response ; request-tagged = _ ∷ rt }} (S p) =
-      let rec = translate-invoke-pointer {record { request = _ ; response = response ; request-tagged = rt }} p
-      in S rec
-    translate-send-pointer : ∀ {ct MT} →
-                               MT ∈ active-reply-type ct →
-                               (TagField ∷ MT) ∈ ct .channel-shape
-    translate-send-pointer {record { channel-shape = [] }} ()
-    translate-send-pointer {record { all-tagged = HasTag MT ∷ _ }} Z = Z
-    translate-send-pointer {record { channel-shape = x ∷ xs ; all-tagged = px ∷ pxs }} (S p) = S (translate-send-pointer p)
-    invoke' : {i : Size} {MT : MessageType} →
-              All receive-field-content MT →
-              (ci : ChannelInitiation) →
-              active-method (active-inbox-shape (ac .methods)) (ac .state-type) (ac .vars) ci →
-              MT ∈ (ci .request) →
-              IsRequestMessage (ci .response .channel-shape) MT →
-              ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) (extract-references MT ++ ac .vars state) (λ st → extract-references MT ++ ac .vars st)
-    invoke' (tag ∷ _ ∷ f) ci handler p (HasTag+Ref MT) =
-      let
-        active-message : Message (active-request-type ci)
-        active-message = Msg (translate-invoke-pointer p) f
-      in do
-        record { new-state = new-state ; reply = SendM which fields } ← handler active-message state
-        send Z (SendM (translate-send-pointer which) (lift tag ∷ fields))
-        return₁ new-state
-    invoke : {i : Size} {MT : MessageType} →
-             All receive-field-content MT →
-             (cis : List ChannelInitiation) →
-             All (active-method (active-inbox-shape (ac .methods)) (ac .state-type) (ac .vars)) cis →
-             MT ∈ active-inbox-shape cis →
-             ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) (add-references-static (ac .vars state) MT) (λ st → add-references-static (ac .vars st) MT)
-    invoke _ _ [] ()
-    invoke f (ci ∷ _) (_ ∷ _) x with (∈++ (ci .request) _ x)
-    invoke f (ci ∷ _) (handler ∷ _) x | Left q =
-      let irm = lookup-all q (ci .request-tagged)
-      in invoke' f ci handler q irm
-    invoke f (_ ∷ cis) (_ ∷ handlers) x | Right q = invoke f cis handlers q
-
-handle-active-method : {i : Size} →
-                       (ac : ActiveObject) →
-                       (input : Message (active-inbox-shape (ac .methods))) →
-                       (state : ac .state-type) →
-                       ∞ActorM i (active-inbox-shape (ac .methods))
-                         (ac .state-type) (add-references (ac .vars state) input) (ac .vars)
-handle-active-method ac input state =
-  do
-    state' ← (invoke-active-method ac input state)
-    forget-message input
-    return₁ state'
-
-run-active-object : {i : Size} →
-                    (ac : ActiveObject) →
-                    (state : ac .state-type) →
-                    ∞ActorM i (active-inbox-shape (ac .methods)) (ac .state-type) ((ac .vars) state) (ac .vars)
-run-active-object ac state .force =
-  receive ∞>>= λ m →
-  handle-active-method ac m state >>= λ state' →
-  run-active-object ac state'
diff --git a/src/Selective/Examples/Bookstore.agda b/src/Selective/Examples/Bookstore.agda
index 842f543..ee6c0ff 100644
--- a/src/Selective/Examples/Bookstore.agda
+++ b/src/Selective/Examples/Bookstore.agda
@@ -1,7 +1,7 @@
 module Selective.Examples.Bookstore where
 
 open import Selective.ActorMonad
-open import Selective.Examples.Call using (UniqueTag ; call)
+open import Selective.Libraries.Call using (UniqueTag ; call)
 open import Prelude
 
 open import Data.Nat
diff --git a/src/Selective/Examples/Chat.agda b/src/Selective/Examples/Chat.agda
index c5ce5c9..f5c7663 100644
--- a/src/Selective/Examples/Chat.agda
+++ b/src/Selective/Examples/Chat.agda
@@ -1,7 +1,7 @@
 module Selective.Examples.Chat where
 
 open import Selective.ActorMonad
-open import Selective.Examples.Call using (UniqueTag ; call)
+open import Selective.Libraries.Call
 open import Prelude
   hiding (Maybe)
 open import Data.Maybe as Maybe
diff --git a/src/Selective/Examples/ChatAO.agda b/src/Selective/Examples/ChatAO.agda
new file mode 100644
index 0000000..cbf599b
--- /dev/null
+++ b/src/Selective/Examples/ChatAO.agda
@@ -0,0 +1,682 @@
+module Selective.Examples.ChatAO where
+
+open import Selective.ActorMonad
+open import Selective.Libraries.Channel
+open import Selective.Libraries.Call2
+open import Selective.Libraries.ActiveObjects
+open import Prelude
+  hiding (Maybe)
+open import Data.Maybe as Maybe
+  hiding (map)
+
+open import Data.List.Properties
+open import Category.Monad
+
+open import Debug
+open import Data.Nat.Show using (show)
+
+RoomName = ℕ
+ClientName = ℕ
+
+Room-to-Client : InboxShape
+
+record Client : Set where
+  field
+    name : ClientName
+    channel : UniqueTag
+
+ClientList : Set
+ClientList = List Client
+
+record RoomState : Set₁ where
+  field
+    clients : ClientList
+
+cl-to-context : ClientList → TypingContext
+cl-to-context = map λ _ → Room-to-Client
+
+rs-to-context : RoomState → TypingContext
+rs-to-context rs = let open RoomState
+  in cl-to-context (rs .clients)
+
+record ChatMessageContent : Set where
+  constructor chat-from_message:_
+  field
+    sender : ClientName
+    message : String
+
+SendChatMessage : MessageType
+SendChatMessage = [ ValueType ChatMessageContent ]ˡ
+
+
+ReceiveChatMessage : MessageType
+ReceiveChatMessage = ValueType UniqueTag ∷ [ ValueType ChatMessageContent ]ˡ
+
+chat-message-header : ActiveMethod
+chat-message-header = VoidMethod [ SendChatMessage ]ˡ
+
+Room-to-Client = [ ReceiveChatMessage ]ˡ
+
+AddToRoom : MessageType
+AddToRoom = ValueType UniqueTag ∷ ValueType ClientName ∷ [ ReferenceType Room-to-Client ]ˡ
+
+add-to-room-header : ActiveMethod
+add-to-room-header = VoidMethod [ AddToRoom ]ˡ
+
+LeaveRoom : MessageType
+LeaveRoom = [ ValueType ClientName ]ˡ
+
+leave-room-header : ActiveMethod
+leave-room-header = VoidMethod [ LeaveRoom ]ˡ
+
+room-methods : List ActiveMethod
+room-methods = chat-message-header ∷ leave-room-header ∷ [ add-to-room-header ]ˡ
+
+room-inbox = methods-shape room-methods
+
+add-to-room : (active-method room-inbox RoomState rs-to-context add-to-room-header)
+add-to-room _ (Msg Z (tag ∷ client-name ∷ _ ∷ [])) state = do
+  let
+    open RoomState
+    state' = record { clients = record { name = client-name ; channel = tag } ∷ state .clients }
+  strengthen (Z ∷ ⊆-refl)
+  return₁ state'
+add-to-room _ (Msg (S ()) _)
+
+record RoomLeave (rs : ClientList) (name : ClientName) : Set₁ where
+  field
+    filtered : ClientList
+    subs : (cl-to-context filtered) ⊆ (cl-to-context rs)
+
+leave-room : (active-method room-inbox RoomState rs-to-context leave-room-header)
+leave-room _ (Msg Z (client-name ∷ [])) state = do
+    let
+      open RoomState
+      open RoomLeave
+      rl = remove-first-client (state .clients) client-name
+      state' = record { clients = rl .filtered }
+    debug ("client#" || show client-name || " left the room") (strengthen (rl .subs))
+    return₁ state'
+  where
+    remove-first-client : (cl : ClientList) → (name : ClientName) → RoomLeave cl name
+    remove-first-client [] name = record { filtered = [] ; subs = [] }
+    remove-first-client (x ∷ cl) name with ((Client.name x) ≟ name)
+    ... | (yes _) = record { filtered = cl ; subs = ⊆-suc ⊆-refl }
+    ... | (no _) =
+      let
+        rec = remove-first-client cl name
+        open RoomLeave
+      in record { filtered = x ∷ rec .filtered ; subs = Z ∷ ⊆-suc (rec .subs) }
+leave-room _ (Msg (S ()) _) _
+
+chat-message : (active-method room-inbox RoomState rs-to-context chat-message-header)
+chat-message _ (Msg Z ((chat-from sender message: message) ∷ [])) state = do
+    let
+      open RoomState
+      debug-msg = ("room sending " || show (pred (length (state .clients))) ||  " messages from " || show sender || ": " || message)
+    debug debug-msg (send-to-others (state .clients) sender message)
+    return₁ state
+  where
+    ++-temp-fix : (l r : ClientList) → (x : Client) → (l ++ (x ∷ r)) ≡ ((l ∷ʳ x) ++ r)
+    ++-temp-fix [] r x = refl
+    ++-temp-fix (x₁ ∷ l) r x = cong (_∷_ x₁) (++-temp-fix l r x)
+    send-to-others : ∀ {i} → (cl : ClientList) →
+                     ClientName →
+                     String →
+                     ∞ActorM i room-inbox ⊤₁ (cl-to-context cl) (λ _ → cl-to-context cl)
+    send-to-others [] _ _ = return _
+    send-to-others cl@(_ ∷ _) name message = send-loop [] cl
+      where
+        build-pointer : (l r : ClientList) →
+                      cl-to-context r ⊢ Room-to-Client →
+                      (cl-to-context (l ++ r)) ⊢ Room-to-Client
+        build-pointer [] r p = p
+        build-pointer (x ∷ l) r p = S (build-pointer l r p)
+        recurse : ∀ {i} → (l r : ClientList) → (x : Client) →
+                  ∞ActorM i room-inbox ⊤₁ (cl-to-context (l ++ (x ∷ r))) (λ _ → (cl-to-context (l ++ (x ∷ r))))
+        send-loop : ∀ {i} → (l r : ClientList) →
+          ∞ActorM i room-inbox ⊤₁ (cl-to-context (l ++ r)) (λ _ → cl-to-context (l ++ r))
+        send-loop l [] = return _
+        send-loop l (x ∷ r) with ((Client.name x) ≟ name)
+        ... | (yes _) = recurse l r x
+        ... | (no _) = let p = build-pointer l (x ∷ r) Z
+          in debug ("Sending to " || show (Client.name x) || ": " || message) (p ![t: Z ] (lift (Client.channel x) ∷ [ lift (chat-from name message: message) ]ᵃ) ) >> recurse l r x
+        recurse l r x rewrite ++-temp-fix l r x = send-loop (l ∷ʳ x) r
+chat-message _ (Msg (S ()) _) _
+
+room : ActiveObject
+room = record {
+  state-type = RoomState
+  ; vars = rs-to-context
+  ; methods = room-methods
+  ; extra-messages = []
+  ; handlers = chat-message ∷ leave-room ∷ [ add-to-room ]ᵃ
+  }
+
+Client-to-Room : InboxShape
+Client-to-Room = SendChatMessage ∷ [ LeaveRoom ]ˡ
+
+-- =============
+--  JOIN ROOM
+-- =============
+
+data JoinRoomSuccess : Set where
+  JR-SUCCESS : RoomName → JoinRoomSuccess
+
+data JoinRoomFail : Set where
+  JR-FAIL : RoomName → JoinRoomFail
+
+data JoinRoomStatus : Set where
+  JRS-SUCCESS JRS-FAIL : RoomName → JoinRoomStatus
+
+JoinRoomSuccessReply : MessageType
+JoinRoomSuccessReply = ValueType UniqueTag ∷ ValueType JoinRoomSuccess ∷ [ ReferenceType Client-to-Room ]ˡ
+
+JoinRoomFailReply : MessageType
+JoinRoomFailReply = ValueType UniqueTag ∷ [ ValueType JoinRoomFail ]ˡ
+
+JoinRoomReplyInterface : InboxShape
+JoinRoomReplyInterface = JoinRoomSuccessReply ∷ JoinRoomFailReply ∷ Room-to-Client
+
+JoinRoom : MessageType
+JoinRoom = ValueType UniqueTag ∷ ReferenceType JoinRoomReplyInterface ∷ ValueType RoomName ∷ [ ValueType ClientName ]ˡ
+
+-- =============
+--  CREATE ROOM
+-- =============
+
+data CreateRoomResult : Set where
+  CR-SUCCESS CR-EXISTS : RoomName → CreateRoomResult
+
+CreateRoomReply : MessageType
+CreateRoomReply = ValueType UniqueTag ∷ [ ValueType CreateRoomResult ]ˡ
+
+CreateRoom : MessageType
+CreateRoom = ValueType UniqueTag ∷ ReferenceType [ CreateRoomReply ]ˡ ∷ [ ValueType RoomName ]ˡ
+
+-- ============
+--  LIST ROOMS
+-- ============
+
+RoomList : Set
+RoomList = List RoomName
+
+ListRoomsReply : MessageType
+ListRoomsReply = ValueType UniqueTag ∷ [ ValueType RoomList ]ˡ
+
+ListRooms : MessageType
+ListRooms = ValueType UniqueTag ∷ [ ReferenceType [ ListRoomsReply ]ˡ ]ˡ
+
+-- ===
+--
+-- ===
+
+Client-to-RoomManager : InboxShape
+Client-to-RoomManager = JoinRoom ∷ CreateRoom ∷ [ ListRooms ]ˡ
+
+RoomManagerInterface : InboxShape
+RoomManagerInterface = Client-to-RoomManager
+
+GetRoomManagerReply : MessageType
+GetRoomManagerReply = ValueType UniqueTag ∷ [ ReferenceType RoomManagerInterface ]ˡ
+
+GetRoomManager : MessageType
+GetRoomManager = ValueType UniqueTag ∷ [ ReferenceType [ GetRoomManagerReply ]ˡ ]ˡ
+
+get-room-manager-ci : ChannelInitiation
+get-room-manager-ci = record {
+  request = [ GetRoomManager ]ˡ
+  ; response = record {
+    channel-shape = [ GetRoomManagerReply ]ˡ
+    ; all-tagged = (HasTag _) ∷ [] }
+  ; request-tagged = (HasTag+Ref _) ∷ []
+  }
+
+get-room-manager-header : ActiveMethod
+get-room-manager-header = ResponseMethod get-room-manager-ci
+
+RoomSupervisorInterface : InboxShape
+RoomSupervisorInterface = [ GetRoomManager ]ˡ
+
+ClientSupervisorInterface : InboxShape
+ClientSupervisorInterface =
+  [ ReferenceType RoomSupervisorInterface ]ˡ ∷ [ GetRoomManagerReply ]ˡ
+
+
+--
+--
+--
+
+-- ======================
+--  ROOM MANAGER METHODS
+-- ======================
+
+join-room-header : ActiveMethod
+join-room-header = VoidMethod [ JoinRoom ]ˡ
+
+create-room-ci : ChannelInitiation
+create-room-ci = record {
+  request = [ CreateRoom ]ˡ
+  ; response = record {
+    channel-shape = [ CreateRoomReply ]ˡ
+    ; all-tagged = (HasTag _) ∷ [] }
+  ; request-tagged = (HasTag+Ref _) ∷ []
+  }
+
+create-room-header : ActiveMethod
+create-room-header = ResponseMethod create-room-ci
+
+list-rooms-header : ActiveMethod
+list-rooms-header = ResponseMethod (record {
+  request = [ ListRooms ]ˡ
+  ; response = record {
+    channel-shape = [ ListRoomsReply ]ˡ
+    ; all-tagged = (HasTag _) ∷ []
+    }
+  ; request-tagged = (HasTag+Ref _) ∷ []
+  })
+
+record RoomManagerState : Set₁ where
+  field
+    rooms : RoomList
+
+rms-to-context : RoomManagerState → TypingContext
+rms-to-context rms =
+  let
+    open RoomManagerState
+    rl-to-context : RoomList → TypingContext
+    rl-to-context = map λ _ → room-inbox
+  in rl-to-context (rms .rooms)
+
+room-manager-methods : List ActiveMethod
+room-manager-methods = join-room-header ∷ create-room-header ∷ [ list-rooms-header ]ˡ
+
+room-manager-inbox = methods-shape room-manager-methods
+
+list-rooms : active-method room-manager-inbox RoomManagerState rms-to-context list-rooms-header
+list-rooms _ _ msg state =
+  let
+    open RoomManagerState
+  in return₁ (record {
+    new-state = state
+    ; reply = SendM Z ((lift (state .rooms)) ∷ [])
+    })
+
+lookup-room : ∀ {i} → {Γ : TypingContext} →
+              (rms : RoomManagerState) →
+              RoomName →
+              ∞ActorM i room-manager-inbox (Maybe ((Γ ++ (rms-to-context rms)) ⊢ room-inbox)) (Γ ++ (rms-to-context rms)) (λ _ → Γ ++ (rms-to-context rms))
+lookup-room rms name =
+    let open RoomManagerState
+    in return₁ (loop _ (rms .rooms))
+    where
+      rl-to-context : RoomList → TypingContext
+      rl-to-context = map λ _ → room-inbox
+      loop : (Γ : TypingContext) → (rl : RoomList) → Maybe ((Γ ++ rl-to-context rl) ⊢ room-inbox)
+      loop [] [] = nothing
+      loop [] (x ∷ xs) with (x ≟ name)
+      ... | (yes p) = just Z
+      ... | (no _) = RawMonad._>>=_ Maybe.monad (loop [] xs) λ p → just (S p)
+      loop (x ∷ Γ) rl = RawMonad._>>=_ Maybe.monad (loop Γ rl) (λ p → just (S p))
+
+create-room : active-method room-manager-inbox RoomManagerState rms-to-context create-room-header
+create-room _ _ (Msg Z (room-name ∷ [])) state = do
+    p ← lookup-room state room-name
+    handle-create-room p
+  where
+    handle-create-room : ∀ {i IS} → Maybe ( (IS ∷ rms-to-context state) ⊢ room-inbox) →
+                         ∞ActorM i room-manager-inbox (ActiveReply create-room-ci RoomManagerState rms-to-context (Msg Z (room-name ∷ [])) IS)
+                         (IS ∷ rms-to-context state)
+                         (reply-vars rms-to-context (Msg Z (room-name ∷ [])) IS)
+    handle-create-room (just x) = return₁ (record { new-state = state ; reply = SendM Z ((lift (CR-EXISTS room-name)) ∷ []) })
+    handle-create-room nothing = do
+      spawn∞ (run-active-object room (record { clients = [] }))
+      let
+        open RoomManagerState
+        state' : RoomManagerState
+        state' = record { rooms = room-name ∷ state .rooms}
+      strengthen ((S Z) ∷ (Z ∷ (⊆-suc (⊆-suc ⊆-refl))))
+      return₁ (record { new-state = state' ; reply = SendM Z ((lift (CR-SUCCESS room-name)) ∷ []) })
+create-room _ _ (Msg (S ()) _) _
+
+join-room : active-method room-manager-inbox RoomManagerState rms-to-context join-room-header
+join-room _ (Msg Z (tag ∷ _ ∷ room-name ∷ client-name ∷ [])) state = do
+    p ← lookup-room state room-name
+    handle-join-room p Z
+    return₁ state
+  where
+    handle-join-room : ∀ {i Γ} → Maybe (Γ ⊢ room-inbox) → Γ ⊢ JoinRoomReplyInterface → ∞ActorM i room-manager-inbox ⊤₁ Γ (λ _ → Γ)
+    handle-join-room (just rp) cp = do
+      (rp ![t: S (S Z) ] ((lift tag) ∷ ((lift client-name) ∷ (([ cp ]>: [ S (S Z) ]ᵐ) ∷ []))))
+      (cp ![t: Z ] ((lift tag) ∷ ((lift (JR-SUCCESS room-name)) ∷ (([ rp ]>: (Z ∷ [ S Z ]ᵐ)) ∷ []))))
+    handle-join-room nothing cp = cp ![t: S Z ] ((lift tag) ∷ ((lift (JR-FAIL room-name)) ∷ []))
+join-room _ (Msg (S ()) _) _
+
+room-manager : ActiveObject
+room-manager = record {
+  state-type = RoomManagerState
+  ; vars = rms-to-context
+  ; methods = room-manager-methods
+  ; extra-messages = []
+  ; handlers = join-room ∷ (create-room ∷ (list-rooms ∷ []))
+  }
+
+-- =================
+--  ROOM SUPERVISOR
+-- =================
+
+rs-context : TypingContext
+rs-context = [ room-manager-inbox ]ˡ
+
+rs-vars : ⊤₁ → TypingContext
+rs-vars _ = rs-context
+
+room-supervisor-methods : List ActiveMethod
+room-supervisor-methods = [ get-room-manager-header ]ˡ
+
+rs-inbox = methods-shape room-supervisor-methods
+
+get-room-manager-handler : active-method rs-inbox ⊤₁ rs-vars get-room-manager-header
+get-room-manager-handler _ _ (Msg Z received-fields) _ = return₁ (record { new-state = _ ; reply = SendM Z [ [ (S Z) ]>: ⊆-refl ]ᵃ })
+get-room-manager-handler _ _ (Msg (S ()) _) _
+
+room-supervisor-ao : ActiveObject
+room-supervisor-ao = record
+                       { state-type = ⊤₁
+                       ; vars = λ _ → rs-context
+                       ; methods = room-supervisor-methods
+                       ; extra-messages = []
+                       ; handlers = [ get-room-manager-handler ]ᵃ
+                       }
+
+-- room-supervisor spawns the room-manager
+-- and provides an interface for getting a reference to the current room-manager
+-- we don't ever change that instance, but we could if we want
+room-supervisor : ∀ {i} → ActorM i RoomSupervisorInterface ⊤₁ [] (λ _ → rs-context)
+room-supervisor = begin do
+    spawn∞ (run-active-object room-manager (record { rooms = [] }))
+    run-active-object room-supervisor-ao _
+
+-- ================
+--  CLIENT GENERAL
+-- ================
+ClientInterface : InboxShape
+ClientInterface = [ ReferenceType RoomManagerInterface ]ˡ ∷ CreateRoomReply ∷ ListRoomsReply ∷ JoinRoomReplyInterface
+
+busy-wait : ∀ {i IS Γ} → ℕ → ∞ActorM i IS ⊤₁ Γ (λ _ → Γ)
+busy-wait zero = return _
+busy-wait (suc n) = return tt >> busy-wait n
+
+client-get-room-manager : ∀ {i} → ∞ActorM i ClientInterface ⊤₁ [] (λ _ → [ RoomManagerInterface ]ˡ)
+client-get-room-manager = do
+  record { msg = Msg Z _} ← (selective-receive (λ {
+    (Msg Z x₁) → true
+    ; (Msg (S _) _) → false
+    }))
+    where
+      record { msg = (Msg (S _) _) ; msg-ok = ()}
+  return _
+
+client-create-room : ∀ {i } →
+                     {Γ : TypingContext} →
+                     Γ ⊢ RoomManagerInterface →
+                     UniqueTag →
+                     RoomName →
+                     ∞ActorM i ClientInterface (Lift CreateRoomResult) Γ (λ _ → Γ)
+client-create-room p tag name = do
+  Msg Z (_ ∷ cr ∷ []) ← (call create-room-ci (record {
+    var = p
+    ; chosen-field = Z
+    ; fields = (lift name) ∷ []
+    ; session = record {
+      can-request = (S Z) ∷ []
+      ; response-session = record {
+      can-receive = (S Z) ∷ []
+      ; tag = tag
+      }
+      }
+      }))
+    where
+      Msg (S ()) _
+  return cr
+
+add-if-join-success : TypingContext →
+                      Lift {lzero} {lsuc lzero} JoinRoomStatus →
+                      TypingContext
+add-if-join-success Γ (lift (JRS-SUCCESS x)) = Client-to-Room ∷ Γ
+add-if-join-success Γ (lift (JRS-FAIL x)) = Γ
+
+client-join-room : ∀ {i Γ} →
+                   Γ ⊢ RoomManagerInterface →
+                   UniqueTag →
+                   RoomName →
+                   ClientName →
+                   ∞ActorM i ClientInterface (Lift JoinRoomStatus) Γ (add-if-join-success Γ)
+client-join-room p tag room-name client-name = do
+    self
+    S p ![t: Z ] (lift tag ∷ (([ Z ]>: ⊆-suc (⊆-suc (⊆-suc ⊆-refl))) ∷ (lift room-name) ∷ [ lift client-name ]ᵃ))
+    (strengthen (⊆-suc ⊆-refl))
+    m ← (selective-receive (select-join-reply tag))
+    handle-message m
+  where
+    select-join-reply : UniqueTag → MessageFilter ClientInterface
+    select-join-reply tag (Msg Z _) = false
+    select-join-reply tag (Msg (S Z) _) = false
+    select-join-reply tag (Msg (S (S Z)) _) = false
+    select-join-reply tag (Msg (S (S (S Z))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
+    select-join-reply tag (Msg (S (S (S (S Z)))) (tag' ∷ _)) = ⌊ tag ≟ tag' ⌋
+    select-join-reply tag (Msg (S (S (S (S (S Z))))) x₁) = false
+    select-join-reply tag (Msg (S (S (S (S (S (S ())))))) _)
+    handle-message : ∀ {tag i Γ} → (m : SelectedMessage (select-join-reply tag)) →
+                     ∞ActorM i ClientInterface (Lift JoinRoomStatus)
+                       (add-selected-references Γ m) (add-if-join-success Γ)
+    handle-message record { msg = (Msg Z _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S (S Z))) (_ ∷ JR-SUCCESS room-name ∷ _ ∷ [])) } = return (JRS-SUCCESS room-name)
+    handle-message record { msg = (Msg (S (S (S (S Z)))) (_ ∷ JR-FAIL room-name ∷ [])) } = return (JRS-FAIL room-name)
+    handle-message record { msg = (Msg (S (S (S (S (S Z))))) _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) }
+
+client-send-message : ∀ {i  Γ} →
+                      Γ ⊢ Client-to-Room →
+                      ClientName →
+                      String →
+                      ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ)
+client-send-message p client-name message = p ![t: Z ] ([ lift (chat-from client-name message: message) ]ᵃ)
+
+client-receive-message : ∀ {i Γ} →
+                         ∞ActorM i ClientInterface (Lift ChatMessageContent) Γ (λ _ → Γ)
+client-receive-message = do
+    m ← (selective-receive select-message)
+    handle-message m
+  where
+    select-message : MessageFilter ClientInterface
+    select-message (Msg (S (S (S (S (S Z))))) _) = true
+    select-message (Msg _ _) = false
+    handle-message : ∀ {i Γ} → (m : SelectedMessage select-message) →
+                     ∞ActorM i ClientInterface (Lift ChatMessageContent) (add-selected-references Γ m) (λ _ → Γ)
+    handle-message record { msg = (Msg Z _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S Z) _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S Z)) _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S (S Z))) x₁) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S (S (S Z)))) _) ; msg-ok = () }
+    handle-message record { msg = (Msg (S (S (S (S (S Z))))) (_ ∷ m ∷ f)) ; msg-ok = _ } = return m
+    handle-message record { msg = (Msg (S (S (S (S (S (S ())))))) _) }
+
+client-leave-room : ∀ {i Γ} →
+                    Γ ⊢ Client-to-Room →
+                    ClientName →
+                    ∞ActorM i ClientInterface ⊤₁ Γ (λ _ → Γ)
+client-leave-room p name = p ![t: S Z ] [ lift name ]ᵃ
+
+debug-chat : {a : Level} {A : Set a} → ClientName → ChatMessageContent → A → A
+debug-chat client-name content = let open ChatMessageContent
+  in debug ("client#" || show client-name || " received \"" || content .message || "\" from client#" || show (content .sender))
+
+-- ==========
+--  CLIENT 1
+-- ==========
+
+room1-2 = 1
+room2-3 = 2
+room3-1 = 3
+room1-2-3 = 4
+name1 = 1
+
+client1 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
+client1 = begin do
+  client-get-room-manager
+  _ ← (client-create-room Z 0 room1-2)
+  _ ← (client-create-room Z 1 room3-1)
+  _ ← (client-create-room Z 2 room1-2-3)
+  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room3-1 name1)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room1-2 name1)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name1)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  busy-wait 100
+  (client-send-message (S Z) name1 "hi from 1 to 2")
+  (client-send-message Z name1 "hi from 1 to 2-3")
+  let open ChatMessageContent
+  lift m1 ← client-receive-message
+  lift m2 ← debug-chat name1 m1 client-receive-message
+  lift m3 ← debug-chat name1 m2 client-receive-message
+  debug-chat name1 m3 (client-send-message Z name1 "hi1 from 1 to 2-3")
+  (client-send-message Z name1 "hi2 from 1 to 2-3")
+  (client-send-message Z name1 "hi3 from 1 to 2-3")
+  client-leave-room (S Z) name1
+  client-leave-room (Z) name1
+  (strengthen [])
+
+-- ==========
+--  CLIENT 2
+-- ==========
+
+name2 = 2
+
+client2 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
+client2 = begin do
+  client-get-room-manager
+  _ ← (client-create-room Z 0 room1-2)
+  _ ← (client-create-room Z 1 room2-3)
+  _ ← (client-create-room Z 2 room1-2-3)
+  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room1-2 name2)
+    where
+    (lift (JRS-FAIL failed-room)) → strengthen []
+  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room2-3 name2)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name2)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  busy-wait 100
+  debug "client2 send message" (client-send-message (S Z) name2 "hi from 2 to 3")
+  debug "client2 send message" (client-send-message Z name2 "hi from 2 to 1-3")
+  let open ChatMessageContent
+  lift m1 ← client-receive-message
+  lift m2 ← debug-chat name2 m1 client-receive-message
+  lift m3 ← debug-chat name2 m2 client-receive-message
+  client-leave-room (S Z) name2
+  client-leave-room (Z) name2
+  debug-chat name2 m3 (strengthen [])
+
+-- ==========
+--  CLIENT 3
+-- ==========
+
+name3 = 3
+
+client3 : ∀ {i} → ActorM i ClientInterface ⊤₁ [] (λ _ → [])
+client3 = begin do
+  client-get-room-manager
+  _ ← (client-create-room Z 0 room2-3)
+  _ ← (client-create-room Z 1 room3-1)
+  _ ← (client-create-room Z 2 room1-2-3)
+  lift (JRS-SUCCESS joined-room) ← (client-join-room Z 3 room2-3 name3)
+    where
+    (lift (JRS-FAIL failed-room)) → strengthen []
+  lift (JRS-SUCCESS joined-room) ← (client-join-room (S Z) 4 room3-1 name3)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  lift (JRS-SUCCESS joined-room) ← (client-join-room (S (S Z)) 5 room1-2-3 name3)
+    where
+      (lift (JRS-FAIL failed-room)) → strengthen []
+  busy-wait 100
+  debug "client3 send message" (client-send-message (S Z) name3 "hi from 3 to 1")
+  debug "client3 send message" (client-send-message Z name3 "hi from 3 to 1-2")
+  let open ChatMessageContent
+  lift m1 ← client-receive-message
+  lift m2 ← debug-chat name3 m1 client-receive-message
+  lift m3 ← debug-chat name3 m2 client-receive-message
+  debug-chat name3 m3 (client-leave-room Z name3)
+  client-leave-room (S Z) name3
+  client-leave-room Z name3
+  (strengthen [])
+
+-- ===================
+--  CLIENT SUPERVISOR
+-- ===================
+
+cs-context : TypingContext
+cs-context = RoomManagerInterface ∷ RoomSupervisorInterface ∷ []
+
+client-supervisor : ∀ {i} → ActorM i ClientSupervisorInterface ⊤₁ [] (λ _ → cs-context)
+client-supervisor = begin do
+    wait-for-room-supervisor
+    (get-room-manager Z 0)
+    spawn-clients
+  where
+    wait-for-room-supervisor : ∀ {i Γ} → ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomSupervisorInterface ∷ Γ)
+    wait-for-room-supervisor = do
+      record { msg = Msg Z f } ← (selective-receive (λ {
+        (Msg Z _) → true
+        ; (Msg (S _) _) → false
+        }))
+        where
+          record { msg = (Msg (S _) _) ; msg-ok = () }
+      return _
+    get-room-manager : ∀ {i Γ} →
+                     Γ ⊢ RoomSupervisorInterface →
+                     UniqueTag →
+                      ∞ActorM i ClientSupervisorInterface ⊤₁ Γ (λ _ → RoomManagerInterface ∷ Γ)
+    get-room-manager p tag = do
+      Msg Z f ← (call get-room-manager-ci (record {
+          var = p
+          ; chosen-field = Z
+          ; fields = []
+          ; session = record {
+            can-request = ⊆-refl
+            ; response-session = record {
+            can-receive = (S Z) ∷ []
+            ; tag = tag }
+            }
+          }))
+        where
+          Msg (S ()) _
+      return _
+    spawn-clients : ∀ {i} → ∞ActorM i ClientSupervisorInterface ⊤₁ cs-context (λ _ → cs-context)
+    spawn-clients = do
+      spawn client1
+      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
+      (strengthen (⊆-suc ⊆-refl))
+      (spawn client2)
+      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
+      (strengthen (⊆-suc ⊆-refl))
+      (spawn client3)
+      Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
+      (strengthen (⊆-suc ⊆-refl))
+
+-- chat-supervisor is the top-most actor
+-- it spawns and connects the ClientRegistry to the RoomRegistry
+chat-supervisor : ∀ {i} → ∞ActorM i [] ⊤₁ [] (λ _ → [])
+chat-supervisor = do
+    spawn room-supervisor
+    spawn client-supervisor
+    Z ![t: Z ] [ [ S Z ]>: ⊆-refl ]ᵃ
+    strengthen []
+
diff --git a/src/Selective/Examples/Main-generated.agda b/src/Selective/Examples/Main-generated.agda
index 30ad3cd..c15c1fd 100644
--- a/src/Selective/Examples/Main-generated.agda
+++ b/src/Selective/Examples/Main-generated.agda
@@ -1,10 +1,11 @@
 module Selective.Examples.Main-generated where
 import Selective.Examples.PingPong as PingPong
-import Selective.Examples.Call as Call
+import Selective.Examples.TestCall as Call
+import Selective.Examples.TestCall2 as Call2
 import Selective.Examples.Fibonacci as Fib
 import Selective.Examples.Chat as Chat
 import Selective.Examples.Bookstore as Bookstore
-import Selective.Examples.TestAC as TestAC
+import Selective.Examples.TestAO as TestAO
 
 open import Selective.Runtime
 open import Selective.SimulationEnvironment
@@ -14,9 +15,10 @@ open ∞ActorM
 
 pingpongEntry = singleton-env (PingPong.spawner .force)
 callEntry = singleton-env (Call.calltestActor .force)
+call2Entry = singleton-env (Call2.calltestActor .force)
 fibEntry = singleton-env (Fib.spawner .force)
 chatEntry = singleton-env (Chat.chat-supervisor .force)
 bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force)
-testacEntry = singleton-env (TestAC.calculator-test-actor .force)
+testaoEntry = singleton-env (TestAO.calculator-test-actor .force)
 
-main = IO.run (run-env testacEntry)
+main = IO.run (run-env call2Entry)
diff --git a/src/Selective/Examples/Main-template.agda b/src/Selective/Examples/Main-template.agda
index ad8938f..3cc2207 100644
--- a/src/Selective/Examples/Main-template.agda
+++ b/src/Selective/Examples/Main-template.agda
@@ -1,10 +1,11 @@
 module Selective.Examples.Main-generated where
 import Selective.Examples.PingPong as PingPong
-import Selective.Examples.Call as Call
+import Selective.Examples.TestCall as Call
+import Selective.Examples.TestCall2 as Call2
 import Selective.Examples.Fibonacci as Fib
 import Selective.Examples.Chat as Chat
 import Selective.Examples.Bookstore as Bookstore
-import Selective.Examples.TestAC as TestAC
+import Selective.Examples.TestAO as TestAO
 
 open import Selective.Runtime
 open import Selective.SimulationEnvironment
@@ -14,9 +15,10 @@ open ∞ActorM
 
 pingpongEntry = singleton-env (PingPong.spawner .force)
 callEntry = singleton-env (Call.calltestActor .force)
+call2Entry = singleton-env (Call2.calltestActor .force)
 fibEntry = singleton-env (Fib.spawner .force)
 chatEntry = singleton-env (Chat.chat-supervisor .force)
 bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force)
-testacEntry = singleton-env (TestAC.calculator-test-actor .force)
+testaoEntry = singleton-env (TestAO.calculator-test-actor .force)
 
 main = IO.run (run-env __ENTRY__)
diff --git a/src/Selective/Examples/TestAC.agda b/src/Selective/Examples/TestAC.agda
deleted file mode 100644
index 8066723..0000000
--- a/src/Selective/Examples/TestAC.agda
+++ /dev/null
@@ -1,74 +0,0 @@
-module Selective.Examples.TestAC where
-
-open import Selective.ActorMonad
-open import Prelude
-open import Selective.Examples.Channel
-open import Selective.Examples.Call2
-open import Selective.Examples.ActiveObjects
-
-
-open import Debug
-open import Data.Nat.Show using (show)
-
-calculator-ci : ChannelInitiation
-calculator-ci = record {
-  request = Calculator
-  ; response = record { channel-shape = AddReply ; all-tagged = (HasTag _) ∷ [] }
-  ; request-tagged = (HasTag+Ref _) ∷ [] }
-
-calculator-methods : List ChannelInitiation
-calculator-methods = calculator-ci ∷ calculator-ci ∷ []
-
-calculator-inbox = active-inbox-shape calculator-methods
-
-add : (active-method calculator-inbox ⊤₁ (λ _ → []) calculator-ci)
-add (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z  [ lift (n + m)]ᵃ })
-add (Msg (S ()) _) _
-
-multiply : (active-method calculator-inbox ⊤₁ (λ _ → []) calculator-ci)
-multiply (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n * m)]ᵃ })
-multiply (Msg (S ()) _) _
-
-calculator : ActiveObject
-calculator = record {
-  state-type = ⊤₁
-  ; vars = λ _ → []
-  ; methods = calculator-methods
-  ; handlers = add ∷ multiply ∷ []
-  }
-
-calculator-actor = run-active-object calculator _
-
-calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calculator-test-actor = do
-  spawn∞ calculator-actor
-  Msg Z (_ ∷ n ∷ []) ← call CalculatorProtocol (record {
-    var = Z
-    ; chosen-field = Z
-    ; fields = lift 32 ∷ [ lift 10 ]ᵃ
-    ; session = record {
-      can-request = [ Z ]ᵐ
-      ; response-session = record {
-        can-receive = [ Z ]ᵐ
-        ; tag = 0
-        }
-      }
-    })
-    where
-      Msg (S ()) _
-  Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculatorProtocol (record {
-    var = Z
-    ; chosen-field = Z
-    ; fields = lift 32 ∷ [ lift 10 ]ᵃ
-    ; session = record {
-      can-request = [ S Z ]ᵐ
-      ; response-session = record {
-        can-receive = [ Z ]ᵐ
-        ; tag = 1
-        }
-      }
-    }))
-    where
-      Msg (S ()) _
-  debug (show m) (strengthen [])
-  return m
diff --git a/src/Selective/Examples/TestAO.agda b/src/Selective/Examples/TestAO.agda
new file mode 100644
index 0000000..defa9d6
--- /dev/null
+++ b/src/Selective/Examples/TestAO.agda
@@ -0,0 +1,105 @@
+module Selective.Examples.TestAO where
+
+open import Selective.ActorMonad
+open import Prelude
+open import Selective.Libraries.Call2
+open import Selective.Libraries.ActiveObjects
+
+
+open import Debug
+open import Data.Nat.Show using (show)
+
+AddReplyMessage : MessageType
+AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
+
+AddReply : InboxShape
+AddReply = [ AddReplyMessage ]ˡ
+
+AddMessage : MessageType
+AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
+
+Calculator : InboxShape
+Calculator = [ AddMessage ]ˡ
+
+CalculatorProtocol : ChannelInitiation
+CalculatorProtocol = record
+                       { request = Calculator
+                       ; response = record {
+                         channel-shape = AddReply
+                         ; all-tagged = (HasTag _) ∷ []
+                         }
+                       ; request-tagged = [ HasTag+Ref _ ]ᵃ
+                       }
+
+TestBox : InboxShape
+TestBox = AddReply
+
+calculator-ci : ChannelInitiation
+calculator-ci = record {
+  request = Calculator
+  ; response = record { channel-shape = AddReply ; all-tagged = (HasTag _) ∷ [] }
+  ; request-tagged = (HasTag+Ref _) ∷ [] }
+
+add-method-header = ResponseMethod calculator-ci
+multiply-method-header = ResponseMethod calculator-ci
+
+calculator-methods : List ActiveMethod
+calculator-methods = add-method-header ∷ multiply-method-header ∷ []
+
+calculator-inbox = methods-shape calculator-methods
+
+calculator-state-vars : ⊤₁ → TypingContext
+calculator-state-vars _ = []
+
+add : (active-method calculator-inbox ⊤₁ calculator-state-vars add-method-header)
+add _ _ (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z  [ lift (n + m)]ᵃ })
+add _ _ (Msg (S ()) _) _
+
+multiply : (active-method calculator-inbox ⊤₁ (λ _ → []) multiply-method-header)
+multiply _ _ (Msg Z (n ∷ m ∷ [])) v = return₁ (record { new-state = _ ; reply = SendM Z [ lift (n * m)]ᵃ })
+multiply _ _ (Msg (S ()) _) _
+
+calculator : ActiveObject
+calculator = record {
+  state-type = ⊤₁
+  ; vars = calculator-state-vars
+  ; methods = calculator-methods
+  ; extra-messages = []
+  ; handlers = add ∷ multiply ∷ []
+  }
+
+calculator-actor = run-active-object calculator _
+
+calculator-test-actor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+calculator-test-actor = do
+  spawn∞ calculator-actor
+  Msg Z (_ ∷ n ∷ []) ← call CalculatorProtocol (record {
+    var = Z
+    ; chosen-field = Z
+    ; fields = lift 32 ∷ [ lift 10 ]ᵃ
+    ; session = record {
+      can-request = [ Z ]ᵐ
+      ; response-session = record {
+        can-receive = [ Z ]ᵐ
+        ; tag = 0
+        }
+      }
+    })
+    where
+      Msg (S ()) _
+  Msg Z (_ ∷ m ∷ []) ← debug (show n) (call CalculatorProtocol (record {
+    var = Z
+    ; chosen-field = Z
+    ; fields = lift 32 ∷ [ lift 10 ]ᵃ
+    ; session = record {
+      can-request = [ S Z ]ᵐ
+      ; response-session = record {
+        can-receive = [ Z ]ᵐ
+        ; tag = 1
+        }
+      }
+    }))
+    where
+      Msg (S ()) _
+  debug (show m) (strengthen [])
+  return m
diff --git a/src/Selective/Examples/TestCall.agda b/src/Selective/Examples/TestCall.agda
new file mode 100644
index 0000000..45d9fea
--- /dev/null
+++ b/src/Selective/Examples/TestCall.agda
@@ -0,0 +1,41 @@
+module Selective.Examples.TestCall where
+
+open import Selective.Libraries.Call
+open import Prelude
+
+AddReplyMessage : MessageType
+AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
+
+AddReply : InboxShape
+AddReply = [ AddReplyMessage ]ˡ
+
+AddMessage : MessageType
+AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
+
+Calculator : InboxShape
+Calculator = [ AddMessage ]ˡ
+
+calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
+calculatorActor .force = receive ∞>>= λ {
+  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
+    (Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ)) ∞>> (do
+    strengthen []
+    calculatorActor)
+  ; (Msg (S ()) _)
+  }
+
+TestBox : InboxShape
+TestBox = AddReply
+
+calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+calltestActor .force = spawn∞ calculatorActor ∞>> do
+    x ← call Z Z 0
+         ((lift 10) ∷ [ lift 32 ]ᵃ)
+         ⊆-refl Z
+    strengthen []
+    return-result x
+  where
+    return-result : SelectedMessage {TestBox} (call-select 0 [ Z ]ᵐ Z) →
+                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
+    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
\ No newline at end of file
diff --git a/src/Selective/Examples/Call2.agda b/src/Selective/Examples/TestCall2.agda
similarity index 68%
rename from src/Selective/Examples/Call2.agda
rename to src/Selective/Examples/TestCall2.agda
index 7d809e8..fd039a9 100644
--- a/src/Selective/Examples/Call2.agda
+++ b/src/Selective/Examples/TestCall2.agda
@@ -1,78 +1,59 @@
-module Selective.Examples.Call2 where
-
-open import Selective.ActorMonad
-open import Selective.Examples.Channel
-open import Prelude
-open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax)
-
-open ChannelType
-open ChannelInitiation
-
-call : ∀ {Γ i caller} →
-        ∀ protocol →
-        Request Γ caller protocol →
-        ∞ActorM i caller (Message (protocol .response .channel-shape)) Γ (add-references Γ)
-call protocol request =
-  let
-    open ChannelInitiationSession
-    open Request
-    open ChannelSession
-  in do
-    initiate-channel _ request
-    let rs = request .session .response-session
-    from-channel (protocol .response) rs
-
-AddReplyMessage : MessageType
-AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
-
-AddReply : InboxShape
-AddReply = [ AddReplyMessage ]ˡ
-
-AddMessage : MessageType
-AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
-
-Calculator : InboxShape
-Calculator = [ AddMessage ]ˡ
-
-CalculatorProtocol : ChannelInitiation
-CalculatorProtocol = record
-                       { request = Calculator
-                       ; response = record {
-                         channel-shape = AddReply
-                         ; all-tagged = (HasTag _) ∷ []
-                         }
-                       ; request-tagged = [ HasTag+Ref _ ]ᵃ
-                       }
-
-calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
-calculatorActor .force = receive ∞>>= λ {
-  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
-    Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do
-    strengthen []
-    calculatorActor)
-  ; (Msg (S ()) _)
-  }
-
-TestBox : InboxShape
-TestBox = AddReply
-
-calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calltestActor = do
-  (spawn∞ calculatorActor)
-  Msg Z (tag ∷ n ∷ []) ← call CalculatorProtocol (record {
-    var = Z
-    ; chosen-field = Z
-    ; fields = (lift 32) ∷ [ lift 10 ]ᵃ
-    ; session = record {
-      can-request = ⊆-refl
-      ; response-session = record {
-        can-receive = [ Z ]ᵐ
-        ; tag = 0
-        }
-      }
-    })
-    where
-      Msg (S ()) _
-  (strengthen [])
-  (return n)
-
+module Selective.Examples.TestCall2 where
+
+open import Selective.Libraries.Call2
+open import Prelude
+
+AddReplyMessage : MessageType
+AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
+
+AddReply : InboxShape
+AddReply = [ AddReplyMessage ]ˡ
+
+AddMessage : MessageType
+AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
+
+Calculator : InboxShape
+Calculator = [ AddMessage ]ˡ
+
+CalculatorProtocol : ChannelInitiation
+CalculatorProtocol = record
+                       { request = Calculator
+                       ; response = record {
+                         channel-shape = AddReply
+                         ; all-tagged = (HasTag _) ∷ []
+                         }
+                       ; request-tagged = [ HasTag+Ref _ ]ᵃ
+                       }
+
+calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
+calculatorActor .force = receive ∞>>= λ {
+  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
+    Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ) ∞>> (do
+    strengthen []
+    calculatorActor)
+  ; (Msg (S ()) _)
+  }
+
+TestBox : InboxShape
+TestBox = AddReply
+
+calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+calltestActor = do
+  (spawn∞ calculatorActor)
+  Msg Z (tag ∷ n ∷ []) ← call CalculatorProtocol (record {
+    var = Z
+    ; chosen-field = Z
+    ; fields = (lift 32) ∷ [ lift 10 ]ᵃ
+    ; session = record {
+      can-request = ⊆-refl
+      ; response-session = record {
+        can-receive = [ Z ]ᵐ
+        ; tag = 0
+        }
+      }
+    })
+    where
+      Msg (S ()) _
+  (strengthen [])
+  (return n)
+
diff --git a/src/Selective/Libraries/ActiveObjects.agda b/src/Selective/Libraries/ActiveObjects.agda
new file mode 100644
index 0000000..dc4fd4c
--- /dev/null
+++ b/src/Selective/Libraries/ActiveObjects.agda
@@ -0,0 +1,227 @@
+module Selective.Libraries.ActiveObjects where
+
+open import Selective.Libraries.Channel public
+open import Prelude
+
+open ChannelType
+open ChannelInitiation
+
+data ActiveMethod : Set₁ where
+  VoidMethod : InboxShape → ActiveMethod
+  ResponseMethod : ChannelInitiation → ActiveMethod
+
+active-request-type : ChannelInitiation → InboxShape
+active-request-type record { request = .[] ; response = response ; request-tagged = [] } = []
+active-request-type record { request = .(_ ∷ _) ; response = response ; request-tagged = (px ∷ pxs) } =
+  let rec = active-request-type (record { request = _ ; response = response ; request-tagged = pxs })
+  in extra-fields-shape px ∷ rec
+
+state-vars : ∀ {ci} {st : Set₁} → (st → TypingContext) → Message ci → InboxShape → st → TypingContext
+state-vars f input caller state = caller ∷ add-references (f state) input
+
+
+active-reply-needed-fields : ∀ mt → IsChannelMessage mt → MessageType
+active-reply-needed-fields _ (HasTag MT) = MT
+
+active-reply-type : ChannelType → InboxShape
+active-reply-type record { channel-shape = [] } = []
+active-reply-type record { channel-shape = (x ∷ xs) ; all-tagged = (px ∷ pxs) } =
+  let rec = active-reply-type (record { channel-shape = xs ; all-tagged = pxs })
+  in active-reply-needed-fields x px ∷ rec
+
+record ActiveReply (ci : ChannelInitiation) (state-type : Set₁) (var-f : state-type → TypingContext) (input : Message (active-request-type ci)) (caller : InboxShape) : Set₁ where
+  field
+    new-state : state-type
+    reply : SendMessage (active-reply-type (ci .response)) (state-vars var-f input caller new-state)
+
+reply-vars : ∀ {st ci var-f input} → (st → TypingContext) → Message (active-request-type ci) → (caller : InboxShape) → ActiveReply ci st var-f input caller → TypingContext
+reply-vars f input caller ar = state-vars f input caller (ActiveReply.new-state ar)
+
+active-method : InboxShape → (state-type : Set₁) → (state-type → TypingContext) → ActiveMethod → Set₂
+active-method IS st var-f (VoidMethod IS') =
+  let input-type = Message IS'
+  in (i : Size) →
+     (input : input-type) →
+     (state : st) →
+     ∞ActorM i IS
+       st
+       (add-references (var-f state) input)
+       (λ state' → add-references (var-f state') input)
+active-method IS st var-f (ResponseMethod ci) =
+  let input-type = Message (active-request-type ci)
+  in (i : Size) →
+     (caller : InboxShape) →
+     (input : input-type) →
+     (state : st) →
+     ∞ActorM i IS
+       (ActiveReply ci st var-f input caller)
+       (caller ∷ add-references (var-f state) input)
+       (reply-vars var-f input caller)
+
+active-method-request : ActiveMethod → InboxShape
+active-method-request (VoidMethod x) = x
+active-method-request (ResponseMethod x) = x .request
+
+methods-shape : List ActiveMethod → InboxShape
+methods-shape [] = []
+methods-shape (am ∷ lci) =
+  let rec = methods-shape lci
+      am-shape = active-method-request am
+  in am-shape ++ rec
+
+record ActiveObject : Set₂ where
+  field
+    state-type : Set₁
+    vars : state-type → TypingContext
+    methods : List ActiveMethod
+    extra-messages : InboxShape
+    handlers : All (active-method (methods-shape methods ++ extra-messages) state-type vars) methods
+
+active-inbox-shape : ActiveObject → InboxShape
+active-inbox-shape ac =
+  let open ActiveObject
+  in methods-shape (ac .methods) ++ (ac .extra-messages)
+
+open ActiveObject
+
+forget-message : ∀ {i Γ} →
+                 {IS IS' : InboxShape} →
+                 (m : Message IS) →
+                 ∞ActorM i IS' ⊤₁ (add-references Γ m) (λ _ → Γ)
+forget-message (Msg x x₁) = strengthen (⊆++-l-refl _ _)
+
+data InEither {a} {A : Set a} (v : A) (xs ys : List A) : Set a where
+  Left : (v ∈ xs) → InEither v xs ys
+  Right : (v ∈ ys) → InEither v xs ys
+
+∈++ : ∀ {a} {A : Set a} {v : A} → (xs ys : List A) → (v ∈ (xs ++ ys)) → InEither v xs ys
+∈++ [] ys p = Right p
+∈++ (x ∷ xs) ys Z = Left Z
+∈++ (x ∷ xs) ys (S p) with (∈++ xs ys p)
+... | Left q = Left (S q)
+... | Right q = Right q
+
+invoke-active-method : {i : Size} →
+                       (ac : ActiveObject) →
+                       (input : Message (methods-shape (ac .methods))) →
+                       (state : ac .state-type) →
+                       ∞ActorM i (active-inbox-shape ac)
+                         (ac .state-type) (add-references (ac .vars state) input) (λ x → add-references (ac .vars x) input)
+invoke-active-method ac (Msg x f) state = invoke f (ac .methods) (ac .handlers) x
+  where
+    translate-invoke-pointer : {ci : ChannelInitiation} →
+                               {MT : MessageType} →
+                               (ValueType UniqueTag ∷ ReferenceType (ci .response .channel-shape) ∷ MT) ∈ ci .request →
+                               MT ∈ active-request-type ci
+    translate-invoke-pointer {record { request-tagged = HasTag+Ref MT ∷ _ }} Z = Z
+    translate-invoke-pointer {record { response = response ; request-tagged = _ ∷ rt }} (S p) =
+      let rec = translate-invoke-pointer {record { request = _ ; response = response ; request-tagged = rt }} p
+      in S rec
+    translate-send-pointer : ∀ {ct MT} →
+                               MT ∈ active-reply-type ct →
+                               (TagField ∷ MT) ∈ ct .channel-shape
+    translate-send-pointer {record { channel-shape = [] }} ()
+    translate-send-pointer {record { all-tagged = HasTag MT ∷ _ }} Z = Z
+    translate-send-pointer {record { channel-shape = x ∷ xs ; all-tagged = px ∷ pxs }} (S p) = S (translate-send-pointer p)
+
+    invoke-void-method : {i : Size} {MT : MessageType} →
+             All receive-field-content MT →
+             (IS : InboxShape) →
+             active-method (active-inbox-shape ac) (ac .state-type) (ac .vars) (VoidMethod IS) →
+             MT ∈ IS →
+             ∞ActorM i (active-inbox-shape ac) (ac .state-type) (extract-references MT ++ ac .vars state) (λ st → extract-references MT ++ ac .vars st)
+    invoke-void-method f IS handler p =
+      let
+        active-message : Message IS
+        active-message = Msg p f
+      in do
+        new-state ← handler _ active-message state
+        return₁ new-state
+    invoke-reply-method : {i : Size} {MT : MessageType} →
+              All receive-field-content MT →
+              (ci : ChannelInitiation) →
+              active-method (active-inbox-shape ac) (ac .state-type) (ac .vars) (ResponseMethod ci) →
+              MT ∈ (ci .request) →
+              IsRequestMessage (ci .response .channel-shape) MT →
+              ∞ActorM i (active-inbox-shape ac) (ac .state-type) (extract-references MT ++ ac .vars state) (λ st → extract-references MT ++ ac .vars st)
+    invoke-reply-method (tag ∷ _ ∷ f) ci handler p (HasTag+Ref MT) =
+      let
+        active-message : Message (active-request-type ci)
+        active-message = Msg (translate-invoke-pointer p) f
+      in do
+        record { new-state = new-state ; reply = SendM which fields } ← handler _ _ active-message state
+        send Z (SendM (translate-send-pointer which) (lift tag ∷ fields))
+        return₁ new-state
+    invoke : {i : Size} {MT : MessageType} →
+             All receive-field-content MT →
+             (ams : List ActiveMethod) →
+             All (active-method (active-inbox-shape ac) (ac .state-type) (ac .vars)) ams →
+             MT ∈ methods-shape ams →
+             ∞ActorM i (active-inbox-shape ac)
+                       (ac .state-type)
+                       (add-references-static (ac .vars state) MT)
+                       (λ st → add-references-static (ac .vars st) MT)
+    invoke _ _ [] ()
+    invoke f (am ∷ _) (_ ∷ _) x with (∈++ (active-method-request am) _ x)
+    invoke f (VoidMethod IS ∷ _) (handler ∷ _) x | Left q = invoke-void-method f IS handler q
+    invoke f (ResponseMethod ci ∷ _) (handler ∷ _) x | Left q =
+      let irm = lookup-all q (ci .request-tagged)
+      in invoke-reply-method f ci handler q irm
+    invoke f (_ ∷ cis) (_ ∷ handlers) x | Right q = invoke f cis handlers q
+
+
+handle-active-method : {i : Size} →
+                       (ac : ActiveObject) →
+                       (input : Message (methods-shape (ac .methods))) →
+                       (state : ac .state-type) →
+                       ∞ActorM i (active-inbox-shape ac)
+                         (ac .state-type) (add-references (ac .vars state) input) (ac .vars)
+handle-active-method ac input state =
+  do
+    state' ← (invoke-active-method ac input state)
+    forget-message input
+    return₁ state'
+
+accept-sublist-unwrapped : (xs ys zs : InboxShape) → ∀{MT} → MT ∈ (xs ++ ys ++ zs) → Bool
+accept-sublist-unwrapped [] [] zs p = false
+accept-sublist-unwrapped [] (y ∷ ys) zs Z = true
+accept-sublist-unwrapped [] (y ∷ ys) zs (S p) = accept-sublist-unwrapped [] ys zs p
+accept-sublist-unwrapped (x ∷ xs) ys zs Z = false
+accept-sublist-unwrapped (x ∷ xs) ys zs (S p) = accept-sublist-unwrapped xs ys zs p
+
+
+accept-sublist : (xs ys zs : InboxShape) → MessageFilter (xs ++ ys ++ zs)
+accept-sublist xs ys zs (Msg received-message-type received-fields) = accept-sublist-unwrapped xs ys zs received-message-type
+
+record AcceptSublistDependent (IS : InboxShape) (accepted-type : MessageType) : Set₁ where
+  field
+    accepted-which : accepted-type ∈ IS
+    fields : All receive-field-content accepted-type
+
+receive-active-method : {i : Size} →
+                        {Γ : TypingContext} →
+                        (ac : ActiveObject) →
+                        ∞ActorM i (active-inbox-shape ac) (Message (methods-shape (ac .methods))) Γ (add-references Γ)
+receive-active-method ac = do
+    record { msg = Msg {MT} p f ; msg-ok = msg-ok } ← selective-receive (accept-sublist [] (methods-shape (ac .methods)) (ac .extra-messages))
+    let record {accepted-which = aw ; fields = fields } = rewrap-message (methods-shape (ac .methods)) (ac .extra-messages) p f msg-ok
+    return₁ (Msg {MT = MT} aw fields)
+  where
+    rewrap-message : ∀{MT} → (ys zs : InboxShape) → (p : MT ∈ (ys ++ zs)) → All receive-field-content MT → (accept-sublist-unwrapped [] ys zs p) ≡ true → AcceptSublistDependent ys MT
+    rewrap-message [] zs which f ()
+    rewrap-message (x ∷ ys) zs Z f p = record { accepted-which = Z ; fields = f }
+    rewrap-message (x ∷ ys) zs (S which) f p =
+      let
+        rec = rewrap-message ys zs which f p
+        open AcceptSublistDependent
+      in record { accepted-which = S (rec .accepted-which) ; fields = rec .fields }
+
+run-active-object : {i : Size} →
+                    (ac : ActiveObject) →
+                    (state : ac .state-type) →
+                    ∞ActorM (↑ i) (active-inbox-shape ac) (ac .state-type) ((ac .vars) state) (ac .vars)
+run-active-object ac state .force =
+  receive-active-method ac ∞>>= λ { m .force →
+  handle-active-method ac m state ∞>>= λ state' →
+  run-active-object ac state'
+  }
diff --git a/src/Selective/Examples/Call.lagda.tex b/src/Selective/Libraries/Call.lagda.tex
similarity index 73%
rename from src/Selective/Examples/Call.lagda.tex
rename to src/Selective/Libraries/Call.lagda.tex
index e79368f..6c792d9 100644
--- a/src/Selective/Examples/Call.lagda.tex
+++ b/src/Selective/Libraries/Call.lagda.tex
@@ -1,7 +1,7 @@
 \begin{code}
-module Selective.Examples.Call where
+module Selective.Libraries.Call where
 
-open import Selective.ActorMonad
+open import Selective.ActorMonad public
 open import Prelude
 
 open SelectedMessage
@@ -93,42 +93,4 @@
       px ∷ (translate-fields vals)
     translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) =
       ([ (S p) ]>: v) ∷ (translate-fields vals)
-
-AddReplyMessage : MessageType
-AddReplyMessage = ValueType UniqueTag ∷ [ ValueType ℕ ]ˡ
-
-AddReply : InboxShape
-AddReply = [ AddReplyMessage ]ˡ
-
-AddMessage : MessageType
-AddMessage = ValueType UniqueTag ∷ ReferenceType AddReply ∷ ValueType ℕ ∷ [ ValueType ℕ ]ˡ
-
-Calculator : InboxShape
-Calculator = [ AddMessage ]ˡ
-
-calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
-calculatorActor .force = receive ∞>>= λ {
-  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
-    (Z ![t: Z ] (lift tag ∷ [ lift (n + m) ]ᵃ)) ∞>> (do
-    strengthen []
-    calculatorActor)
-  ; (Msg (S ()) _)
-  }
-
-TestBox : InboxShape
-TestBox = AddReply
-
-calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calltestActor .force = spawn∞ calculatorActor ∞>> do
-    x ← call Z Z 0
-         ((lift 10) ∷ [ lift 32 ]ᵃ)
-         ⊆-refl Z
-    strengthen []
-    return-result x
-  where
-    return-result : SelectedMessage {TestBox} (call-select 0 [ Z ]ᵐ Z) →
-                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
-    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
-
 \end{code}
diff --git a/src/Selective/Libraries/Call2.agda b/src/Selective/Libraries/Call2.agda
new file mode 100644
index 0000000..96bb9e7
--- /dev/null
+++ b/src/Selective/Libraries/Call2.agda
@@ -0,0 +1,21 @@
+module Selective.Libraries.Call2 where
+
+open import Selective.Libraries.Channel public
+open import Prelude
+
+open ChannelType
+open ChannelInitiation
+
+call : ∀ {Γ i caller} →
+        ∀ protocol →
+        Request Γ caller protocol →
+        ∞ActorM i caller (Message (protocol .response .channel-shape)) Γ (add-references Γ)
+call protocol request =
+  let
+    open ChannelInitiationSession
+    open Request
+    open ChannelSession
+  in do
+    initiate-channel _ request
+    let rs = request .session .response-session
+    from-channel (protocol .response) rs
diff --git a/src/Selective/Examples/CallNoComments.lagda.tex b/src/Selective/Libraries/CallNoComments.lagda.tex
similarity index 98%
rename from src/Selective/Examples/CallNoComments.lagda.tex
rename to src/Selective/Libraries/CallNoComments.lagda.tex
index 70b4d44..7915d78 100644
--- a/src/Selective/Examples/CallNoComments.lagda.tex
+++ b/src/Selective/Libraries/CallNoComments.lagda.tex
@@ -1,5 +1,5 @@
 \begin{code}
-module Selective.Examples.CallNoComments where
+module Selective.Libraries.CallNoComments where
 
 open import Selective.ActorMonad
 open import Prelude
diff --git a/src/Selective/Examples/Channel.agda b/src/Selective/Libraries/Channel.agda
similarity index 92%
rename from src/Selective/Examples/Channel.agda
rename to src/Selective/Libraries/Channel.agda
index 9762457..a31bbf4 100644
--- a/src/Selective/Examples/Channel.agda
+++ b/src/Selective/Libraries/Channel.agda
@@ -1,8 +1,7 @@
-module Selective.Examples.Channel where
+module Selective.Libraries.Channel where
 
-open import Selective.ActorMonad
+open import Selective.ActorMonad public
 open import Prelude
-open import Data.Product using (Σ ; _,_ ; _×_ ; Σ-syntax)
 
 UniqueTag = ℕ
 TagField = ValueType UniqueTag
@@ -60,8 +59,16 @@ data DecideAccept : {MT CT : MessageType} {caller : InboxShape} →
                       IsChannelMessage CT →
                       All receive-field-content MT →
                       Set₁ where
-     Acceptable : ∀ {MT caller tag} {rest : All receive-field-content MT} {p : (TagField ∷ MT) ∈ caller} → DecideAccept tag p p (HasTag MT) (tag ∷ rest)
-     Unacceptable : ∀ {MT CT caller tag} {p : MT ∈ caller} {q : CT ∈ caller} {irp : IsChannelMessage CT} {fields : All receive-field-content MT} → DecideAccept tag p q irp fields
+     Acceptable : ∀ {MT caller tag}
+                    {rest : All receive-field-content MT}
+                    {p : (TagField ∷ MT) ∈ caller} →
+                    DecideAccept tag p p (HasTag MT) (tag ∷ rest)
+     Unacceptable : ∀ {MT CT caller tag}
+                      {p : MT ∈ caller}
+                      {q : CT ∈ caller}
+                      {irp : IsChannelMessage CT}
+                      {fields : All receive-field-content MT} →
+                      DecideAccept tag p q irp fields
 
 accept-response-candidate : {MT CT : MessageType} {receiver : InboxShape} →
                             (tag : UniqueTag) →
@@ -120,7 +127,8 @@ convert-response-unwrapped tag x fields (candidate ∷ candidates) ok  with (acc
 
 
 convert-response : ∀ {ct receiver} {session : ChannelSession ct receiver} →
-                     (sm : SelectedMessage (accept-response session)) → ChannelMessageDependent (ct .channel-shape) (selected-type sm)
+                     (sm : SelectedMessage (accept-response session)) →
+                     ChannelMessageDependent (ct .channel-shape) (selected-type sm)
 convert-response {ct} {session = session} record { msg = (Msg x fields) ; msg-ok = msg-ok } =
   let
   open ChannelType