diff --git a/README.md b/README.md
index c8d7d8c..a4ba4e4 100644
--- a/README.md
+++ b/README.md
@@ -36,8 +36,9 @@ philosophy).
 Finite state machine
 
 ```
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec binary {
   [(-i []) ok]
@@ -45,20 +46,11 @@ Finite state machine
   [(-i [1|X]) (+i X)]})
 
 'input words
-(:= e (+i []))
-(:: e binary)
-
-(:= 0 (+i [0]))
-(:: 0 binary)
-
-(:= 000 (+i [0 0 0]))
-(:: 000 binary)
-
-(:= 010 (+i [0 1 0]))
-(:: 010 binary)
-
-(:= 110 (+i [1 1 0]))
-(:: 110 binary)
+(:= e (+i []))        (:: e binary)
+(:= 0 (+i [0]))       (:: 0 binary)
+(:= 000 (+i [0 0 0])) (:: 000 binary)
+(:= 010 (+i [0 1 0])) (:: 010 binary)
+(:= 110 (+i [1 1 0])) (:: 110 binary)
 
 '''
 automaton accepting words ending with 00
@@ -77,17 +69,17 @@ automaton accepting words ending with 00
 
 (:= kill (-a _ _))
 
-<show exec { @(exec { @#e #a1 }) #kill }>
-<show exec { @(exec { @#000 #a1 }) #kill }>
-<show exec { @(exec { @#010 #a1 }) #kill }>
-<show exec { @(exec { @#110 #a1 }) #kill }>
+(show (process (interact @#e #a1)   #kill))
+(show (process (interact @#000 #a1) #kill))
+(show (process (interact @#010 #a1) #kill))
+(show (process (interact @#110 #a1) #kill))
 ```
 
 More examples can be found in `examples/`.
 
 ## Learn
 
-This project is still in (chaotic) development, hence the syntax and features
+This project is still in development, hence the syntax and features
 are still changing frequently.
 
 To learn more about the current implementation of stellogen:
diff --git a/bin/sgen.ml b/bin/sgen.ml
index 62f7c85..65d7dce 100644
--- a/bin/sgen.ml
+++ b/bin/sgen.ml
@@ -13,9 +13,19 @@ let parse input_file =
 let run input_file =
   let expr = parse input_file in
   let preprocessed = Expr.preprocess expr in
-  let p = Expr.program_of_expr preprocessed in
-  let _ = Stellogen.Sgen_eval.eval_program p in
-  ()
+  match Expr.program_of_expr preprocessed with
+  | Ok p ->
+    let _ = Stellogen.Sgen_eval.eval_program p in
+    ()
+  | Error e ->
+    let open Stellogen.Sgen_eval in
+    begin
+      match pp_err (ExprError e) with
+      | Ok pp ->
+        Out_channel.output_string Out_channel.stderr pp;
+        ()
+      | Error _ -> ()
+    end
 
 let preprocess_only input_file =
   let expr = parse input_file in
diff --git a/examples/automata.sg b/examples/automata.sg
index 8fb3e76..5bbc7f7 100644
--- a/examples/automata.sg
+++ b/examples/automata.sg
@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec binary {
   [(-i []) ok]
@@ -7,20 +8,11 @@
   [(-i [1|X]) (+i X)]})
 
 'input words
-(:= e (+i []))
-(:: e binary)
-
-(:= 0 (+i [0]))
-(:: 0 binary)
-
-(:= 000 (+i [0 0 0]))
-(:: 000 binary)
-
-(:= 010 (+i [0 1 0]))
-(:: 010 binary)
-
-(:= 110 (+i [1 1 0]))
-(:: 110 binary)
+(:= e (+i []))        (:: e binary)
+(:= 0 (+i [0]))       (:: 0 binary)
+(:= 000 (+i [0 0 0])) (:: 000 binary)
+(:= 010 (+i [0 1 0])) (:: 010 binary)
+(:= 110 (+i [1 1 0])) (:: 110 binary)
 
 (:= (initial Q) [(-i W) (+a W Q)])
 (:= (accept Q) [(-a [] Q) accept])
@@ -39,7 +31,7 @@ automaton accepting words ending with 00
 
 (:= kill (-a _ _))
 
-<show exec { @(exec { @#e #a1 }) #kill }>
-<show exec { @(exec { @#000 #a1 }) #kill }>
-<show exec { @(exec { @#010 #a1 }) #kill }>
-<show exec { @(exec { @#110 #a1 }) #kill }>
+(show (process (interact @#e #a1)   #kill))
+(show (process (interact @#000 #a1) #kill))
+(show (process (interact @#010 #a1) #kill))
+(show (process (interact @#110 #a1) #kill))
diff --git a/examples/binary4.sg b/examples/binary4.sg
index 6eab180..95077ba 100644
--- a/examples/binary4.sg
+++ b/examples/binary4.sg
@@ -1,38 +1,46 @@
-(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok])
-
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec (process #Test #Tested)) ok))
+  (== @(interact (process #Test #Tested)) ok))
+
+(spec u4 [(-b _ 1 _) (-b _ 2 _) (-b _ 3 _) (-b _ 4 _) ok])
 
 (:= (make_bin Name X1 X2 X3 X4)
   { [(+b Name 1 X1)] [(+b Name 2 X2)] [(+b Name 3 X3)] [(+b Name 4 X4)] })
 
-(:= b1 #(make_bin b1 0 0 0 1))
-(:: b1 u4)
-
-(:= b2 #(make_bin b2 0 0 1 1))
-(:: b2 u4)
+(:= b1 #(make_bin b1 0 0 0 1)) (:: b1 u4)
+(:= b2 #(make_bin b2 0 0 1 1)) (:: b2 u4)
 
 (show #b1)
 (show #b2)
 
+(:= (if A = X then R = Z) [(-b A I X) (+b R I Z)])
 (:= (if A = X and B = Y then R = Z) [(-b A I X) (-b B I Y) (+b R I Z)])
 
-'''
-'FIXME
-
-(:= (and AA BB RR) {
-  #(if AA = 0 and BB = XX then RR = 0)
-  #(if AA = 1 and BB = XX then RR = XX) })
-(show #(and b1 b2 r1))
-(show (process #b1 #(and b1 b2 r1) #b2))
+(:= (and A B R) {
+  #(if A = 0 and B = _ then R = 0)
+  #(if A = 1 and B = X then R = X) })
+(:= rand (process #b1 #(and b1 b2 r) #b2))
+(show #rand)
+(== #rand #(make_bin r 0 0 0 1))
 
 (:= (or A B R) {
-  [(-b A I 0) (-b B I X) (+b R I X)]
-  [(-b A I 1) (-b B I X) (+b R I 1)]})
-
-(:= (xor A B R) {
-  [(-b A I 1) (-b B I 0) (+b R I 1)]
-  [(-b A I 0) (-b B I 1) (+b R I 1)]
-  [(-b A I 0) (-b B I 0) (+b R I 0)]
-  [(-b A I 1) (-b B I 1) (+b R I 0)]})
+  #(if A = 0 and B = X then R = X)
+  #(if A = 1 and B = Y then R = 1) })
+(:= ror (process #b1 #(or b1 b2 r) #b2))
+(show #ror)
+(== #ror #(make_bin r 0 0 1 1))
+
+(:= (not A R) {
+  #(if A = 1 then R = 0)
+  #(if A = 0 then R = 1) })
+(:= rnot (process #b1 #(not b1 r)))
+(show #rnot)
+(== #rnot #(make_bin r 1 1 1 0))
+
+(:= rnand (process #b1 #(and b1 b2 r1) #b2 #(not r1 r2)))
+(show #rnand)
+
+'''
+(:= rxor (process #rnand #(and r2 r r3) #ror))
+(show #rxor)
 '''
diff --git a/examples/circuits.sg b/examples/circuits.sg
index 7f7ce7e..a4123cd 100644
--- a/examples/circuits.sg
+++ b/examples/circuits.sg
@@ -8,7 +8,7 @@ FIXME
   [(+not 1 0)] [(+not 0 1)]
   [(+and 1 X X)][(+and 0 X 0)]})
 
-<show exec (process
+<show interact (process
   'inputs
   [(-1 X) (+c0 X)]
   'layer 1
@@ -21,7 +21,7 @@ FIXME
   [(-c4 R) R]
   #semantics)>
 
-<show exec (process
+<show interact (process
   'inputs
   {
     [(-0 X) (+c0 X)]
diff --git a/examples/lambda.sg b/examples/lambda.sg
index c379e9a..be6679f 100644
--- a/examples/lambda.sg
+++ b/examples/lambda.sg
@@ -7,7 +7,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]})
 
-<show exec { #id #id_arg #linker }>
+(show (interact #id #id_arg #linker))
 
 ' id x
 (:= var_x [(x (exp X Y)) (+arg (exp [l|X] Y))])
@@ -16,7 +16,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]})
 
-<show exec { #id #var_x #linker }>
+(show (interact #id #var_x #linker))
 
 ' lproj x
 (:= lproj {
diff --git a/examples/linear_lambda.sg b/examples/linear_lambda.sg
index 7571cfb..f6d467c 100644
--- a/examples/linear_lambda.sg
+++ b/examples/linear_lambda.sg
@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { #Tested #Test }) ok))
+  (== @(interact #Tested #Test) ok))
 
 ' identity function (\x -> x)
 (:= id [(+id [l|X]) (+id [r|X])])
@@ -11,7 +12,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]])
 
-<show exec { #id #id_arg #linker }>
+(show (interact #id #id_arg #linker))
 
 ' id x
 (:= x_arg [(x X) (+arg [l X])])
@@ -20,7 +21,7 @@
   [(-id X) (-arg X)]
   @[(+arg [r|X]) (out X)]])
 
-<show exec { #id #x_arg #linker }>
+(show (interact #id #x_arg #linker))
 
 ' linear types
 (spec (larrow a a) {
diff --git a/examples/mall.sg b/examples/mall.sg
index c00dda6..fbcf53b 100644
--- a/examples/mall.sg
+++ b/examples/mall.sg
@@ -9,6 +9,6 @@
 
 (:= cut [(-5 X) (-3 X)])
 
-<show exec (process
+<show interact (process
   #with
   { #plus #cut })>
diff --git a/examples/mll.sg b/examples/mll.sg
index ef72d90..86c62c5 100644
--- a/examples/mll.sg
+++ b/examples/mll.sg
@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { #Tested #Test }) ok))
+  (== @(interact #Tested #Test) ok))
 
 ' test of linear identity
 (spec (larrow a a) {
@@ -42,17 +43,17 @@
   [+cuts [
     [(-7 X) (-8 X)]]]})
 
-(:= vehicle <eval exec { #ps1 @[-vehicle] }>)
-(:= cuts    <eval exec { #ps1 @[-cuts] }>)
+(:= vehicle (eval (interact #ps1 @[-vehicle])))
+(:= cuts    (eval (interact #ps1 @[-cuts])))
 
-<show exec { #vehicle #cuts }>
+(show (interact #vehicle #cuts))
 
 (spec (tens a b) {
   [(-1 [g|X]) (-2 [g|X]) (+3 [g|X])]
   @[(-3 [g|X]) ok]})
 
 (new-declaration (::lin Tested Test)
-  (== @(linexec { #Tested #Test }) ok))
+  (== @(fire #Tested #Test) ok))
 
 ' does not typecheck
 ' (::lin vehicle ((tens a a) linear))
diff --git a/examples/nat.sg b/examples/nat.sg
index bc609b7..42eaebf 100644
--- a/examples/nat.sg
+++ b/examples/nat.sg
@@ -1,18 +1,14 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec nat {
   [(-nat 0) ok]
   [(-nat (s N)) (+nat N)]})
 
-(:= 0 (+nat 0))
-(:: 0 nat)
-
-(:= 1 (+nat (s 0)))
-(:: 1 nat)
-
-(:= 2 <+nat s s 0>)
-(:: 2 nat)
+(:= 0 (+nat 0))     (:: 0 nat)
+(:= 1 (+nat (s 0))) (:: 1 nat)
+(:= 2 <+nat s s 0>) (:: 2 nat)
 
 (:= add1 [(-nat X) (+nat (s X))])
 
@@ -20,6 +16,6 @@
   [(-nat 0) (res 1)]
   [(-nat (s _)) (res 0)]})
 
-<show exec { @#add1 #2 }>
-<show exec { #is_empty @#0 }>
-<show exec { #is_empty @#1 }>
+(show (interact @#add1 #2))
+(show (interact #is_empty @#0))
+(show (interact #is_empty @#1))
diff --git a/examples/npda.sg b/examples/npda.sg
index c70855b..68652ca 100644
--- a/examples/npda.sg
+++ b/examples/npda.sg
@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec binary {
   [(-i []) ok]
@@ -7,17 +8,10 @@
   [(-i [1|X]) (+i X)]})
 
 'input words
-(:= e (+i []))
-(:: e binary)
-
-(:= 0000 (+i [0 0 0 0]))
-(:: 0000 binary)
-
-(:= 0110 (+i [0 1 1 0]))
-(:: 0110 binary)
-
-(:= 1110 (+i [1 1 1 0]))
-(:: 1110 binary)
+(:= e (+i []))           (:: e binary)
+(:= 0000 (+i [0 0 0 0])) (:: 0000 binary)
+(:= 0110 (+i [0 1 1 0])) (:: 0110 binary)
+(:= 1110 (+i [1 1 1 0])) (:: 1110 binary)
 
 (:= (initial Q) [(-i W) (+a W [] Q)])
 (:= (accept Q) [(-a [] [] Q) accept])
@@ -37,7 +31,7 @@
 
 (:= kill (-a _ _ _))
 
-<show exec { @(exec { @#e #a1 }) #kill }>
-<show exec { @(exec { @#0000 #a1 }) #kill }>
-<show exec { @(exec { @#0110 #a1 }) #kill }>
-<show exec { @(exec { @#1110 #a1 }) #kill }>
+(show (process (interact @#e #a1)    #kill))
+(show (process (interact @#0000 #a1) #kill))
+(show (process (interact @#0110 #a1) #kill))
+(show (process (interact @#1110 #a1) #kill))
diff --git a/examples/prolog.sg b/examples/prolog.sg
index 220a0a9..08b26a0 100644
--- a/examples/prolog.sg
+++ b/examples/prolog.sg
@@ -6,7 +6,7 @@
 ' 2 + 2 = R
 (:= query [(-add <s s 0> <s s 0> R) R])
 
-<show exec { #add @#query }>
+(show (interact #add @#query))
 
 (:= graph {
   [(+from 1) (+to 2)]
@@ -22,6 +22,6 @@
   @[(-from 1)]
   [(-to 4) ok]})
 
-<show exec (process
+<show interact (process
   #query
   { #graph #composition })>
diff --git a/examples/stack.sg b/examples/stack.sg
index f44d55a..856a4f8 100644
--- a/examples/stack.sg
+++ b/examples/stack.sg
@@ -1,4 +1,4 @@
-<show exec (process
+<show interact (process
   (+stack0 [])
   'push 1 then 0
   [(-stack0 X) (+stack1 [1|X])]
diff --git a/examples/sumtypes.sg b/examples/sumtypes.sg
index b8ca74a..0060d3f 100644
--- a/examples/sumtypes.sg
+++ b/examples/sumtypes.sg
@@ -1,5 +1,6 @@
+(new-declaration (spec X Y) (:= X Y))
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 
 (spec direction {
   [-north ok]
@@ -7,19 +8,15 @@
   [-west ok]
   [-east ok]})
 
-(:= n +north)
-(:: n direction)
+(:= n +north) (:: n direction)
 
-(spec result {
-  [(-ok X) ok]
-  [(-error X) ok]})
+(spec result { [(-ok X) ok] [(-error X) ok]})
 
-(:= x (+ok a))
-(:: x result)
+(:= x (+ok a)) (:: x result)
 
 'pattern matching
 (:= get_ok {
   [(-ok X) X]
   [(-error X) (+error X)]})
 
-<show exec { #get_ok @#x }>
+(show (interact #get_ok @#x))
diff --git a/examples/syntax.sg b/examples/syntax.sg
index 7687058..0299f9c 100644
--- a/examples/syntax.sg
+++ b/examples/syntax.sg
@@ -32,8 +32,8 @@
 'execution
 (:= x [(+f X) X])
 (:= y (-f a))
-(:= ex (linexec { @#x #y })) 'linear
-(:= ex (exec { @#x #y }))    'non-linear
+(:= ex (fire @#x #y)) 'linear
+(:= ex (interact @#x #y))    'non-linear
 
 'show constellation
 (show #ex)
@@ -50,7 +50,7 @@
   [(+f b)]
   @[(-f X) (-f Y) (r X Y) || (!= X Y)]})
 (show #ineq)
-<show exec #ineq>
+<show interact #ineq>
 
 'process
 (:= c (process
@@ -66,7 +66,7 @@
 (show #g)
 
 'field access and evaluation
-(:= (get G X) <<eval exec { #G @[(-field X)] }>>)
+(:= (get G X) (eval (interact #G @[(-field X)])))
 (show #(get g test1))
 (show #(get g test2))
 
@@ -74,10 +74,11 @@
 (:= g1 [
   [(+field test1) [
     [(+field test2) [(+f c) ok]]]]])
-(:= g2 <eval exec { #g1 @[(-field test1)] }>)
-<show eval exec { #g2 @[(-field test2)] }>
+(:= g2 (eval (interact #g1 @[(-field test1)])))
+<show eval (interact #g2 @[(-field test2)])>
 
 'define type
+(new-declaration (spec X Y) (:= X Y))
 (spec nat {
   [(-nat 0) ok]
   [(-nat (s N)) (+nat N)]})
@@ -89,12 +90,12 @@
 
 'type checking
 (:= 2 <+nat s s 0>)
-(== @(exec { @#2 #nat }) ok)
+(== @(interact @#2 #nat) ok)
 
 'import file
 '(use "examples/automata.sg")
 
 'declaration definition
 (new-declaration (:: Tested Test)
-  (== @(exec { @#Tested #Test }) ok))
+  (== @(interact @#Tested #Test) ok))
 (:: 2 nat)
diff --git a/examples/turing.sg b/examples/turing.sg
index 462085b..f037e90 100644
--- a/examples/turing.sg
+++ b/examples/turing.sg
@@ -29,12 +29,12 @@
   [(-m q3 L e R) (+m qr L e R)]
   [(-m qr L C R) reject]})
 
-<show exec { @(+i [a e]) #mt}>
-<show exec { @(+i [b e]) #mt}>
-<show exec { @(+i [a b b e]) #mt}>
+(show (interact @(+i [a e]) #mt))
+(show (interact @(+i [b e]) #mt))
+(show (interact @(+i [a b b e]) #mt))
 
-<show exec { @(+i [e]) #mt}>
-<show exec { @(+i [a b e]) #mt}>
-<show exec { @(+i [a a b b e]) #mt}>
-<show exec { @(+i [a b b a e]) #mt}>
-<show exec { @(+i [a b a b e]) #mt}>
+(show (interact @(+i [e]) #mt))
+(show (interact @(+i [a b e]) #mt))
+(show (interact @(+i [a a b b e]) #mt))
+(show (interact @(+i [a b b a e]) #mt))
+(show (interact @(+i [a b a b e]) #mt))
diff --git a/nvim/syntax/stellogen.vim b/nvim/syntax/stellogen.vim
index 043cf5a..afa0c07 100644
--- a/nvim/syntax/stellogen.vim
+++ b/nvim/syntax/stellogen.vim
@@ -1,6 +1,6 @@
 syn clear
 
-syn keyword sgKeyword new declaration eval slice show use exec spec linexec process
+syn keyword sgKeyword new declaration eval slice show use interact fire process
 syn match sgComment "\s*'[^'].*$"
 syn match sgId "#\%(\l\|\d\)\w*"
 syn region sgComment start="'''" end="'''" contains=NONE
diff --git a/src/expr.ml b/src/expr.ml
index 15e1051..4f8a5a3 100644
--- a/src/expr.ml
+++ b/src/expr.ml
@@ -1,6 +1,9 @@
 open Base
 open Lsc_ast
 open Sgen_ast
+open Expr_err
+
+let ( let* ) x f = Result.bind x ~f
 
 type ident = string
 
@@ -117,101 +120,152 @@ let symbol_of_str (s : string) : idfunc =
   | '-' -> (Neg, rest)
   | _ -> (Null, s)
 
-let rec ray_of_expr : expr -> ray = function
-  | Symbol s -> to_func (symbol_of_str s, [])
-  | Var "_" -> to_var ("_" ^ fresh_placeholder ())
-  | Var s -> to_var s
-  | List [] -> failwith "error: ray cannot be empty"
-  | List (Symbol h :: t) -> to_func (symbol_of_str h, List.map ~f:ray_of_expr t)
-  | List (_ :: _) as e ->
-    failwith ("error: ray " ^ to_string e ^ " must start with constant")
-
-let bans_of_expr : expr list -> ban list =
+let rec ray_of_expr : expr -> (ray, expr_err) Result.t = function
+  | Symbol s -> to_func (symbol_of_str s, []) |> Result.return
+  | Var "_" -> to_var ("_" ^ fresh_placeholder ()) |> Result.return
+  | Var s -> to_var s |> Result.return
+  | List [] -> Error EmptyRay
+  | List (Symbol h :: t) ->
+    let* args = List.map ~f:ray_of_expr t |> Result.all in
+    to_func (symbol_of_str h, args) |> Result.return
+  | List (_ :: _) as e -> Error (NonConstantRayHeader (to_string e))
+
+let bans_of_expr es : (ban list, expr_err) Result.t =
   let ban_of_expr = function
     | List [ Symbol k; a; b ] when equal_string k ineq_op ->
-      Ineq (ray_of_expr a, ray_of_expr b)
+      let* ra = ray_of_expr a in
+      let* rb = ray_of_expr b in
+      Ineq (ra, rb) |> Result.return
     | List [ Symbol k; a; b ] when equal_string k incomp_op ->
-      Incomp (ray_of_expr a, ray_of_expr b)
-    | _ -> failwith "error: invalid ban expression"
+      let* ra = ray_of_expr a in
+      let* rb = ray_of_expr b in
+      Incomp (ra, rb) |> Result.return
+    | _ as e -> Error (InvalidBan (to_string e))
   in
-  List.map ~f:ban_of_expr
+  List.map ~f:ban_of_expr es |> Result.all
 
-let rec raylist_of_expr (e : expr) : ray list =
+let rec raylist_of_expr (e : expr) : (ray list, expr_err) Result.t =
   match e with
-  | Symbol k when equal_string k nil_op -> []
-  | Symbol _ | Var _ -> [ ray_of_expr e ]
+  | Symbol k when equal_string k nil_op -> Ok []
+  | Symbol _ | Var _ ->
+    let* r = ray_of_expr e in
+    Ok [ r ]
   | List [ Symbol s; h; t ] when equal_string s cons_op ->
-    ray_of_expr h :: raylist_of_expr t
-  | e -> failwith ("error: unhandled star " ^ to_string e)
+    let* rh = ray_of_expr h in
+    let* rt = raylist_of_expr t in
+    Ok (rh :: rt)
+  | e -> Error (InvalidRaylist (to_string e))
 
-let rec star_of_expr : expr -> Marked.star = function
+let rec star_of_expr : expr -> (Marked.star, expr_err) Result.t = function
   | List [ Symbol k; s ] when equal_string k focus_op ->
-    star_of_expr s |> Marked.remove |> Marked.make_state
+    let* ss = star_of_expr s in
+    ss |> Marked.remove |> Marked.make_state |> Result.return
   | List [ Symbol k; s; List ps ] when equal_string k params_op ->
-    Action { content = raylist_of_expr s; bans = bans_of_expr ps }
-  | e -> Action { content = raylist_of_expr e; bans = [] }
-
-let rec constellation_of_expr : expr -> Marked.constellation = function
-  | Symbol s -> [ Action { content = [ var (s, None) ]; bans = [] } ]
-  | Var x -> [ Action { content = [ var (x, None) ]; bans = [] } ]
+    let* content = raylist_of_expr s in
+    let* bans = bans_of_expr ps in
+    Marked.Action { content; bans } |> Result.return
+  | e ->
+    let* content = raylist_of_expr e in
+    Marked.Action { content; bans = [] } |> Result.return
+
+let rec constellation_of_expr :
+  expr -> (Marked.constellation, expr_err) Result.t = function
+  | Symbol s ->
+    [ Marked.Action { content = [ var (s, None) ]; bans = [] } ]
+    |> Result.return
+  | Var x ->
+    [ Marked.Action { content = [ var (x, None) ]; bans = [] } ]
+    |> Result.return
   | List [ Symbol s; h; t ] when equal_string s cons_op ->
-    star_of_expr h :: constellation_of_expr t
-  | List g -> [ Action { content = [ ray_of_expr (List g) ]; bans = [] } ]
+    let* sh = star_of_expr h in
+    let* ct = constellation_of_expr t in
+    Ok (sh :: ct)
+  | List g ->
+    let* rg = ray_of_expr (List g) in
+    [ Marked.Action { content = [ rg ]; bans = [] } ] |> Result.return
 
 (* ---------------------------------------
    Stellogen expr of Expr
    --------------------------------------- *)
 
-let rec sgen_expr_of_expr (e : expr) : sgen_expr =
+let rec sgen_expr_of_expr (e : expr) : (sgen_expr, expr_err) Result.t =
   match e with
   | Symbol k when equal_string k nil_op ->
-    Raw [ Action { content = []; bans = [] } ]
+    Raw [ Action { content = []; bans = [] } ] |> Result.return
   (* ray *)
   | Var _ | Symbol _ ->
-    Raw [ Action { content = [ ray_of_expr e ]; bans = [] } ]
+    let* re = ray_of_expr e in
+    Raw [ Action { content = [ re ]; bans = [] } ] |> Result.return
   (* star *)
-  | List (Symbol s :: _) when equal_string s params_op -> Raw [ star_of_expr e ]
-  | List (Symbol s :: _) when equal_string s cons_op -> Raw [ star_of_expr e ]
+  | List (Symbol s :: _) when equal_string s params_op ->
+    let* se = star_of_expr e in
+    Raw [ se ] |> Result.return
+  | List (Symbol s :: _) when equal_string s cons_op ->
+    let* se = star_of_expr e in
+    Raw [ se ] |> Result.return
   (* id *)
-  | List [ Symbol k; g ] when equal_string k call_op -> Id (ray_of_expr g)
+  | List [ Symbol k; g ] when equal_string k call_op ->
+    let* re = ray_of_expr g in
+    Call re |> Result.return
   (* focus @ *)
   | List [ Symbol k; g ] when equal_string k focus_op ->
-    Focus (sgen_expr_of_expr g)
+    let* sgg = sgen_expr_of_expr g in
+    Focus sgg |> Result.return
   (* group *)
   | List (Symbol k :: gs) when equal_string k group_op ->
-    Group (List.map ~f:sgen_expr_of_expr gs)
+    let* sggs = List.map ~f:sgen_expr_of_expr gs |> Result.all in
+    Group sggs |> Result.return
   (* process *)
-  | List (Symbol "process" :: gs) -> Process (List.map ~f:sgen_expr_of_expr gs)
-  (* exec *)
-  | List [ Symbol "exec"; g ] -> Exec (false, sgen_expr_of_expr g)
-  (* linear exec *)
-  | List [ Symbol "linexec"; g ] -> Exec (true, sgen_expr_of_expr g)
+  | List (Symbol "process" :: gs) ->
+    let* sggs = List.map ~f:sgen_expr_of_expr gs |> Result.all in
+    Process sggs |> Result.return
+  (* interact *)
+  | List (Symbol "interact" :: gs) ->
+    let* sggs = List.map ~f:sgen_expr_of_expr gs |> Result.all in
+    Exec (false, Group sggs) |> Result.return
+  (* fire *)
+  | List (Symbol "fire" :: gs) ->
+    let* sggs = List.map ~f:sgen_expr_of_expr gs |> Result.all in
+    Exec (true, Group sggs) |> Result.return
   (* eval *)
-  | List [ Symbol "eval"; g ] -> Eval (sgen_expr_of_expr g)
+  | List [ Symbol "eval"; g ] ->
+    let* sgg = sgen_expr_of_expr g in
+    Eval sgg |> Result.return
   (* KEEP LAST -- raw constellation *)
-  | List g -> Raw (constellation_of_expr (List g))
+  | List e ->
+    let* ce = constellation_of_expr (List e) in
+    Raw ce |> Result.return
 
 (* ---------------------------------------
    Stellogen program of Expr
    --------------------------------------- *)
 
-let decl_of_expr : expr -> declaration = function
+let decl_of_expr : expr -> (declaration, expr_err) Result.t = function
   (* definition := *)
   | List [ Symbol k; x; g ] when equal_string k def_op ->
-    Def (ray_of_expr x, sgen_expr_of_expr g)
-  | List [ Symbol "spec"; x; g ] -> Def (ray_of_expr x, sgen_expr_of_expr g)
-  | List [ Symbol "exec"; x; g ] -> Def (ray_of_expr x, sgen_expr_of_expr g)
+    let* rx = ray_of_expr x in
+    let* sgg = sgen_expr_of_expr g in
+    Def (rx, sgg) |> Result.return
   (* show *)
-  | List [ Symbol "show"; g ] -> Show (sgen_expr_of_expr g)
+  | List [ Symbol "show"; g ] ->
+    let* sgg = sgen_expr_of_expr g in
+    Show sgg |> Result.return
   (* expect *)
   | List [ Symbol k; g1; g2 ] when equal_string k expect_op ->
-    Expect (sgen_expr_of_expr g1, sgen_expr_of_expr g2, const "default")
+    let* sgg1 = sgen_expr_of_expr g1 in
+    let* sgg2 = sgen_expr_of_expr g2 in
+    Expect (sgg1, sgg2, const "default") |> Result.return
   | List [ Symbol k; g1; g2; m ] when equal_string k expect_op ->
-    Expect (sgen_expr_of_expr g1, sgen_expr_of_expr g2, ray_of_expr m)
+    let* sgg1 = sgen_expr_of_expr g1 in
+    let* sgg2 = sgen_expr_of_expr g2 in
+    let* rm = ray_of_expr m in
+    Expect (sgg1, sgg2, rm) |> Result.return
   (* use *)
-  | List [ Symbol k; r ] when equal_string k "use" -> Use (ray_of_expr r)
-  | e -> failwith ("error: invalid declaration " ^ to_string e)
+  | List [ Symbol k; r ] when equal_string k "use" ->
+    let* rr = ray_of_expr r in
+    Use rr |> Result.return
+  | e -> Error (InvalidDeclaration (to_string e))
 
-let program_of_expr = List.map ~f:decl_of_expr
+let program_of_expr e = List.map ~f:decl_of_expr e |> Result.all
 
 let preprocess e = e |> List.map ~f:expand_macro |> unfold_decl_def []
diff --git a/src/expr_err.ml b/src/expr_err.ml
new file mode 100644
index 0000000..b145122
--- /dev/null
+++ b/src/expr_err.ml
@@ -0,0 +1,6 @@
+type expr_err =
+  | EmptyRay
+  | NonConstantRayHeader of string
+  | InvalidBan of string
+  | InvalidRaylist of string
+  | InvalidDeclaration of string
diff --git a/src/lsc_ast.ml b/src/lsc_ast.ml
index 6ec0500..9306d97 100644
--- a/src/lsc_ast.ml
+++ b/src/lsc_ast.ml
@@ -88,6 +88,10 @@ let is_polarised r : bool =
   let aux = function Pos, _ | Neg, _ -> true | _ -> false in
   exists_func aux r
 
+let inject i : StellarSig.idvar -> StellarSig.idvar = function
+  | x, None -> (x, Some i)
+  | x, Some i -> (x, Some i)
+
 let replace_indices (i : int) : ray -> ray =
   map Fn.id (fun (x, _) -> Var (x, Some i))
 
diff --git a/src/sgen_ast.ml b/src/sgen_ast.ml
index a92c2b1..1d5d2b9 100644
--- a/src/sgen_ast.ml
+++ b/src/sgen_ast.ml
@@ -1,5 +1,6 @@
 open Base
 open Lsc_ast
+open Expr_err
 
 type ident = StellarRays.term
 
@@ -9,7 +10,7 @@ type idfunc = polarity * string
 
 type sgen_expr =
   | Raw of Marked.constellation
-  | Id of ident
+  | Call of ident
   | Exec of bool * sgen_expr
   | Group of sgen_expr list
   | Focus of sgen_expr
@@ -19,6 +20,7 @@ type sgen_expr =
 type err =
   | ExpectError of Marked.constellation * Marked.constellation * ident
   | UnknownID of string
+  | ExprError of expr_err
 
 type env = { objs : (ident * sgen_expr) list }
 
diff --git a/src/sgen_eval.ml b/src/sgen_eval.ml
index c21c300..270226d 100644
--- a/src/sgen_eval.ml
+++ b/src/sgen_eval.ml
@@ -9,41 +9,43 @@ let ( let* ) x f = Result.bind x ~f
 
 let unifiable r r' = StellarRays.solution [ (r, r') ] |> Option.is_some
 
-let find_with_solution env x =
-  let rec aux = function
+let rec find_with_solution env x =
+  let rec aux : (ident * sgen_expr) list -> 'a option = function
     | [] -> None
-    | (key, value) :: rest -> (
-      match StellarRays.solution [ (key, x) ] with
-      | Some subst -> Some (value, subst)
-      | None -> aux rest )
+    | (key, value) :: rest ->
+      let repl_key = replace_indices 0 key in
+      let repl_value = map_ray env ~f:(replace_indices 0) value in
+      let repl_x = replace_indices 1 x in
+      begin
+        match StellarRays.solution [ (repl_key, repl_x) ] with
+        | Some subst -> Some (repl_value, subst)
+        | None -> aux rest
+      end
   in
   aux env.objs
 
-let add_obj env x e = List.Assoc.add ~equal:unifiable env.objs x e
+and add_obj env x e = List.Assoc.add ~equal:unifiable env.objs x e
 
-let get_obj env x = find_with_solution env x
+and get_obj env x : 'a option = find_with_solution env x
 
-let rec map_sgen_expr env ~f : sgen_expr -> (sgen_expr, err) Result.t = function
-  | Raw g -> Raw (f g) |> Result.return
-  | Id x -> Id x |> Result.return
+and map_ray env ~f : sgen_expr -> sgen_expr = function
+  | Raw g -> Raw (List.map ~f:(Marked.map ~f) g)
+  | Call x -> Call (f x)
   | Exec (b, e) ->
-    let* map_e = map_sgen_expr env ~f e in
-    Exec (b, map_e) |> Result.return
+    let map_e = map_ray env ~f e in
+    Exec (b, map_e)
   | Group es ->
-    let* map_es = List.map ~f:(map_sgen_expr env ~f) es |> Result.all in
-    Group map_es |> Result.return
+    let map_es = List.map ~f:(map_ray env ~f) es in
+    Group map_es
   | Focus e ->
-    let* map_e = map_sgen_expr env ~f e in
-    Focus map_e |> Result.return
+    let map_e = map_ray env ~f e in
+    Focus map_e
   | Process gs ->
-    let* procs = List.map ~f:(map_sgen_expr env ~f) gs |> Result.all in
-    Process procs |> Result.return
+    let procs = List.map ~f:(map_ray env ~f) gs in
+    Process procs
   | Eval e ->
-    let* map_e = map_sgen_expr env ~f e in
-    Eval map_e |> Result.return
-
-let subst_vars env _from _to =
-  map_sgen_expr env ~f:(subst_all_vars [ (_from, _to) ])
+    let map_e = map_ray env ~f e in
+    Eval map_e
 
 let pp_err e : (string, err) Result.t =
   let red text = "\x1b[31m" ^ text ^ "\x1b[0m" in
@@ -62,17 +64,44 @@ let pp_err e : (string, err) Result.t =
   | UnknownID x ->
     sprintf "%s: identifier '%s' not found.\n" (red "UnknownID Error") x
     |> Result.return
+  | ExprError e -> begin
+    match e with
+    | EmptyRay ->
+      sprintf "%s: rays cannot be empty.\n" (red "Expression Parsing Error")
+      |> Result.return
+    | NonConstantRayHeader e ->
+      sprintf "%s: ray '%s' must start with a constant function symbol.\n"
+        (red "Expression Parsing Error")
+        e
+      |> Result.return
+    | InvalidBan e ->
+      sprintf "%s: invalid ban expression '%s'.\n"
+        (red "Expression Parsing Error")
+        e
+      |> Result.return
+    | InvalidRaylist e ->
+      sprintf "%s: expression '%s' is not a valid star.\n"
+        (red "Expression Parsing Error")
+        e
+      |> Result.return
+    | InvalidDeclaration e ->
+      sprintf "%s: expression '%s' is not a valid declaration.\n"
+        (red "Expression Parsing Error")
+        e
+      |> Result.return
+  end
 
 let rec eval_sgen_expr (env : env) :
   sgen_expr -> (Marked.constellation, err) Result.t = function
   | Raw mcs -> Ok mcs
-  | Id x -> begin
+  | Call x -> begin
     match get_obj env x with
     | None -> Error (UnknownID (string_of_ray x))
     | Some (g, subst) ->
       let result =
         List.fold_result subst ~init:g ~f:(fun g_acc (xfrom, xto) ->
-          subst_vars env xfrom xto g_acc )
+          map_ray env ~f:(StellarRays.subst [ (xfrom, xto) ]) g_acc
+          |> Result.return )
       in
       Result.bind result ~f:(eval_sgen_expr env)
   end
@@ -102,7 +131,12 @@ let rec eval_sgen_expr (env : env) :
     match eval_e with
     | [ State { content = [ r ]; bans = _ } ]
     | [ Action { content = [ r ]; bans = _ } ] ->
-      r |> expr_of_ray |> Expr.sgen_expr_of_expr |> eval_sgen_expr env
+      let er = expr_of_ray r in
+      begin
+        match Expr.sgen_expr_of_expr er with
+        | Ok sg -> eval_sgen_expr env sg
+        | Error e -> Error (ExprError e)
+      end
     | e ->
       failwith
         ( "eval error: "
@@ -144,7 +178,7 @@ let rec eval_decl env : declaration -> (env, err) Result.t = function
            (Marked.normalize_all eval_e2)
     then Error (ExpectError (eval_e1, eval_e2, message))
     else Ok env
-  | Use path ->
+  | Use path -> (
     let open Lsc_ast.StellarRays in
     let formatted_filename : string =
       match path with
@@ -160,9 +194,11 @@ let rec eval_decl env : declaration -> (env, err) Result.t = function
     Sedlexing.set_position lexbuf (start_pos formatted_filename);
     let expr = Sgen_parsing.parse_with_error formatted_filename lexbuf in
     let preprocessed = Expr.preprocess expr in
-    let p = Expr.program_of_expr preprocessed in
-    let* env = eval_program p in
-    Ok env
+    match Expr.program_of_expr preprocessed with
+    | Ok p ->
+      let* env = eval_program p in
+      Ok env
+    | Error e -> Error (ExprError e) )
 
 and eval_program (p : program) =
   match
diff --git a/test/subjects/linear.sg b/test/subjects/linear.sg
index e44ea9b..f6a9f6d 100644
--- a/test/subjects/linear.sg
+++ b/test/subjects/linear.sg
@@ -1,14 +1,16 @@
+(new-declaration (spec X Y) (:= X Y))
+
 (:= 1 (+nat (s 0)))
 (:= 2 (+nat <s s 0>))
 (:= 3 (+nat <s s s 0>))
 
 (spec nat [(-nat (s X)) (+nat X)])
 
-(:= tested @(linexec { @#1 #nat }))
+(:= tested @(fire @#1 #nat))
 (== #tested (+nat 0))
 
-(:= tested @(linexec { @#2 #nat }))
+(:= tested @(fire @#2 #nat))
 (== #tested (+nat (s 0)))
 
-(:= tested @(linexec { @#3 #nat }))
+(:= tested @(fire @#3 #nat))
 (== #tested (+nat <s s 0>))
diff --git a/test/subjects/prolog.sg b/test/subjects/prolog.sg
index e767c8a..0793840 100644
--- a/test/subjects/prolog.sg
+++ b/test/subjects/prolog.sg
@@ -2,23 +2,23 @@
   [(+add 0 Y Y)]
   [(-add X Y Z) (+add (s X) Y (s Z))]})
 
-(:= tested (exec { #add @[(-add 0 0 R) R] }))
+(:= tested (interact { #add @[(-add 0 0 R) R] }))
 (== #tested 0)
 
-(:= tested (exec { #add @[(-add (s 0) 0 R) R] }))
+(:= tested (interact { #add @[(-add (s 0) 0 R) R] }))
 (== #tested (s 0))
 
-(:= tested (exec { #add @[(-add 0 (s 0) R) R] }))
+(:= tested (interact { #add @[(-add 0 (s 0) R) R] }))
 (== #tested (s 0))
 
-(:= tested (exec { #add @[(-add <s s 0> <s s 0> R) R] }))
+(:= tested (interact { #add @[(-add <s s 0> <s s 0> R) R] }))
 (== #tested <s s s s 0>)
 
-(:= tested (exec { #add @[(-add <s s 0> R <s s 0>) R] }))
+(:= tested (interact { #add @[(-add <s s 0> R <s s 0>) R] }))
 (== #tested 0)
 
-(:= tested (exec { #add @[(-add <s s 0> R <s s s 0>) R] }))
+(:= tested (interact { #add @[(-add <s s 0> R <s s s 0>) R] }))
 (== #tested <s 0>)
 
-(:= tested (exec { #add @[(-add <s s 0> R <s s s s 0>) R] }))
+(:= tested (interact { #add @[(-add <s s 0> R <s s s s 0>) R] }))
 (== #tested <s s 0>)
diff --git a/test/subjects/records.sg b/test/subjects/records.sg
index 0afe23a..8f0a2a7 100644
--- a/test/subjects/records.sg
+++ b/test/subjects/records.sg
@@ -5,14 +5,14 @@
     [+test22 {
       [+test3 3]}]}]})
 
-(:= x <eval exec { #g @[-test1] }>)
+(:= x <eval interact { #g @[-test1] }>)
 (== #x 1)
 
-(:= x <eval exec { #g @[-test2] }>)
-(:= y <eval exec { #x @[-test21] }>)
+(:= x <eval interact { #g @[-test2] }>)
+(:= y <eval interact { #x @[-test21] }>)
 (== #y 2)
 
-(:= x <eval exec { #g @[-test2] }>)
-(:= y <eval exec { #x @[-test22] }>)
-(:= z <eval exec { #y @[-test3] }>)
+(:= x <eval interact { #g @[-test2] }>)
+(:= y <eval interact { #x @[-test22] }>)
+(:= z <eval interact { #y @[-test3] }>)
 (== #z 3)
diff --git a/test/test.ml b/test/test.ml
index 7ff034c..0af74b3 100644
--- a/test/test.ml
+++ b/test/test.ml
@@ -4,8 +4,17 @@ let sgen filename () =
   let lexbuf = Sedlexing.Utf8.from_channel (Stdlib.open_in filename) in
   let expr = Stellogen.Sgen_parsing.parse_with_error filename lexbuf in
   let preprocessed = Stellogen.Expr.preprocess expr in
-  let p = Stellogen.Expr.program_of_expr preprocessed in
-  Stellogen.Sgen_eval.eval_program p
+  match Stellogen.Expr.program_of_expr preprocessed with
+  | Ok p -> Stellogen.Sgen_eval.eval_program p
+  | Error e ->
+    let open Stellogen.Sgen_eval in
+    begin
+      match pp_err (ExprError e) with
+      | Ok pp ->
+        Out_channel.output_string Out_channel.stderr pp;
+        Error (ExprError e)
+      | Error e -> Error e
+    end
 
 let make_ok_test name path f =
   let test got () =