diff --git a/src/EnvironmentOperations.agda b/src/EnvironmentOperations.agda
index d56a5c6..817dde6 100644
--- a/src/EnvironmentOperations.agda
+++ b/src/EnvironmentOperations.agda
@@ -35,14 +35,17 @@ new-actor {IS} {A} {post} m name = record
                                         ; pre = []
                                         ; pre-eq-refs = refl
                                         ; post = post
-                                        ; actor-m = m
+                                        ; computation = m ⟶ []
                                         ; name = name
                                         }
 
+
 -- An actor can be lifted to run sub-programs that need less references
-lift-actor : (actor : Actor) → {pre : TypingContext} → (references : Store) →
-              (pre-eq-refs : (map shape references) ≡ pre) →
-              ActorM ∞ (inbox-shape actor) (A actor) pre (post actor) → Actor
+lift-actor : (actor : Actor) → {pre : TypingContext} →
+             (references : Store) →
+             (pre-eq-refs : (map shape references) ≡ pre) →
+             ActorState ∞ (inbox-shape actor) (A actor) pre (post actor) →
+             Actor
 lift-actor actor {pre} references pre-eq-refs m = record
                                               { inbox-shape = inbox-shape actor
                                               ; A = A actor
@@ -50,13 +53,13 @@ lift-actor actor {pre} references pre-eq-refs m = record
                                               ; pre = pre
                                               ; pre-eq-refs = pre-eq-refs
                                               ; post = post actor
-                                              ; actor-m = m
+                                              ; computation = m
                                               ; name = name actor
                                               }
 
 -- Replace the monadic part of an actor
 -- Many of the bind-operations don't change anything except what the next step should be.
-replace-actorM : (actor : Actor) → ActorM ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
+replace-actorM : (actor : Actor) → ActorState ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
 replace-actorM actor m = record
                            { inbox-shape = inbox-shape actor
                            ; A = A actor
@@ -64,14 +67,15 @@ replace-actorM actor m = record
                            ; pre = pre actor
                            ; pre-eq-refs = pre-eq-refs actor
                            ; post = post actor
-                           ; actor-m = m
+                           ; computation = m
                            ; name = name actor
                            }
 
+
 -- Add one reference to an actor.
 -- Used when receiving a reference, spawn, or self.
 -- The precondition and references are equal via the congruence relation on consing the shape of the reference.
-add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
+add-reference : (actor : Actor) → (nm : NamedInbox) → ActorState ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
 add-reference actor nm m = record
                              { inbox-shape = inbox-shape actor
                              ; A = A actor
@@ -79,11 +83,11 @@ add-reference actor nm m = record
                              ; pre = shape nm ∷ pre actor
                              ; pre-eq-refs = cong (_∷_ (shape nm)) (pre-eq-refs actor)
                              ; post = post actor
-                             ; actor-m = m
+                             ; computation = m
                              ; name = name actor
                              }
 
-add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
+add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorState ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
 add-references-to-actor actor nms m = record
                                         { inbox-shape = inbox-shape actor
                                         ; A = A actor
@@ -91,13 +95,13 @@ add-references-to-actor actor nms m = record
                                         ; pre = map shape nms ++ pre actor
                                         ; pre-eq-refs = trans (map-++-commute shape nms (references actor)) (cong (_++_ (map shape nms)) (pre-eq-refs actor))
                                         ; post = post actor
-                                        ; actor-m = m
+                                        ; computation = m
                                         ; name = name actor
                                         }
 
 add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} →
   map shape nms ++ pre actor ≡ add-references (pre actor) x →
-  ActorM ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) →
+  ActorState ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) →
   Actor
 add-references-rewrite actor nms {x} p m = record
                              { inbox-shape = inbox-shape actor
@@ -106,7 +110,7 @@ add-references-rewrite actor nms {x} p m = record
                              ; pre = add-references (pre actor) x
                              ; pre-eq-refs = trans (trans (map-++-commute shape nms (references actor)) (cong (_++_ (map shape nms)) (pre-eq-refs actor))) p
                              ; post = post actor
-                             ; actor-m = m
+                             ; computation = m
                              ; name = name actor
                              }
 
@@ -247,27 +251,27 @@ messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-va
 
 -- Add a new actor to the environment.
 -- The actor is added to the top of the list of actors.
-add-top : ∀ {IS A post} → ActorM ∞ IS A [] post → Env → Env
-add-top {IS} {A} {post} actor-m env = record
-                                 { acts = record
-                                            { inbox-shape = IS
-                                            ; A = A
-                                            ; references = []
-                                            ; pre = []
-                                            ; pre-eq-refs = refl
-                                            ; post = post
-                                            ; actor-m = actor-m
-                                            ; name = fresh-name env
-                                            } ∷ acts env
-                                 ; blocked = blocked env
-                                 ; env-inboxes = [] ∷ env-inboxes env
-                                 ; store = inbox# fresh-name env [ IS ] ∷ store env
-                                 ; fresh-name = suc (fresh-name env)
-                                 ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env)
-                                 ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
-                                 ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
-                                 ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map  Data.Nat.Properties.≤-step (name-is-fresh env)
-                                 }
+add-top : ∀ {IS A post} → ActorState ∞ IS A [] post → Env → Env
+add-top {IS} {A} {post} m env = record
+                 { acts = record
+                        { inbox-shape = IS
+                        ; A = A
+                        ; references = []
+                        ; pre = []
+                        ; pre-eq-refs = refl
+                        ; post = post
+                        ; computation = m
+                        ; name = fresh-name env
+                        } ∷ acts env
+                   ; blocked = blocked env
+                   ; env-inboxes = [] ∷ env-inboxes env
+                   ; store = inbox# fresh-name env [ IS ] ∷ store env
+                   ; fresh-name = suc (fresh-name env)
+                   ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env)
+                   ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
+                   ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
+                   ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map  Data.Nat.Properties.≤-step (name-is-fresh env)
+                   }
   where
     map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ IS ] ∷ store) inbs
     map-suc store [] frsh = []
diff --git a/src/Runtime.agda b/src/Runtime.agda
index 259873c..a295c04 100644
--- a/src/Runtime.agda
+++ b/src/Runtime.agda
@@ -37,8 +37,7 @@ showNames (x ∷ x₁ ∷ names) = show x ++ ", " ++ showNames (x₁ ∷ names)
 -- Creates a nicely formatted string out of a step-trace from the simulation
 show-trace : Trace → String
 show-trace (Return name) = show name ++ " returned"
-show-trace (Bind trace) = "Bind [ " ++ show-trace trace ++ " ]"
-show-trace (BindDouble name) = "Bind " ++ (show name)
+show-trace (Bind name) = "Bind [ " ++ show name ++ " ]"
 show-trace (Spawn spawner spawned) = (show spawner) ++ " spawned " ++ (show spawned)
 show-trace (Send sender receiver references) = (show sender) ++ " sent a message to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]"
 show-trace (Receive name Nothing) = (show name) ++ " received nothing. It was put in the blocked list"
diff --git a/src/Selective/EnvironmentOperations.agda b/src/Selective/EnvironmentOperations.agda
index 189f59b..16fb36c 100644
--- a/src/Selective/EnvironmentOperations.agda
+++ b/src/Selective/EnvironmentOperations.agda
@@ -18,7 +18,7 @@ open import Data.Bool using (Bool ; true ; false)
 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans ; inspect ; [_])
 open import Relation.Nullary using (Dec ; yes ; no)
 
-open import Level using (Lift ; lift ; Level) renaming (suc to lsuc)
+open import Level using (Level ; Lift ; lift) renaming (suc to lsuc)
 open import Size using (∞)
 
 open Actor
@@ -36,14 +36,17 @@ new-actor {IS} {A} {post} m name = record
                                         ; pre = []
                                         ; pre-eq-refs = refl
                                         ; post = post
-                                        ; actor-m = m
+                                        ; computation = m ⟶ []
                                         ; name = name
                                         }
 
+
 -- An actor can be lifted to run sub-programs that need less references
-lift-actor : (actor : Actor) → {pre : TypingContext} → (references : Store) →
-              (pre-eq-refs : (map shape references) ≡ pre) →
-              ActorM ∞ (inbox-shape actor) (A actor) pre (post actor) → Actor
+lift-actor : (actor : Actor) → {pre : TypingContext} →
+             (references : Store) →
+             (pre-eq-refs : (map shape references) ≡ pre) →
+             ActorState ∞ (inbox-shape actor) (A actor) pre (post actor) →
+             Actor
 lift-actor actor {pre} references pre-eq-refs m = record
                                               { inbox-shape = inbox-shape actor
                                               ; A = A actor
@@ -51,13 +54,13 @@ lift-actor actor {pre} references pre-eq-refs m = record
                                               ; pre = pre
                                               ; pre-eq-refs = pre-eq-refs
                                               ; post = post actor
-                                              ; actor-m = m
+                                              ; computation = m
                                               ; name = name actor
                                               }
 
 -- Replace the monadic part of an actor
 -- Many of the bind-operations don't change anything except what the next step should be.
-replace-actorM : (actor : Actor) → ActorM ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
+replace-actorM : (actor : Actor) → ActorState ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
 replace-actorM actor m = record
                            { inbox-shape = inbox-shape actor
                            ; A = A actor
@@ -65,14 +68,15 @@ replace-actorM actor m = record
                            ; pre = pre actor
                            ; pre-eq-refs = pre-eq-refs actor
                            ; post = post actor
-                           ; actor-m = m
+                           ; computation = m
                            ; name = name actor
                            }
 
+
 -- Add one reference to an actor.
 -- Used when receiving a reference, spawn, or self.
 -- The precondition and references are equal via the congruence relation on consing the shape of the reference.
-add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
+add-reference : (actor : Actor) → (nm : NamedInbox) → ActorState ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
 add-reference actor nm m = record
                              { inbox-shape = inbox-shape actor
                              ; A = A actor
@@ -80,11 +84,11 @@ add-reference actor nm m = record
                              ; pre = shape nm ∷ pre actor
                              ; pre-eq-refs = cong (_∷_ (shape nm)) (pre-eq-refs actor)
                              ; post = post actor
-                             ; actor-m = m
+                             ; computation = m
                              ; name = name actor
                              }
 
-add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
+add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorState ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
 add-references-to-actor actor nms m = record
                                         { inbox-shape = inbox-shape actor
                                         ; A = A actor
@@ -92,13 +96,13 @@ add-references-to-actor actor nms m = record
                                         ; pre = map shape nms ++ pre actor
                                         ; pre-eq-refs = trans (map-++-commute shape nms (references actor)) (cong (_++_ (map shape nms)) (pre-eq-refs actor))
                                         ; post = post actor
-                                        ; actor-m = m
+                                        ; computation = m
                                         ; name = name actor
                                         }
 
 add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} →
   map shape nms ++ pre actor ≡ add-references (pre actor) x →
-  ActorM ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) →
+  ActorState ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) →
   Actor
 add-references-rewrite actor nms {x} p m = record
                              { inbox-shape = inbox-shape actor
@@ -107,7 +111,7 @@ add-references-rewrite actor nms {x} p m = record
                              ; pre = add-references (pre actor) x
                              ; pre-eq-refs = trans (trans (map-++-commute shape nms (references actor)) (cong (_++_ (map shape nms)) (pre-eq-refs actor))) p
                              ; post = post actor
-                             ; actor-m = m
+                             ; computation = m
                              ; name = name actor
                              }
 
@@ -241,34 +245,34 @@ messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-va
       FieldsHavePointer store fields →
       FieldsHavePointer (inbox# n [ x ] ∷ store) fields
     fields-valid-suc [] = []
-    fields-valid-suc (v+ valid) = v+ fields-valid-suc valid
-    fields-valid-suc (x ∷r valid) = (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷r (fields-valid-suc valid)
+    fields-valid-suc (FhpV ∷ valid) = FhpV ∷ fields-valid-suc valid
+    fields-valid-suc (FhpR x ∷ valid) = FhpR (suc-p (suc-helper (actual-has-pointer x) frsh) x) ∷ (fields-valid-suc valid)
     message-valid-suc : (nx : NamedMessage IS) → message-valid store nx → message-valid (inbox# n [ x ] ∷ store) nx
     message-valid-suc (NamedM x₁ x₂) px = fields-valid-suc px
 
 -- Add a new actor to the environment.
 -- The actor is added to the top of the list of actors.
-add-top : ∀ {IS A post} → ActorM ∞ IS A [] post → Env → Env
-add-top {IS} {A} {post} actor-m env = record
-                                 { acts = record
-                                            { inbox-shape = IS
-                                            ; A = A
-                                            ; references = []
-                                            ; pre = []
-                                            ; pre-eq-refs = refl
-                                            ; post = post
-                                            ; actor-m = actor-m
-                                            ; name = fresh-name env
-                                            } ∷ acts env
-                                 ; blocked = blocked env
-                                 ; env-inboxes = [] ∷ env-inboxes env
-                                 ; store = inbox# fresh-name env [ IS ] ∷ store env
-                                 ; fresh-name = suc (fresh-name env)
-                                 ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env)
-                                 ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
-                                 ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
-                                 ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map  Data.Nat.Properties.≤-step (name-is-fresh env)
-                                 }
+add-top : ∀ {IS A post} → ActorState ∞ IS A [] post → Env → Env
+add-top {IS} {A} {post} m env = record
+                 { acts = record
+                        { inbox-shape = IS
+                        ; A = A
+                        ; references = []
+                        ; pre = []
+                        ; pre-eq-refs = refl
+                        ; post = post
+                        ; computation = m
+                        ; name = fresh-name env
+                        } ∷ acts env
+                   ; blocked = blocked env
+                   ; env-inboxes = [] ∷ env-inboxes env
+                   ; store = inbox# fresh-name env [ IS ] ∷ store env
+                   ; fresh-name = suc (fresh-name env)
+                   ; actors-valid = record { actor-has-inbox = zero ; references-have-pointer = [] } ∷ ∀map (valid-actor-suc (name-is-fresh env)) (actors-valid env)
+                   ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
+                   ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
+                   ; name-is-fresh = Data.Nat.s≤s (≤-reflexive refl) ∷ ∀map  Data.Nat.Properties.≤-step (name-is-fresh env)
+                   }
   where
     map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ IS ] ∷ store) inbs
     map-suc store [] frsh = []
@@ -502,8 +506,8 @@ valid++ (NamedM x x₁) v = valid-fields v
                    All (reference-has-pointer store) p →
                    All (reference-has-pointer store) (extract-inboxes fields ++ p)
     valid-fields [] ps = ps
-    valid-fields (v+ fhp) ps = valid-fields fhp ps
-    valid-fields (px ∷r fhp) ps = px ∷ (valid-fields fhp ps)
+    valid-fields (FhpV ∷ fhp) ps = valid-fields fhp ps
+    valid-fields (FhpR px ∷ fhp) ps = px ∷ (valid-fields fhp ps)
 
 open _⊢>:_
 
@@ -529,12 +533,13 @@ make-pointers-compatible : ∀ {MT} store pre refs (eq : map shape refs ≡ pre)
                            (rhp : All (reference-has-pointer store) refs) →
                          FieldsHavePointer store (name-fields pre refs rhp fields eq)
 make-pointers-compatible store pre refs eq [] rhp = []
-make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = v+ make-pointers-compatible store _ refs refl fields rhp
-make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = (make-pointer-compatible store x refs px rhp foundFw) ∷r (make-pointers-compatible store _ refs refl fields rhp)
+make-pointers-compatible store _ refs refl (_∷_ {ValueType x} px fields) rhp = FhpV ∷ make-pointers-compatible store _ refs refl fields rhp
+make-pointers-compatible store _ refs refl (_∷_ {ReferenceType x} px fields) rhp = FhpR (make-pointer-compatible store x refs px rhp foundFw) ∷ (make-pointers-compatible store _ refs refl fields rhp)
   where
     foundFw : FoundReference store (actual px)
     foundFw = lookup-reference _ refs rhp refl (actual-is-sendable px)
 
+
 record SplitList {a : Level} {A : Set a} (ls : List A) : Set (lsuc a) where
   field
     heads : List A
diff --git a/src/Selective/Runtime.agda b/src/Selective/Runtime.agda
index 9f5ec33..afe4f90 100644
--- a/src/Selective/Runtime.agda
+++ b/src/Selective/Runtime.agda
@@ -37,8 +37,7 @@ showNames (x ∷ x₁ ∷ names) = show x ++ ", " ++ showNames (x₁ ∷ names)
 -- Creates a nicely formatted string out of a step-trace from the simulation
 show-trace : Trace → String
 show-trace (Return name) = show name ++ " returned"
-show-trace (Bind trace) = "Bind [ " ++ show-trace trace ++ " ]"
-show-trace (BindDouble name) = "Bind " ++ (show name)
+show-trace (Bind name) = "Bind [ " ++ show name ++ " ]"
 show-trace (Spawn spawner spawned) = (show spawner) ++ " spawned " ++ (show spawned)
 show-trace (Send sender receiver references) = (show sender) ++ " sent a message to " ++ (show receiver) ++ " forwarding [" ++ showNames references ++ "]"
 show-trace (Receive name Nothing) = (show name) ++ " received nothing. It was put in the blocked list"
diff --git a/src/Selective/Simulate.agda b/src/Selective/Simulate.agda
index 2997c89..635b15d 100644
--- a/src/Selective/Simulate.agda
+++ b/src/Selective/Simulate.agda
@@ -26,8 +26,7 @@ data ReceiveKind : Set where
 
 data Trace : Set where
   Return : Name → Trace
-  Bind : Trace → Trace
-  BindDouble : Name → Trace -- If we encounter a bind and then a bind again...
+  Bind : Name → Trace
   Spawn : (spawner : Name) → (spawned : Name) → Trace
   Send : (sender : Name) → (receiver : Name) → (references : List Name) → Trace
   Receive : Name → ReceiveKind → Trace
@@ -61,147 +60,96 @@ open ∞Colist
 --
 -- The simulation function is structured by pattern matching on every constructor of ActorM
 -- for the top-most actor.
--- The behaviour of one step depends on whether there is a step coming after or if this is the
--- last step for the actor, so for every constructor we need to handle the case of when the
--- constructor is used in a bind or separately.
 simulate : Env → ∞Colist ∞ EnvStep
 simulate env with (acts env) | (actors-valid env)
--- ===== OUT OF ACTORS =====
 simulate env | [] | _ = delay []
-simulate env | actor ∷ rest | _ with (actor-m actor)
--- ===== Return =====
--- If an actor returns a value but there is nothing that follows,
--- then the actor is done and we can drop it from the list of actors.
-simulate env | actor ∷ rest | _ |
-  Return val = keep-simulating (Return (name actor)) (drop-top-actor env)
--- ===== Bind =====
-simulate env | actor ∷ rest | _ | m ∞>>= f with (m .force)
--- ===== Bind Value =====
--- return v >>= f ≡ f v, via the left identity monad law
--- We keep simulating, with the monadic part of the actor replaced by the value of f applied to v.
--- Recall that the precondition of a return is the same as the postcondition,
--- so the available references does not change.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Return val = keep-simulating (Bind (Return (name actor))) env'
+simulate env | actor ∷ rest | _ with (computation actor)
+simulate env | actor ∷ rest | _ | Return val ⟶ [] = keep-simulating (Return (name actor)) (drop-top-actor env)
+simulate env | actor ∷ rest | valid ∷ restValid | Return val ⟶ (f ∷ cont) = keep-simulating (Return (name actor)) env'
   where
-    bindAct : Actor
-    bindAct = replace-actorM actor ((f val) .force)
+    actor' : Actor
+    actor' = replace-actorM actor ((f val) .force ⟶ cont)
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid)
--- ===== Bind Bind =====
--- (m >>= f) >>= g ≡ m >>= (λ x → f x >>= g) via the associativity monad law.
--- We need to use the associativity law to 'free' the left-most part so that
--- it can be run just one step.
--- The simulation will keep shifting parantheses until it eventually reaches
--- a part that is not a bind inside a bind.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= g |
-  mm ∞>>= f = keep-simulating (Bind (BindDouble (name actor))) env'
+    env' = replace-actors
+             env
+             (actor' ∷ rest)
+             (rewrap-valid-actor valid refl refl refl ∷ restValid)
+simulate env | actor ∷ rest | valid ∷ restValid | (m ∞>>= f) ⟶ cont = keep-simulating (Bind (name actor)) env'
   where
-    bindAct : Actor
-    bindAct = replace-actorM actor (mm ∞>>= λ x → f x >>= g)
+    actor' : Actor
+    actor' = replace-actorM actor (m .force ⟶ (f ∷ cont))
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid)
--- ===== Bind Spawn =====
--- Spawns a new actor and continues with (f tt).
--- Both the spawned actor and (f tt) are put at the back of the round-robin queue.
---
--- The new actor gets the next fresh name and the next env stores the fresh name that comes after that.
--- We prove that the next fresh env is unused via (m ≤ n → m ≤ 1 + n).
---
--- The new actor is added to the top of the store,
--- so we need to update every proof that states that a pointer into the store is valid.
--- Updating the proofs is an easy application of suc for _↦_∈e_ and <-¬≡.
---
--- In conclusion, the spawned actor is first added to the top of the round-robin queue
--- and then moved to the back.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Spawn {NewIS} {B} {_} {postN} bm = keep-simulating (Spawn (name actor) (fresh-name env)) (top-actor-to-back env')
+    env' = replace-actors
+             env
+             (actor' ∷ rest)
+             (rewrap-valid-actor valid refl refl refl ∷ restValid)
+simulate env | actor ∷ rest | valid ∷ restValid | Spawn {NewIS} {B} act ⟶ cont = keep-simulating (Spawn (name actor) (fresh-name env)) env'
   where
     newStoreEntry : NamedInbox
-    newStoreEntry = inbox# fresh-name env [ NewIS ]
+    newStoreEntry = inbox# (fresh-name env) [ NewIS ]
     newStore : Store
     newStore = newStoreEntry ∷ store env
     newAct : Actor
-    newAct = new-actor bm (fresh-name env)
+    newAct = new-actor act (fresh-name env)
     newActValid : ValidActor newStore newAct
     newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] }
     newIsFresh : NameFresh newStore (suc (fresh-name env))
     newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env)
-    bindAct : Actor
-    bindAct = add-reference actor newStoreEntry ((f _) .force)
-    bindActValid : ValidActor newStore bindAct
-    bindActValid = record {
-      actor-has-inbox = suc {pr =
-        suc-helper (actor-has-inbox valid) (name-is-fresh env)
-        } (actor-has-inbox valid)
+    actor' : Actor
+    actor' = add-reference actor newStoreEntry (Return _ ⟶ cont)
+    valid' : ValidActor newStore actor'
+    valid' = record {
+      actor-has-inbox = suc {pr = suc-helper (actor-has-inbox valid) (name-is-fresh env)} (actor-has-inbox valid)
       ; references-have-pointer = [p: zero ][handles: ⊆-refl ] ∷ ∀map
                                       (λ p → suc-p (suc-helper (actual-has-pointer p) (name-is-fresh env)) p)
                                       (references-have-pointer valid) }
     env' : Env
     env' = record
-             { acts = newAct ∷ bindAct ∷ rest
+             { acts = newAct ∷ actor' ∷ rest
              ; blocked = blocked env
-             ; env-inboxes = [] ∷ env-inboxes env
              ; store = newStore
-             ; fresh-name = suc (fresh-name env)
-             ; actors-valid = newActValid ∷ bindActValid ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid
+             ; env-inboxes = [] ∷ env-inboxes env
+             ; actors-valid = newActValid ∷ valid' ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid
              ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
              ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
+             ; fresh-name = suc (fresh-name env)
              ; name-is-fresh = newIsFresh
              }
          where
-           map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs
+           map-suc : (store : Store) → {store' : Store} {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → NameFresh store n → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs
            map-suc store [] frsh = []
-           map-suc store (x ∷ valid) frsh = (messages-valid-suc frsh x) ∷ (map-suc store valid frsh)
--- ===== Bind send reference =====
--- Spawns a reference message and continues with (f tt).
---
--- We find where to send the mesage using lookup-reference,
--- which just traverses the index into 'pre' to find which name / pointer
--- to use from 'references'.
--- We find which name / pointer is being forwarded in the same manner
--- and stores the name together with the message.
--- The found pointer is kept as a proof that we can find the referenced inbox
--- in the store, and the pointer proof is updated whenever the store is updated.
--- Updating the proof is not doing any actual useful work,
--- but we still can't make the proof irrelevant, since we would then need to use a
--- lookup function whenever we dereference a pointer.
---
--- add-message takes a named message and a proof that the named message is valid.
---
--- Sending a message to an actor that is blocked,
--- unblocks it and moves it to the actor queue.
--- The unblocked actor is put in the back of the round-robin queue.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Send {ToIS = ToIS} canSendTo (SendM p fields) = keep-simulating (Bind (Send (name actor) (name foundTo) (reference-names namedFields))) withUnblocked
+           map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ map-suc store valid frsh
+simulate env | actor ∷ rest | valid ∷ restValid | Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont =
+  keep-simulating (Send (name actor) (name foundTo) (reference-names namedFields)) withUnblocked
   where
     foundTo : FoundReference (store env) ToIS
     foundTo = lookup-reference-act valid canSendTo
     namedFields = name-fields-act (store env) actor fields valid
-    bindAct : Actor
-    bindAct = replace-actorM actor ((f _) .force)
+    actor' : Actor
+    actor' = replace-actorM actor (Return _ ⟶ cont)
     withM : Env
-    withM = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid)
+    withM = replace-actors
+              env
+              (actor' ∷ rest)
+              ((rewrap-valid-actor valid refl refl refl) ∷ restValid)
     withUpdatedInbox : Env
-    withUpdatedInbox = update-inbox-env withM (underlying-pointer foundTo) (
-      add-message (NamedM (translate-message-pointer foundTo p) namedFields)
-                          (make-pointers-compatible (store env) (pre actor) (references actor) (pre-eq-refs actor) fields (references-have-pointer valid)))
+    withUpdatedInbox = update-inbox-env
+                         withM
+                         (underlying-pointer foundTo)
+                         (add-message
+                           (NamedM
+                             (translate-message-pointer foundTo tag)
+                             namedFields)
+                           (make-pointers-compatible
+                             (store env)
+                             (pre actor)
+                             (references actor)
+                             (pre-eq-refs actor)
+                             fields
+                             (references-have-pointer valid)))
     withUnblocked : Env
     withUnblocked = unblock-actor withUpdatedInbox (name foundTo)
--- ===== Bind receive =====
--- Receives a message and continues with (f (receivedMessage)) if there is a message in the inbox.
--- The actor is put into the blocked list if the inbox is empty.
---
--- We find the pointer to the actors inbox in the store via (actor-has-inbox valid).
--- We always remove the received message from the inbox (and do nothing if there is no message),
--- but also pattern match on what the next message is, to figure out the right behaviour:
--- * An empty inbox just moves the actor to the blocked list,
---   where it will stay until a message is sent to it.
--- * If the next message is a value, just continue with (f message)
--- * If the next message is a reference,
---   take the proof that the message is valid and use that to prove that the added reference is valid.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Receive = keep-simulating (Bind (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox)))) (env' actorsInbox)
+simulate env | actor ∷ rest | valid ∷ restValid | Receive ⟶ cont = keep-simulating (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox))) (env' actorsInbox)
   where
     actorsInbox : GetInbox (store env) (inbox-shape actor)
     actorsInbox = get-inbox env (actor-has-inbox valid)
@@ -210,29 +158,44 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
     receiveKind [] = Nothing
     receiveKind (NamedM _ ps ∷ xs) = Value (reference-names ps)
     env' : GetInbox (store env) (inbox-shape actor) → Env
-    env' record { messages = [] ; valid = _ } = replace-actors+blocked env
-                                                rest restValid
-                                                (actor ∷ blocked env) (valid ∷ blocked-valid env)
-    env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vmsg } = record
-                                                                   { acts = add-references-rewrite actor (named-inboxes nm) {unname-message nm} (add-references++ nm nmv (pre actor) ) ((f (unname-message nm) .force)) ∷ rest
-                                                                   ; blocked = blocked env
-                                                                   ; env-inboxes = updated-inboxes inboxesAfter
-                                                                   ; store = store env
-                                                                   ; actors-valid = record {
-                                                                     actor-has-inbox = actor-has-inbox valid
-                                                                     ; references-have-pointer = valid++ nm nmv (references-have-pointer valid) } ∷ restValid
-                                                                   ; blocked-valid = blocked-valid env
-                                                                   ; messages-valid = inboxes-valid inboxesAfter
-                                                                   ; fresh-name = fresh-name env
-                                                                   ; name-is-fresh = name-is-fresh env
-                                                                   }
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  SelectiveReceive filter = keep-simulating (Bind (Selective (name actor) (receiveKind selectedMessage))) (env' selectedMessage)
+    env' record { messages = [] } = replace-actors+blocked
+                                      env
+                                      rest
+                                      restValid
+                                      (actor ∷ blocked env)
+                                      (valid ∷ blocked-valid env)
+    env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vms } = record
+                                             { acts = add-references-rewrite
+                                                        actor
+                                                        (named-inboxes nm)
+                                                        {unname-message nm}
+                                                        (add-references++
+                                                          nm
+                                                          nmv
+                                                          (pre actor))
+                                                        (Return (unname-message nm) ⟶ cont)
+                                                        ∷ rest
+                                             ; blocked = blocked env
+                                             ; store = store env
+                                             ; env-inboxes = updated-inboxes inboxesAfter
+                                             ; actors-valid = record {
+                                               actor-has-inbox = actor-has-inbox valid
+                                               ; references-have-pointer = valid++
+                                                                             nm
+                                                                             nmv
+                                                                             (references-have-pointer valid) }
+                                               ∷ restValid
+                                             ; blocked-valid = blocked-valid env
+                                             ; messages-valid = inboxes-valid inboxesAfter
+                                             ; fresh-name = fresh-name env
+                                             ; name-is-fresh = name-is-fresh env
+                                             }
+simulate env | actor ∷ rest | valid ∷ restValid | SelectiveReceive filter ⟶ cont = keep-simulating (Selective (name actor) (receiveKind selectedMessage)) (env' selectedMessage)
   where
     actorsInbox : GetInbox (store env) (inbox-shape actor)
     actorsInbox = get-inbox env (actor-has-inbox valid)
     selectedMessage : FoundInList (GetInbox.messages actorsInbox) (λ x → filter (unname-message x))
-    selectedMessage = find-split (GetInbox.messages actorsInbox) λ x → filter (unname-message x)
+    selectedMessage = find-split (GetInbox.messages actorsInbox) (λ x → filter (unname-message x))
     inboxesAfter = update-inboxes (store env) (env-inboxes env)
                                   (messages-valid env) (actor-has-inbox valid)
                                   (remove-found-message filter)
@@ -253,7 +216,7 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
                                           (GetInbox.valid actorsInbox)
                                           split)
                                         (pre actor))
-                                      (f (record { msg = unname-message (SplitList.el split) ; msg-ok = x }) .force) ∷ rest
+                                      (Return (record { msg = unname-message (SplitList.el split) ; msg-ok = x }) ⟶ cont) ∷ rest
                              ; blocked = blocked env
                              ; store = store env
                              ; env-inboxes = updated-inboxes inboxesAfter
@@ -270,82 +233,29 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
                              ; fresh-name = fresh-name env
                              ; name-is-fresh = name-is-fresh env
                              }
--- ===== Bind lift =====
--- To bind a lift we just perform the lifting of the actor and rewrap it in the same bind, like so:
--- ((Lift x) >>= f) ⇒ liftedX >>= f
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Strengthen {ys} {xs} inc = keep-simulating (Bind (Strengthen (name actor))) env'
+simulate env | actor ∷ rest | valid ∷ restValid | Self ⟶ cont = keep-simulating (Self (name actor)) env'
   where
-    liftedRefs = lift-references inc (references actor) (pre-eq-refs actor)
-    strengthenedM : ∞ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys)
-    strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs)) = return _
-    -- liftedBx : ActorM (inbox-shape actor) B (map shape (contained liftedRefs)) postX
-    -- liftedBx rewrite (sym (contained-eq-inboxes liftedRefs)) = bx
-    bindAct : Actor
-    bindAct = lift-actor actor (contained liftedRefs) refl (strengthenedM ∞>>= f)
-    bindActValid : ValidActor (store env) bindAct
-    bindActValid = record { actor-has-inbox = actor-has-inbox valid
-                          ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) }
+    actor' : Actor
+    actor' = add-reference actor inbox# (name actor) [ (inbox-shape actor) ] (Return _ ⟶ cont)
+    valid' : ValidActor (store env) actor'
+    valid' = record {
+                  actor-has-inbox = actor-has-inbox valid
+                  ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid }
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (bindActValid ∷ restValid)
--- ===== Bind self =====
--- To bind 'self' we just need to add the actors name and type to its references / precondition.
--- We get the proof that the added reference is valid via (actor-has-inbox valid).
--- countinues with (f tt)
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Self = keep-simulating (Bind (Self (name actor))) env'
+    env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid)
+simulate env | actor ∷ rest | valid ∷ restValid | Strengthen {ys} inc ⟶ cont = keep-simulating (Strengthen (name actor)) env'
   where
-    bindAct : Actor
-    bindAct = add-reference actor (inbox# name actor [ inbox-shape actor ]) ((f _) .force)
-    bindActValid : ValidActor (store env) bindAct
-    bindActValid = record { actor-has-inbox = actor-has-inbox valid
-                          ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid }
+    liftedRefs = lift-references inc (references actor) (pre-eq-refs actor)
+    strengthenedM : ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys)
+    strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs))= Return _
+    actor' : Actor
+    actor' = lift-actor actor (contained liftedRefs) refl (strengthenedM ⟶ cont)
+    valid' : ValidActor (store env) actor'
+    valid' = record {
+      actor-has-inbox = actor-has-inbox valid
+      ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) }
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (bindActValid ∷ restValid)
--- ===== Spawn =====
--- Spawn without a following bind.
--- The current actor is finished, so we drop it using drop-top-actor.
--- The new actor is added to the top and will be moved to the bottom of the
--- round-robin queue by keep-simulating
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Spawn act₁ = keep-simulating (Spawn (name actor) (fresh-name env)) (add-top act₁ (drop-top-actor env))
--- ===== Send reference =====
--- Send reference without a following bind.
--- Very similar to send reference with a following bind,
--- but we also drop the actor that sent the value.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Send {ToIS = ToIS} canSendTo (SendM p fields) = keep-simulating (Send (name actor) (name foundTo) (reference-names namedFields)) withUnblocked
-  where
-    foundTo : FoundReference (store env) ToIS
-    foundTo = lookup-reference-act valid canSendTo
-    namedFields = name-fields-act (store env) actor fields valid
-    withUpdatedInbox : Env
-    withUpdatedInbox = update-inbox-env env
-                       (underlying-pointer foundTo)
-                       (add-message (NamedM (translate-message-pointer foundTo p) namedFields)
-                       (make-pointers-compatible (store env) (pre actor) (references actor) (pre-eq-refs actor) fields (references-have-pointer valid)))
-    withTopDropped : Env
-    withTopDropped = drop-top-actor withUpdatedInbox
-    withUnblocked : Env
-    withUnblocked = unblock-actor withTopDropped (name foundTo)
--- ===== Receive =====
--- Receive without a following bind is like return,
--- so just drop the actor.
--- We could remve the message in the inbox,
--- but there is currently no proofs that care about doing so.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Receive = keep-simulating (Receive (name actor) Dropped) (drop-top-actor env)
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  SelectiveReceive _ = keep-simulating (Selective (name actor) Dropped) (drop-top-actor env)
--- ===== Lift =====
--- Just performs the lifting by translating a subset for preconditions
--- to a subset for references.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Strengthen inc = keep-simulating (Strengthen (name actor)) (drop-top-actor env)
--- Self without a following bind is like return,
--- so just drop the actor.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Self = keep-simulating (Self (name actor)) (drop-top-actor env)
+    env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid)
 
 
 keep-simulating trace env .force = record { env = env ; trace = trace } ∷ simulate (top-actor-to-back env)
diff --git a/src/Selective/SimulationEnvironment.agda b/src/Selective/SimulationEnvironment.agda
index b115eab..e8a1d20 100644
--- a/src/Selective/SimulationEnvironment.agda
+++ b/src/Selective/SimulationEnvironment.agda
@@ -9,7 +9,7 @@ open import Data.Nat using (ℕ ; _≟_)
 open import Data.Unit using (⊤ ; tt)
 
 open import Level using (Lift ; lift)
-open import Size using (∞)
+open import Size using (Size ; ∞)
 
 open import Data.Empty using (⊥)
 open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
@@ -77,6 +77,26 @@ record _comp↦_∈_ (n : Name) (wanted : InboxShape) (store : Store) : Set₁ w
     actual-has-pointer : n ↦ actual ∈e store
     actual-handles-wanted : wanted <: actual
 
+Cont : ∀ (i : Size) (IS : InboxShape) {A B : Set₁}
+            (pre : A → TypingContext)
+            (post : B → TypingContext) →
+            Set₂
+Cont i IS {A} {B} pre post = (x : A) → ∞ActorM i IS B (pre x) post
+
+data ContStack (i : Size) (IS : InboxShape) {A : Set₁} (pre : A → TypingContext) :
+     ∀ {B : Set₁} (post : B → TypingContext) → Set₂ where
+  []    : ContStack i IS pre pre
+  _∷_   : ∀{B C}{mid : B → TypingContext} {post : C → TypingContext}
+        → Cont i IS pre mid → ContStack i IS mid post → ContStack i IS pre post
+
+record ActorState (i : Size) (IS : InboxShape) (C : Set₁) (pre : TypingContext) (post : C → TypingContext) : Set₂ where
+  constructor _⟶_
+  field
+    {A}   : Set₁
+    {mid} : A → TypingContext
+    act   : ActorM i IS A pre mid
+    cont  : ContStack i IS mid post
+
 -- An ActorM wrapped up with all of its parameters
 -- We use this to be able to store actor monads of different types in the same list.
 -- We give each actor a name so that we can find its inbox in the store.
@@ -92,7 +112,7 @@ record Actor : Set₂ where
     pre         : TypingContext
     pre-eq-refs : (map NamedInbox.shape references) ≡ pre
     post        : A → TypingContext
-    actor-m     : ActorM ∞ inbox-shape A pre post
+    computation : ActorState ∞ inbox-shape A pre post
     name        : Name
 
 named-field-content : MessageField → Set
@@ -146,15 +166,16 @@ record ValidActor (store : Store) (actor : Actor) : Set₂ where
     actor-has-inbox : has-inbox store actor
     references-have-pointer : all-references-have-a-pointer store actor
 
+data FieldHasPointer (store : Store) : ∀ {f} → named-field-content f → Set₁ where
+  FhpV : ∀ {A} {v : A} → FieldHasPointer store {ValueType A} v
+  FhpR : ∀ {name Fw} → name comp↦ Fw ∈ store → FieldHasPointer store {ReferenceType Fw} name
+
 data FieldsHavePointer (store : Store) : ∀ {MT} → All named-field-content MT → Set₁ where
   [] : FieldsHavePointer store []
-  v+_ : ∀ {MT A} {v : A} {nfc : All named-field-content MT} →
-    FieldsHavePointer store nfc →
-    FieldsHavePointer store {ValueType A ∷ MT} (v ∷ nfc)
-  _∷r_ : ∀ {name Fw MT} {nfc : All named-field-content MT} →
-    name comp↦ Fw ∈ store →
+  _∷_ : ∀ {F p MT} {nfc : All named-field-content MT} →
+    FieldHasPointer store {F} p →
     FieldsHavePointer store nfc →
-    FieldsHavePointer store {ReferenceType Fw ∷ MT} (name ∷ nfc)
+    FieldsHavePointer store {F ∷ MT} (p ∷ nfc)
 
 -- To limit references to only those that are valid for the current store,
 -- we have to prove that name in the message points to an inbox of the same
@@ -229,7 +250,7 @@ singleton-env {IS} {A} {post} actor = record
                                   ; pre = []
                                   ; pre-eq-refs = refl
                                   ; post = post
-                                  ; actor-m = actor
+                                  ; computation = record { act = actor ; cont = [] }
                                   ; name = 0
                                   } ∷ []
                        ; blocked = []
diff --git a/src/Simulate.agda b/src/Simulate.agda
index 5cb0cf2..f903213 100644
--- a/src/Simulate.agda
+++ b/src/Simulate.agda
@@ -26,8 +26,7 @@ data ReceiveKind : Set where
 
 data Trace : Set where
   Return : Name → Trace
-  Bind : Trace → Trace
-  BindDouble : Name → Trace -- If we encounter a bind and then a bind again...
+  Bind : Name → Trace
   Spawn : (spawner : Name) → (spawned : Name) → Trace
   Send : (sender : Name) → (receiver : Name) → (references : List Name) → Trace
   Receive : Name → ReceiveKind → Trace
@@ -60,147 +59,96 @@ open ∞Colist
 --
 -- The simulation function is structured by pattern matching on every constructor of ActorM
 -- for the top-most actor.
--- The behaviour of one step depends on whether there is a step coming after or if this is the
--- last step for the actor, so for every constructor we need to handle the case of when the
--- constructor is used in a bind or separately.
 simulate : Env → ∞Colist ∞ EnvStep
 simulate env with (acts env) | (actors-valid env)
--- ===== OUT OF ACTORS =====
 simulate env | [] | _ = delay []
-simulate env | actor ∷ rest | _ with (actor-m actor)
--- ===== Return =====
--- If an actor returns a value but there is nothing that follows,
--- then the actor is done and we can drop it from the list of actors.
-simulate env | actor ∷ rest | _ |
-  Return val = keep-simulating (Return (name actor)) (drop-top-actor env)
--- ===== Bind =====
-simulate env | actor ∷ rest | _ | m ∞>>= f with (m .force)
--- ===== Bind Value =====
--- return v >>= f ≡ f v, via the left identity monad law
--- We keep simulating, with the monadic part of the actor replaced by the value of f applied to v.
--- Recall that the precondition of a return is the same as the postcondition,
--- so the available references does not change.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Return val = keep-simulating (Bind (Return (name actor))) env'
+simulate env | actor ∷ rest | _ with (computation actor)
+simulate env | actor ∷ rest | _ | Return val ⟶ [] = keep-simulating (Return (name actor)) (drop-top-actor env)
+simulate env | actor ∷ rest | valid ∷ restValid | Return val ⟶ (f ∷ cont) = keep-simulating (Return (name actor)) env'
   where
-    bindAct : Actor
-    bindAct = replace-actorM actor ((f val) .force)
+    actor' : Actor
+    actor' = replace-actorM actor ((f val) .force ⟶ cont)
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid)
--- ===== Bind Bind =====
--- (m >>= f) >>= g ≡ m >>= (λ x → f x >>= g) via the associativity monad law.
--- We need to use the associativity law to 'free' the left-most part so that
--- it can be run just one step.
--- The simulation will keep shifting parantheses until it eventually reaches
--- a part that is not a bind inside a bind.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= g |
-  mm ∞>>= f = keep-simulating (Bind (BindDouble (name actor))) env'
+    env' = replace-actors
+             env
+             (actor' ∷ rest)
+             (rewrap-valid-actor valid refl refl refl ∷ restValid)
+simulate env | actor ∷ rest | valid ∷ restValid | (m ∞>>= f) ⟶ cont = keep-simulating (Bind (name actor)) env'
   where
-    bindAct : Actor
-    bindAct = replace-actorM actor (mm ∞>>= λ x → f x >>= g)
+    actor' : Actor
+    actor' = replace-actorM actor (m .force ⟶ (f ∷ cont))
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid)
--- ===== Bind Spawn =====
--- Spawns a new actor and continues with (f tt).
--- Both the spawned actor and (f tt) are put at the back of the round-robin queue.
---
--- The new actor gets the next fresh name and the next env stores the fresh name that comes after that.
--- We prove that the next fresh env is unused via (m ≤ n → m ≤ 1 + n).
---
--- The new actor is added to the top of the store,
--- so we need to update every proof that states that a pointer into the store is valid.
--- Updating the proofs is an easy application of suc for _↦_∈e_ and <-¬≡.
---
--- In conclusion, the spawned actor is first added to the top of the round-robin queue
--- and then moved to the back.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Spawn {NewIS} {B} {_} {postN} bm = keep-simulating (Spawn (name actor) (fresh-name env)) (top-actor-to-back env')
+    env' = replace-actors
+             env
+             (actor' ∷ rest)
+             (rewrap-valid-actor valid refl refl refl ∷ restValid)
+simulate env | actor ∷ rest | valid ∷ restValid | Spawn {NewIS} {B} act ⟶ cont = keep-simulating (Spawn (name actor) (fresh-name env)) env'
   where
     newStoreEntry : NamedInbox
-    newStoreEntry = inbox# fresh-name env [ NewIS ]
+    newStoreEntry = inbox# (fresh-name env) [ NewIS ]
     newStore : Store
     newStore = newStoreEntry ∷ store env
     newAct : Actor
-    newAct = new-actor bm (fresh-name env)
+    newAct = new-actor act (fresh-name env)
     newActValid : ValidActor newStore newAct
     newActValid = record { actor-has-inbox = zero ; references-have-pointer = [] }
     newIsFresh : NameFresh newStore (suc (fresh-name env))
     newIsFresh = s≤s (≤-reflexive refl) ∷ ∀map ≤-step (name-is-fresh env)
-    bindAct : Actor
-    bindAct = add-reference actor newStoreEntry ((f _) .force)
-    bindActValid : ValidActor newStore bindAct
-    bindActValid = record {
-      actor-has-inbox = suc {pr =
-        suc-helper (actor-has-inbox valid) (name-is-fresh env)
-        } (actor-has-inbox valid)
+    actor' : Actor
+    actor' = add-reference actor newStoreEntry (Return _ ⟶ cont)
+    valid' : ValidActor newStore actor'
+    valid' = record {
+      actor-has-inbox = suc {pr = suc-helper (actor-has-inbox valid) (name-is-fresh env)} (actor-has-inbox valid)
       ; references-have-pointer = [p: zero ][handles: ⊆-refl ] ∷ ∀map
                                       (λ p → suc-p (suc-helper (actual-has-pointer p) (name-is-fresh env)) p)
                                       (references-have-pointer valid) }
     env' : Env
     env' = record
-             { acts = newAct ∷ bindAct ∷ rest
+             { acts = newAct ∷ actor' ∷ rest
              ; blocked = blocked env
-             ; env-inboxes = [] ∷ env-inboxes env
              ; store = newStore
-             ; fresh-name = suc (fresh-name env)
-             ; actors-valid = newActValid ∷ bindActValid ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid
+             ; env-inboxes = [] ∷ env-inboxes env
+             ; actors-valid = newActValid ∷ valid' ∷ ∀map (valid-actor-suc (name-is-fresh env)) restValid
              ; blocked-valid = ∀map (valid-actor-suc (name-is-fresh env)) (blocked-valid env)
              ; messages-valid = [] ∷ map-suc (store env) (messages-valid env) (name-is-fresh env)
+             ; fresh-name = suc (fresh-name env)
              ; name-is-fresh = newIsFresh
              }
          where
-           map-suc : (store : Store) → {store' : Store} → {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → (NameFresh store n) → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs
+           map-suc : (store : Store) → {store' : Store} {inbs : Inboxes store'} → InboxesValid store inbs → ∀ {n} → NameFresh store n → InboxesValid (inbox# n [ NewIS ] ∷ store) inbs
            map-suc store [] frsh = []
-           map-suc store (x ∷ valid) frsh = (messages-valid-suc frsh x) ∷ (map-suc store valid frsh)
--- ===== Bind send reference =====
--- Spawns a reference message and continues with (f tt).
---
--- We find where to send the mesage using lookup-reference,
--- which just traverses the index into 'pre' to find which name / pointer
--- to use from 'references'.
--- We find which name / pointer is being forwarded in the same manner
--- and stores the name together with the message.
--- The found pointer is kept as a proof that we can find the referenced inbox
--- in the store, and the pointer proof is updated whenever the store is updated.
--- Updating the proof is not doing any actual useful work,
--- but we still can't make the proof irrelevant, since we would then need to use a
--- lookup function whenever we dereference a pointer.
---
--- add-message takes a named message and a proof that the named message is valid.
---
--- Sending a message to an actor that is blocked,
--- unblocks it and moves it to the actor queue.
--- The unblocked actor is put in the back of the round-robin queue.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Send {ToIS = ToIS} canSendTo (SendM p fields) = keep-simulating (Bind (Send (name actor) (name foundTo) (reference-names namedFields))) withUnblocked
+           map-suc store (x ∷ valid) frsh = messages-valid-suc frsh x ∷ map-suc store valid frsh
+simulate env | actor ∷ rest | valid ∷ restValid | Send {ToIS = ToIS} canSendTo (SendM tag fields) ⟶ cont =
+  keep-simulating (Send (name actor) (name foundTo) (reference-names namedFields)) withUnblocked
   where
     foundTo : FoundReference (store env) ToIS
     foundTo = lookup-reference-act valid canSendTo
     namedFields = name-fields-act (store env) actor fields valid
-    bindAct : Actor
-    bindAct = replace-actorM actor ((f _) .force)
+    actor' : Actor
+    actor' = replace-actorM actor (Return _ ⟶ cont)
     withM : Env
-    withM = replace-actors env (bindAct ∷ rest) (rewrap-valid-actor valid refl refl refl ∷ restValid)
+    withM = replace-actors
+              env
+              (actor' ∷ rest)
+              ((rewrap-valid-actor valid refl refl refl) ∷ restValid)
     withUpdatedInbox : Env
-    withUpdatedInbox = update-inbox-env withM (underlying-pointer foundTo) (
-      add-message (NamedM (translate-message-pointer foundTo p) namedFields)
-                          (make-pointers-compatible (store env) (pre actor) (references actor) (pre-eq-refs actor) fields (references-have-pointer valid)))
+    withUpdatedInbox = update-inbox-env
+                         withM
+                         (underlying-pointer foundTo)
+                         (add-message
+                           (NamedM
+                             (translate-message-pointer foundTo tag)
+                             namedFields)
+                           (make-pointers-compatible
+                             (store env)
+                             (pre actor)
+                             (references actor)
+                             (pre-eq-refs actor)
+                             fields
+                             (references-have-pointer valid)))
     withUnblocked : Env
     withUnblocked = unblock-actor withUpdatedInbox (name foundTo)
--- ===== Bind receive =====
--- Receives a message and continues with (f (receivedMessage)) if there is a message in the inbox.
--- The actor is put into the blocked list if the inbox is empty.
---
--- We find the pointer to the actors inbox in the store via (actor-has-inbox valid).
--- We always remove the received message from the inbox (and do nothing if there is no message),
--- but also pattern match on what the next message is, to figure out the right behaviour:
--- * An empty inbox just moves the actor to the blocked list,
---   where it will stay until a message is sent to it.
--- * If the next message is a value, just continue with (f message)
--- * If the next message is a reference,
---   take the proof that the message is valid and use that to prove that the added reference is valid.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Receive = keep-simulating (Bind (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox)))) (env' actorsInbox)
+simulate env | actor ∷ rest | valid ∷ restValid | Receive ⟶ cont = keep-simulating (Receive (name actor) (receiveKind (GetInbox.messages actorsInbox))) (env' actorsInbox)
   where
     actorsInbox : GetInbox (store env) (inbox-shape actor)
     actorsInbox = get-inbox env (actor-has-inbox valid)
@@ -209,96 +157,61 @@ simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
     receiveKind [] = Nothing
     receiveKind (NamedM _ ps ∷ xs) = Value (reference-names ps)
     env' : GetInbox (store env) (inbox-shape actor) → Env
-    env' record { messages = [] ; valid = _ } = replace-actors+blocked env
-                                                rest restValid
-                                                (actor ∷ blocked env) (valid ∷ blocked-valid env)
-    env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vmsg } = record
-                                                                   { acts = add-references-rewrite actor (named-inboxes nm) {unname-message nm} (add-references++ nm nmv (pre actor) ) ((f (unname-message nm) .force)) ∷ rest
-                                                                   ; blocked = blocked env
-                                                                   ; env-inboxes = updated-inboxes inboxesAfter
-                                                                   ; store = store env
-                                                                   ; actors-valid = record {
-                                                                     actor-has-inbox = actor-has-inbox valid
-                                                                     ; references-have-pointer = valid++ nm nmv (references-have-pointer valid) } ∷ restValid
-                                                                   ; blocked-valid = blocked-valid env
-                                                                   ; messages-valid = inboxes-valid inboxesAfter
-                                                                   ; fresh-name = fresh-name env
-                                                                   ; name-is-fresh = name-is-fresh env
-                                                                   }
--- ===== Bind lift =====
--- To bind a lift we just perform the lifting of the actor and rewrap it in the same bind, like so:
--- ((Lift x) >>= f) ⇒ liftedX >>= f
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Strengthen {ys} {xs} inc = keep-simulating (Bind (Strengthen (name actor))) env'
+    env' record { messages = [] } = replace-actors+blocked
+                                      env
+                                      rest
+                                      restValid
+                                      (actor ∷ blocked env)
+                                      (valid ∷ blocked-valid env)
+    env' record { messages = (nm ∷ messages) ; valid = nmv ∷ vms } = record
+                                             { acts = add-references-rewrite
+                                                        actor
+                                                        (named-inboxes nm)
+                                                        {unname-message nm}
+                                                        (add-references++
+                                                          nm
+                                                          nmv
+                                                          (pre actor))
+                                                        (Return (unname-message nm) ⟶ cont)
+                                                        ∷ rest
+                                             ; blocked = blocked env
+                                             ; store = store env
+                                             ; env-inboxes = updated-inboxes inboxesAfter
+                                             ; actors-valid = record {
+                                               actor-has-inbox = actor-has-inbox valid
+                                               ; references-have-pointer = valid++
+                                                                             nm
+                                                                             nmv
+                                                                             (references-have-pointer valid) }
+                                               ∷ restValid
+                                             ; blocked-valid = blocked-valid env
+                                             ; messages-valid = inboxes-valid inboxesAfter
+                                             ; fresh-name = fresh-name env
+                                             ; name-is-fresh = name-is-fresh env
+                                             }
+simulate env | actor ∷ rest | valid ∷ restValid | Self ⟶ cont = keep-simulating (Self (name actor)) env'
   where
-    liftedRefs = lift-references inc (references actor) (pre-eq-refs actor)
-    strengthenedM : ∞ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys)
-    strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs)) = return _
-    -- liftedBx : ActorM (inbox-shape actor) B (map shape (contained liftedRefs)) postX
-    -- liftedBx rewrite (sym (contained-eq-inboxes liftedRefs)) = bx
-    bindAct : Actor
-    bindAct = lift-actor actor (contained liftedRefs) refl (strengthenedM ∞>>= f)
-    bindActValid : ValidActor (store env) bindAct
-    bindActValid = record { actor-has-inbox = actor-has-inbox valid
-                          ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) }
+    actor' : Actor
+    actor' = add-reference actor inbox# (name actor) [ (inbox-shape actor) ] (Return _ ⟶ cont)
+    valid' : ValidActor (store env) actor'
+    valid' = record {
+                  actor-has-inbox = actor-has-inbox valid
+                  ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid }
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (bindActValid ∷ restValid)
--- ===== Bind self =====
--- To bind 'self' we just need to add the actors name and type to its references / precondition.
--- We get the proof that the added reference is valid via (actor-has-inbox valid).
--- countinues with (f tt)
-simulate env | actor@(_) ∷ rest | valid ∷ restValid | m ∞>>= f |
-  Self = keep-simulating (Bind (Self (name actor))) env'
+    env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid)
+simulate env | actor ∷ rest | valid ∷ restValid | Strengthen {ys} inc ⟶ cont = keep-simulating (Strengthen (name actor)) env'
   where
-    bindAct : Actor
-    bindAct = add-reference actor (inbox# name actor [ inbox-shape actor ]) ((f _) .force)
-    bindActValid : ValidActor (store env) bindAct
-    bindActValid = record { actor-has-inbox = actor-has-inbox valid
-                          ; references-have-pointer = [p: (actor-has-inbox valid) ][handles: ⊆-refl ] ∷ references-have-pointer valid }
+    liftedRefs = lift-references inc (references actor) (pre-eq-refs actor)
+    strengthenedM : ActorM ∞ (inbox-shape actor) ⊤₁ (map shape (contained liftedRefs)) (λ _ → ys)
+    strengthenedM rewrite (sym (contained-eq-inboxes liftedRefs))= Return _
+    actor' : Actor
+    actor' = lift-actor actor (contained liftedRefs) refl (strengthenedM ⟶ cont)
+    valid' : ValidActor (store env) actor'
+    valid' = record {
+      actor-has-inbox = actor-has-inbox valid
+      ; references-have-pointer = All-⊆ (subset liftedRefs) (references-have-pointer valid) }
     env' : Env
-    env' = replace-actors env (bindAct ∷ rest) (bindActValid ∷ restValid)
--- ===== Spawn =====
--- Spawn without a following bind.
--- The current actor is finished, so we drop it using drop-top-actor.
--- The new actor is added to the top and will be moved to the bottom of the
--- round-robin queue by keep-simulating
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Spawn act₁ = keep-simulating (Spawn (name actor) (fresh-name env)) (add-top act₁ (drop-top-actor env))
--- ===== Send reference =====
--- Send reference without a following bind.
--- Very similar to send reference with a following bind,
--- but we also drop the actor that sent the value.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Send {ToIS = ToIS} canSendTo (SendM p fields) = keep-simulating (Send (name actor) (name foundTo) (reference-names namedFields)) withUnblocked
-  where
-    foundTo : FoundReference (store env) ToIS
-    foundTo = lookup-reference-act valid canSendTo
-    namedFields = name-fields-act (store env) actor fields valid
-    withUpdatedInbox : Env
-    withUpdatedInbox = update-inbox-env env
-                       (underlying-pointer foundTo)
-                       (add-message (NamedM (translate-message-pointer foundTo p) namedFields)
-                       (make-pointers-compatible (store env) (pre actor) (references actor) (pre-eq-refs actor) fields (references-have-pointer valid)))
-    withTopDropped : Env
-    withTopDropped = drop-top-actor withUpdatedInbox
-    withUnblocked : Env
-    withUnblocked = unblock-actor withTopDropped (name foundTo)
--- ===== Receive =====
--- Receive without a following bind is like return,
--- so just drop the actor.
--- We could remve the message in the inbox,
--- but there is currently no proofs that care about doing so.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Receive = keep-simulating (Receive (name actor) Dropped) (drop-top-actor env)
--- ===== Lift =====
--- Just performs the lifting by translating a subset for preconditions
--- to a subset for references.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Strengthen inc = keep-simulating (Strengthen (name actor)) (drop-top-actor env)
--- Self without a following bind is like return,
--- so just drop the actor.
-simulate env | actor@(_) ∷ rest | valid ∷ restValid |
-  Self = keep-simulating (Self (name actor)) (drop-top-actor env)
+    env' = replace-actors env (actor' ∷ rest) (valid' ∷ restValid)
 
 
 keep-simulating trace env .force = record { env = env ; trace = trace } ∷ simulate (top-actor-to-back env)
diff --git a/src/SimulationEnvironment.agda b/src/SimulationEnvironment.agda
index 15a52db..5551ee0 100644
--- a/src/SimulationEnvironment.agda
+++ b/src/SimulationEnvironment.agda
@@ -9,7 +9,7 @@ open import Data.Nat using (ℕ ; _≟_)
 open import Data.Unit using (⊤ ; tt)
 
 open import Level using (Lift ; lift)
-open import Size using (∞)
+open import Size using (Size ; ∞)
 
 open import Data.Empty using (⊥)
 open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
@@ -77,6 +77,26 @@ record _comp↦_∈_ (n : Name) (wanted : InboxShape) (store : Store) : Set₁ w
     actual-has-pointer : n ↦ actual ∈e store
     actual-handles-wanted : wanted <: actual
 
+Cont : ∀ (i : Size) (IS : InboxShape) {A B : Set₁}
+            (pre : A → TypingContext)
+            (post : B → TypingContext) →
+            Set₂
+Cont i IS {A} {B} pre post = (x : A) → ∞ActorM i IS B (pre x) post
+
+data ContStack (i : Size) (IS : InboxShape) {A : Set₁} (pre : A → TypingContext) :
+     ∀ {B : Set₁} (post : B → TypingContext) → Set₂ where
+  []    : ContStack i IS pre pre
+  _∷_   : ∀{B C}{mid : B → TypingContext} {post : C → TypingContext}
+        → Cont i IS pre mid → ContStack i IS mid post → ContStack i IS pre post
+
+record ActorState (i : Size) (IS : InboxShape) (C : Set₁) (pre : TypingContext) (post : C → TypingContext) : Set₂ where
+  constructor _⟶_
+  field
+    {A}   : Set₁
+    {mid} : A → TypingContext
+    act   : ActorM i IS A pre mid
+    cont  : ContStack i IS mid post
+
 -- An ActorM wrapped up with all of its parameters
 -- We use this to be able to store actor monads of different types in the same list.
 -- We give each actor a name so that we can find its inbox in the store.
@@ -92,7 +112,7 @@ record Actor : Set₂ where
     pre         : TypingContext
     pre-eq-refs : (map NamedInbox.shape references) ≡ pre
     post        : A → TypingContext
-    actor-m     : ActorM ∞ inbox-shape A pre post
+    computation : ActorState ∞ inbox-shape A pre post
     name        : Name
 
 named-field-content : MessageField → Set
@@ -227,7 +247,7 @@ singleton-env {IS} {A} {post} actor = record
                                   ; pre = []
                                   ; pre-eq-refs = refl
                                   ; post = post
-                                  ; actor-m = actor
+                                  ; computation = record { act = actor ; cont = [] }
                                   ; name = 0
                                   } ∷ []
                        ; blocked = []