diff --git a/generate-table.py b/generate-table.py
old mode 100644
new mode 100755
index 04ceb74..61b54c0
--- a/generate-table.py
+++ b/generate-table.py
@@ -3,7 +3,7 @@
 import subprocess
 from tabulate import tabulate
 
-REPETITIONS = 100
+REPETITIONS = 1000
 
 BENCHMARKS =\
     [
@@ -16,13 +16,14 @@
         ("Ping Pong", os.path.join("test", "examples", "savina", "ping_pong_strict.pat")),
         ("Thread Ring", os.path.join("test", "examples", "savina", "thread_ring.pat")),
         ("Counter", os.path.join("test", "examples", "savina", "count.pat")),
-        ("K-Fork", os.path.join("test", "examples", "savina", "kfork.pat")),
+        ("K-Fork", os.path.join("test", "examples", "savina", "lists", "kfork.pat")),
         ("Fibonacci", os.path.join("test", "examples", "savina", "fib.pat")),
-        ("Big", os.path.join("test", "examples", "savina", "big.pat")),
+        ("Big", os.path.join("test", "examples", "savina", "lists", "big.pat")),
         ("Philosopher", os.path.join("test", "examples", "savina", "philosopher.pat")),
-        ("Smokers", os.path.join("test", "examples", "savina", "cig_smok.pat")),
+        ("Smokers", os.path.join("test", "examples", "savina", "lists", "cig_smok.pat")),
         ("Log Map", os.path.join("test", "examples", "savina", "log_map.pat")),
-        ("Transaction", os.path.join("test", "examples", "savina", "banking.pat"))
+        ("Transaction", os.path.join("test", "examples", "savina", "lists", "banking.pat")),
+	("Barber", os.path.join("test", "examples", "savina", "lists", "barber.pat")),
      ]
 
 # Tries to run in strict mode -- returns True if it works, False otherwise
diff --git a/lib/common/ir.ml b/lib/common/ir.ml
index c659c71..63b59ce 100644
--- a/lib/common/ir.ml
+++ b/lib/common/ir.ml
@@ -97,6 +97,12 @@ and comp_node =
         branch1: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp;
         branch2: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp
     }
+    | CaseL of {
+        term: value;
+        ty: (Type.t[@name "ty"]);
+        nil: comp;
+        cons: ((Binder.t[@name "binder"]) * (Binder.t[@name "binder"])) * comp
+    }
     | New of string
     | Spawn of comp
     | Send of {
@@ -119,6 +125,8 @@ and value_node =
     | Primitive of primitive_name
     | Variable of (Var.t[@name "var"]) * (Pretype.t[@name "pretype"]) option
     | Tuple of value list
+    | Nil
+    | Cons of value * value
     | Inl of value
     | Inr of value
     | Lam of {
@@ -189,6 +197,16 @@ and pp_branch name ppf ((bnd, ty), c) =
         Binder.pp bnd
         Type.pp ty
         pp_comp c
+and pp_nil name ppf c =
+  fprintf ppf "%s([]) -> @[<v>%a@]"
+    name
+    pp_comp c
+and pp_cons name ppf ((bnd1, bnd2), c) =
+    fprintf ppf "%s(%a :: %a) -> @[<v>%a@]"
+        name
+        Binder.pp bnd1
+        Binder.pp bnd2
+        pp_comp c
 (* Expressions *)
 and pp_comp ppf comp_with_pos =
     let comp_node = WithPos.node comp_with_pos in
@@ -242,6 +260,13 @@ and pp_comp ppf comp_with_pos =
             pp_value term
             (pp_branch "inl") branch1
             (pp_branch "inr") branch2
+    | CaseL { term; ty; nil; cons } ->
+        fprintf ppf
+            "caseL %a: %a of {@[<v>@[<v>%a@]@,@[<v>%a@]@]}"
+            pp_value term
+            Type.pp ty
+            (pp_nil "nil") nil
+            (pp_cons "cons") cons
     | Guard { target; pattern; guards; _ } ->
         fprintf ppf
             "guard %a : %a {@,@[<v 2>  %a@]@,}"
@@ -260,6 +285,9 @@ and pp_value ppf v =
     | Constant c -> Constant.pp ppf c
     | Tuple vs ->
         fprintf ppf "%a" (pp_print_comma_list pp_value) vs
+    | Nil -> Format.pp_print_string ppf "Nil"
+    | Cons (v1, v2) ->
+        fprintf ppf "%a :: %a" pp_value v1 pp_value v2
     | Inl v -> fprintf ppf "inl(%a)" pp_value v
     | Inr v -> fprintf ppf "inr(%a)" pp_value v
     | Lam { linear; parameters; result_type; body } ->
@@ -269,7 +297,7 @@ and pp_value ppf v =
             (pp_print_comma_list pp_param) parameters
             Type.pp result_type
             pp_comp body
-and pp_guard ppf guard_with_pos = 
+and pp_guard ppf guard_with_pos =
     let guard_node = WithPos.node guard_with_pos in
     match guard_node with
     | Receive { tag; payload_binders; mailbox_binder; cont } ->
@@ -293,7 +321,7 @@ let is_free_guard = function
     | Free _ -> true
     | _ -> false
 
-let is_fail_guard guard = 
+let is_fail_guard guard =
     match WithPos.node guard with
     | Fail -> true
     | _ -> false
@@ -312,4 +340,3 @@ let substitute_solution sol =
         end
     in
     visitor#visit_program ()
-
diff --git a/lib/common/pretype.ml b/lib/common/pretype.ml
index 16d5af8..976d354 100644
--- a/lib/common/pretype.ml
+++ b/lib/common/pretype.ml
@@ -13,6 +13,7 @@ type t =
     | PInterface of string
     | PSum of (t * t)
     | PTuple of t list
+    | PList of t
     [@@name "pretype"]
     [@@deriving visitors { variety = "map" }]
 and base = [%import: Common_types.Base.t]
@@ -38,6 +39,9 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
+    | PList t ->
+        Format.fprintf ppf "List(%a)"
+            pp t
     | PInterface name -> ps name
 
 let show t =
@@ -51,6 +55,7 @@ let rec of_type = function
         PFun { linear; args; result = result }
     | Type.Tuple ts -> PTuple (List.map of_type ts)
     | Type.Sum (t1, t2) -> PSum (of_type t1, of_type t2)
+    | Type.List t -> PList (of_type t)
     | Type.Mailbox { interface; _ } -> PInterface interface
 
 (* As long as a pretype isn't a mailbox type, and isn't a function
@@ -75,4 +80,10 @@ let rec to_type = function
                 | Some ty1, Some ty2 -> Some (Type.Sum (ty1, ty2))
                 | _, _ -> None
         end
+    | PList t ->
+        begin
+        match to_type t with
+            | Some t -> Some (Type.List t)
+            | _ -> None
+        end
     | PInterface _ -> None
diff --git a/lib/common/sugar_ast.ml b/lib/common/sugar_ast.ml
index ebd1d1a..35c6619 100644
--- a/lib/common/sugar_ast.ml
+++ b/lib/common/sugar_ast.ml
@@ -39,6 +39,15 @@ and expr_node =
         term: expr;
         cont: expr
     }
+    (* Lists *)
+    | Nil
+    | Cons of (expr * expr)
+    | CaseL of {
+        term: expr;
+        ty: (Type.t[@name "ty"]);
+        nil: expr;
+        cons: (sugar_binder * sugar_binder) * expr
+    }
     (* Sums *)
     | Inl of expr
     | Inr of expr
@@ -238,6 +247,23 @@ and pp_expr ppf expr_with_pos =
             (pp_print_comma_list Type.pp) ts
             pp_expr term
             pp_expr cont
+    | Nil -> pp_print_string ppf "nil"
+    | Cons (e1, e2) ->
+        fprintf ppf "cons %a %a" pp_expr e1 pp_expr e2
+    | CaseL { term; ty = t1; nil = e1; cons = ((b1, b2), e2) } -> begin
+      match t1 with
+        | List t ->
+	          fprintf
+            ppf
+            "caseL %a : %a of {@[@[nil -> @[%a@]@]@]@[cons %a %a -> @[%a@]@]@]}"
+            pp_expr term
+            Type.pp t1
+            pp_expr e1
+            pp_bnd_ann (b1, t)
+            pp_bnd_ann (b2, t1)
+            pp_expr e2
+        | _ -> fprintf ppf "bad list"
+      end
     | Guard { target; pattern; guards; _ } ->
         fprintf ppf
             "guard %a : %a {@,@[<v 2>  %a@]@,}"
@@ -246,7 +272,7 @@ and pp_expr ppf expr_with_pos =
             (pp_print_newline_list pp_guard) guards
     | Free e -> fprintf ppf "free(%a)" pp_expr e
     | SugarFail (e, ty) -> fprintf ppf "fail(%a)[%a]" pp_expr e Type.pp ty
-and pp_guard ppf guard_with_node = 
+and pp_guard ppf guard_with_node =
     let guard_node = WithPos.node guard_with_node in
     match guard_node with
     | Receive { tag; payload_binders; mailbox_binder; cont } ->
@@ -255,12 +281,12 @@ and pp_guard ppf guard_with_node =
             (pp_print_comma_list pp_print_string) payload_binders
             mailbox_binder
             pp_expr cont
-    (* 
+    (*
        free -> M
        can be treated as syntactic sugar for
        empty(x) -> free(x); M
     *)
-    | GFree e -> 
+    | GFree e ->
         fprintf ppf "free ->@,  @[<v>%a@]" pp_expr e
     | Empty (x, e) ->
         fprintf ppf "empty(%s) ->@,  @[<v>%a@]" x pp_expr e
@@ -284,4 +310,3 @@ let substitute_solution sol =
         end
     in
     visitor#visit_program ()
-
diff --git a/lib/common/type.ml b/lib/common/type.ml
index 7e5097f..f11c787 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -27,9 +27,10 @@ module Quasilinearity = struct
        to be returnable.
      *)
     let is_sub x1 x2 =
-        match x1, x2 with
-            | Returnable, Usable -> true
-            | x1, x2 -> x1 = x2
+        (Settings.(get disable_quasilinearity)) ||
+            match x1, x2 with
+                | Returnable, Usable -> true
+                | x1, x2 -> x1 = x2
 
     let max ql1 ql2 =
         if ql1 = Returnable || ql2 = Returnable then
@@ -253,6 +254,7 @@ type t =
     | Fun of { linear: bool; args: t list; result: t }
     | Tuple of t list
     | Sum of (t * t)
+    | List of t
     | Mailbox of {
         capability: (Capability.t [@name "capability"]);
         interface: string;
@@ -288,6 +290,7 @@ let rec contains_mailbox_type = function
     | Mailbox _ -> true
     | Sum (t1, t2) -> contains_mailbox_type t1 || contains_mailbox_type t2
     | Tuple ts -> List.exists contains_mailbox_type ts
+    | List t -> contains_mailbox_type t
     | _ -> false
 
 (* Easy constructors *)
@@ -325,6 +328,9 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
+    | List t ->
+        fprintf ppf "List(%a)"
+            pp t
     | Mailbox { capability; interface; pattern; quasilinearity } ->
         let ql =
             match quasilinearity with
@@ -358,6 +364,7 @@ let rec is_lin = function
     | Mailbox { capability = Out; pattern = Some One; _ } -> false
     | Tuple ts -> List.exists is_lin ts
     | Sum (t1, t2) -> is_lin t1 || is_lin t2
+    | List t -> is_lin t
     (* ...but otherwise a mailbox type must be used linearly. *)
     | Mailbox _ -> true
 
@@ -369,6 +376,13 @@ let is_output_mailbox = function
     | Mailbox { capability = Out; pattern = Some _; _ } -> true
     | _ -> false
 
+let rec contains_output_mailbox = function
+    | Mailbox { capability = Out; pattern = Some _; _} -> true
+    | Sum (t1, t2) -> contains_output_mailbox t1 || contains_output_mailbox t2
+    | Tuple ts -> List.exists contains_output_mailbox ts
+    | List t -> contains_output_mailbox t
+    | _ -> false
+
 let is_tuple = function
     | Tuple _ -> true
     | _ -> false
@@ -377,6 +391,10 @@ let is_sum = function
     | Sum _ -> true
     | _ -> false
 
+let is_list = function
+  | List _ -> true
+  | _ -> false
+
 let get_pattern = function
     | Mailbox { pattern = Some pat; _ } -> pat
     | _ -> raise (Errors.internal_error "type.ml" "attempted to get pattern of non-mailbox type")
@@ -394,21 +412,20 @@ let rec make_usable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Usable }
     | Tuple ts -> Tuple (List.map make_usable ts)
     | Sum (t1, t2) -> Sum (make_usable t1, make_usable t2)
+    | List t -> List (make_usable t)
     | t -> t
 
-let rec make_returnable = function
+(* Tuples, sums, and lists can all be returnable even if they contain things that are not returnable,
+   as long as we are careful to avoid aliasing when deconstructing the value. *)
+let make_returnable = function
     | Mailbox m -> Mailbox { m with quasilinearity = Quasilinearity.Returnable }
-    | Tuple ts -> Tuple (List.map make_returnable ts) 
-    | Sum (t1, t2) -> Sum (make_returnable t1, make_returnable t2)
     | t -> t
 
 let is_unr = is_lin >> not
 
-let rec is_returnable = function
+let is_returnable = function
     | Mailbox { quasilinearity = ql; _ } ->
         ql = Quasilinearity.Returnable
-    | Tuple ts -> List.for_all is_returnable ts
-    | Sum  (t1, t2) -> is_returnable t1 && is_returnable t2
     | _ -> true
 
 let make_function_type linear args result =
@@ -420,3 +437,4 @@ let make_tuple_type tys =
 let make_sum_type ty1 ty2 =
     Sum (make_returnable ty1, make_returnable ty2)
 
+let make_list_type ty = List ty
diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index a18f9d6..cb1a3bf 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -22,6 +22,8 @@ let rec annotate_type =
             Tuple (List.map annotate_type ts)
         | Sum (t1, t2) ->
             Sum (annotate_type t1, annotate_type t2)
+        | List t ->
+            List (annotate_type t)
         | Mailbox { pattern = Some _; _ } as mb -> mb
         | Mailbox { capability; interface; pattern = None; quasilinearity } ->
             Mailbox {
@@ -31,7 +33,7 @@ let rec annotate_type =
                 quasilinearity
             }
 
-let annotate_interface_type = 
+let annotate_interface_type =
     let open Type in
     function
         (* Outermost MB types (i.e., payloads) are treated as usable. *)
@@ -80,6 +82,42 @@ let visitor =
                 let new_body = self#visit_expr env body in
                 let new_lam = Lam { linear; parameters; result_type; body = new_body } in
                 { expr_with_pos with node = new_lam }
+            | Let { annot = Some ty; binder; term; body } ->
+                let ty = annotate_type ty in
+                let term = self#visit_expr env term in
+                let body = self#visit_expr env body in
+                let new_let = Let { annot = Some ty; binder; term; body } in
+                { expr_with_pos with node = new_let }
+            | LetTuple { annot = Some tys; binders; term; cont } ->
+                let tys = List.map annotate_type tys in
+                let term = self#visit_expr env term in
+                let cont = self#visit_expr env cont in
+                let new_let = LetTuple { annot = Some tys; binders; term; cont } in
+                { expr_with_pos with node = new_let }
+            | Case { term; branch1 = ((bnd1, ty1), e1); branch2 = ((bnd2, ty2), e2) } ->
+                let term = self#visit_expr env term in
+                let ty1 = annotate_type ty1 in
+                let ty2 = annotate_type ty2 in
+                let e1 = self#visit_expr env e1 in
+                let e2 = self#visit_expr env e2 in
+                let new_case = Case {
+                    term; branch1 = ((bnd1, ty1), e1); branch2 = ((bnd2, ty2), e2) }
+                in
+                { expr_with_pos with node = new_case }
+            | CaseL { term; ty = ty1; nil = nil_cont; cons = ((x_bnd, xs_bnd), cons_cont)} ->
+                let term = self#visit_expr env term in
+                let ty_ann = annotate_type ty1 in
+                let nil_cont = self#visit_expr env nil_cont in
+                let cons_cont = self#visit_expr env cons_cont in
+                let new_case =
+                    CaseL {
+                        term;
+                        ty = ty_ann;
+                        nil = nil_cont;
+                        cons = ((x_bnd, xs_bnd), cons_cont)
+                    }
+                in
+                { expr_with_pos with node = new_case }
             | _ -> super#visit_expr env expr_with_pos
 
         method! visit_program env p =
@@ -103,4 +141,3 @@ let annotate prog =
         Format.(fprintf std_formatter "=== Annotated Program ===\n%a\n\n"
         Sugar_ast.pp_program prog));
     prog
-
diff --git a/lib/frontend/lexer.mll b/lib/frontend/lexer.mll
index 2f3a4d9..d06edff 100644
--- a/lib/frontend/lexer.mll
+++ b/lib/frontend/lexer.mll
@@ -45,9 +45,12 @@ let keywords = [
     "if", IF;
     "else", ELSE;
     "case", CASE;
+    "caseL", CASEL;
     "of", OF;
     "inl", INL;
-    "inr", INR
+    "inr", INR;
+    "nil", NIL;
+    "List", LIST
 ]
 }
 
@@ -108,6 +111,7 @@ rule read =
     | "!="     { add_to_source_code lexbuf; NEQ }
     | "->"     { add_to_source_code lexbuf; RIGHTARROW }
     | "-o"     { add_to_source_code lexbuf; LOLLI }
+    | "::"     { add_to_source_code lexbuf; CONS }
     | _ { raise (SyntaxError ("Unexpected char: " ^ Lexing.lexeme lexbuf)) }
     | eof      { EOF }
 and read_string buf =
diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly
index 8971b26..5f41aee 100644
--- a/lib/frontend/parser.mly
+++ b/lib/frontend/parser.mly
@@ -16,7 +16,7 @@ module ParserPosition
     (* parser position produced by Menhir *)
     type t = Lexpos.t * Lexpos.t
     (* Convert position produced by a parser to SourceCode position *)
-    let pos (start, finish) = 
+    let pos (start, finish) =
         let code = get_instance () in
         Position.make ~start ~finish ~code:code
     (* Wrapper around SourceCode.WithPos.make.  Accepts parser positions. *)
@@ -93,6 +93,10 @@ These will be added in later
 %token AND
 %token OR
 %token CASE
+%token CASEL
+%token LIST
+%token NIL
+%token CONS
 %token OF
 %token INL
 %token INR
@@ -125,6 +129,12 @@ inl_branch:
 inr_branch:
     | INR LEFT_PAREN VARIABLE RIGHT_PAREN type_annot RIGHTARROW expr { (($3, $5), $7) }
 
+nil_branch:
+    | NIL RIGHTARROW expr { $3 }
+
+cons_branch:
+    | LEFT_PAREN VARIABLE CONS VARIABLE RIGHT_PAREN RIGHTARROW expr { (($2, $4), $7) }
+
 expr:
     (* Let *)
     | LET VARIABLE type_annot? EQ expr IN expr
@@ -152,6 +162,8 @@ basic_expr:
     | INR LEFT_PAREN expr RIGHT_PAREN { with_pos_from_positions $startpos $endpos ( Inr $3 )}
     | CASE expr OF LEFT_BRACE inl_branch PIPE inr_branch RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Case { term = $2; branch1 = $5; branch2 = $7} )}
+    | CASEL basic_expr type_annot OF LEFT_BRACE nil_branch PIPE cons_branch RIGHT_BRACE
+        { with_pos_from_positions $startpos $endpos ( CaseL { term = $2; ty = $3; nil = $6; cons = $8} )}
     (* New *)
     | NEW LEFT_BRACK interface_name RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( New $3 )}
     (* Spawn *)
@@ -161,21 +173,23 @@ basic_expr:
     (* Sugared Fail forms *)
     | FAIL LEFT_PAREN expr RIGHT_PAREN LEFT_BRACK ty RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( SugarFail ($3, $6))}
     | tuple_exprs { with_pos_from_positions $startpos $endpos ( Tuple $1 ) }
+    | NIL { with_pos_from_positions $startpos $endpos ( Nil ) }
+    | LEFT_PAREN expr CONS expr RIGHT_PAREN { with_pos_from_positions $startpos $endpos ( Cons ($2, $4) ) }
     (* App *)
     | fact LEFT_PAREN expr_list RIGHT_PAREN
         { with_pos_from_positions $startpos $endpos (
             App {   func = with_pos_from_positions $startpos $endpos ($1);
-                    args = $3 } 
+                    args = $3 }
         )}
     (* Lam *)
     | linearity LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Lam { linear = $1; parameters = $3; result_type = $6; body = $8 } )}
     (* Send *)
-    | fact BANG message 
-        { with_pos_from_positions $startpos $endpos( 
-            Send {  target = with_pos_from_positions $startpos $endpos ($1); 
-                    message = $3; 
-                    iname = None 
+    | fact BANG message
+        { with_pos_from_positions $startpos $endpos(
+            Send {  target = with_pos_from_positions $startpos $endpos ($1);
+                    message = $3;
+                    iname = None
             }
         )}
     (* If-Then-Else *)
@@ -255,6 +269,7 @@ ty:
     | parenthesised_datatypes LOLLI simple_ty       { Type.Fun { linear = true;  args = $1; result = $3} }
     | LEFT_PAREN simple_ty PLUS simple_ty RIGHT_PAREN { Type.make_sum_type $2 $4 }
     | tuple_annotation { Type.make_tuple_type $1 }
+    | LIST LEFT_PAREN simple_ty RIGHT_PAREN { Type.make_list_type $3 }
     | simple_ty { $1 }
 
 interface_name:
@@ -275,7 +290,7 @@ simple_pat:
             match $1 with
                 | 0 -> Type.Pattern.Zero
                 | 1 -> Type.Pattern.One
-                | _ -> raise (parse_error "Invalid pattern: expected 0 or 1." 
+                | _ -> raise (parse_error "Invalid pattern: expected 0 or 1."
                                 [Position.make ~start:$startpos ~finish:$endpos ~code:!source_code_instance])
         }
     | LEFT_PAREN pat RIGHT_PAREN { $2 }
@@ -285,7 +300,7 @@ ql:
         match $2 with
             | "R" -> Type.Quasilinearity.Returnable
             | "U" -> Type.Quasilinearity.Usable
-            | _ -> raise (parse_error "Invalid usage: expected U or R." 
+            | _ -> raise (parse_error "Invalid usage: expected U or R."
                             [Position.make ~start:$startpos ~finish:$endpos ~code:!source_code_instance])
     }
 
@@ -342,13 +357,13 @@ annotated_var_list:
     | separated_list(COMMA, annotated_var)  { $1 }
 
 interface:
-    | INTERFACE interface_name LEFT_BRACE message_list RIGHT_BRACE 
+    | INTERFACE interface_name LEFT_BRACE message_list RIGHT_BRACE
         { with_pos_from_positions $startpos $endpos ( Interface.make $2 $4)  }
 
 decl:
     | DEF VARIABLE LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr
     RIGHT_BRACE {
-        with_pos_from_positions $startpos $endpos ( 
+        with_pos_from_positions $startpos $endpos (
         {
           decl_name = $2;
           decl_parameters = $4;
diff --git a/lib/frontend/sugar_to_ir.ml b/lib/frontend/sugar_to_ir.ml
index 38e31a4..8c324f8 100644
--- a/lib/frontend/sugar_to_ir.ml
+++ b/lib/frontend/sugar_to_ir.ml
@@ -55,7 +55,7 @@ let rec transform_prog :
     let (bnds, env') = add_names env (fun d -> d.Sugar_ast.decl_name) nodes in
     {
         prog_interfaces;
-        prog_decls = WithPos.combine_with_pos_list poses 
+        prog_decls = WithPos.combine_with_pos_list poses
                     (List.map (fun (b, d) -> transform_decl env' d b id) (List.combine bnds nodes));
         prog_body =
             match prog_body with
@@ -139,6 +139,11 @@ and transform_expr :
         | Tuple es ->
             transform_exprs env es (fun _ vs ->
                 with_same_pos (Ir.Return (with_same_pos (Ir.Tuple vs))) |> k env)
+        | Nil -> with_same_pos (Ir.Return (with_same_pos (Ir.Nil))) |> k env
+        | Cons (e1, e2) ->
+            transform_subterm env e1 (fun _ v1 ->
+            transform_subterm env e2 (fun _ v2 ->
+                with_same_pos (Ir.Return (with_same_pos (Ir.Cons (v1, v2)))) |> k env))
         | LetTuple {binders = bs; term; cont; _ } ->
             (* let x = M in N*)
             (* Create IR variables based on the binders *)
@@ -168,6 +173,21 @@ and transform_expr :
                     branch1 = (ir_bnd1, ty1), (transform_expr env1 comp1 id);
                     branch2 = (ir_bnd2, ty2), (transform_expr env2 comp2 id);
                 }) |> k env)
+        | CaseL {
+            term;
+            ty = ty1;
+            nil = comp1;
+            cons = ((bnd1, bnd2), comp2) } ->
+            transform_subterm env term (fun env v ->
+                let (ir_bnd1, env1) = add_name env bnd1 in
+                let (ir_bnd2, env2) = add_name env1 bnd2 in
+                with_same_pos (
+                Ir.CaseL {
+                    term = v;
+                    ty = ty1;
+                    nil = (transform_expr env comp1 id);
+                    cons = (ir_bnd1, ir_bnd2), (transform_expr env2 comp2 id);
+                }) |> k env)
         | Seq (e1, e2) ->
             transform_expr env e1 (fun env c1 ->
             let pos' = WithPos.pos c1 in
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 5c9a344..9e4abee 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -106,7 +106,7 @@ let rec synthesise_val :
                     (* Finally, ensure that the declared type is a subtype of
                        the inferred type *)
                     List.fold_left (fun acc (inferred, declared) ->
-                        Constraint_set.union acc (subtype ienv declared inferred pos)) 
+                        Constraint_set.union acc (subtype ienv declared inferred pos))
                         Constraint_set.empty
                         zipped
                 in
@@ -158,6 +158,8 @@ and check_val :
             | Sum (t1, t2), PSum (pt1, pt2) ->
                 check_pretype_consistency t1 pt1;
                 check_pretype_consistency t2 pt2
+            | List t, PList pt ->
+                check_pretype_consistency t pt
             | _, _ -> Gripers.pretype_consistency ty pty [pos]
     in
     match WithPos.node v with
@@ -182,6 +184,22 @@ and check_val :
                         check_val ienv decl_env v (Type.make_returnable t2)
                     | _ -> Gripers.expected_sum_type ty [pos]
             end
+        | Nil ->
+            begin
+                match ty with
+                    | Type.List _ -> Ty_env.empty, Constraint_set.empty
+                    | _ -> Gripers.expected_list_type ty [pos]
+            end
+        | Cons (v1, v2) ->
+            begin
+                match ty with
+                    | Type.List t ->
+                        let (env1, constrs1) = check_val ienv decl_env v1 t in
+                        let (env2, constrs2) = check_val ienv decl_env v2 ty in
+                        let env, constrs3 = Ty_env.combine ienv env1 env2 pos in
+                        env, Constraint_set.union_many [constrs1; constrs2; constrs3]
+                    | _ -> Gripers.expected_list_type ty [pos]
+            end
         | Tuple vs ->
             let ts =
                 begin
@@ -351,7 +369,7 @@ and synthesise_comp :
                         in
                         let () =
                             if Type.is_lin binder_ty then
-                                Gripers.unused_synthesised_linear_var 
+                                Gripers.unused_synthesised_linear_var
                                 binder_var binder_ty [pos]
                         in
                         let (env, env_constrs) =
@@ -431,6 +449,54 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
                       env2_constrs; isect_constrs; env_constrs; term_constrs ]
             in
             (env, constrs)
+        | CaseL { term; ty = ty1; nil = comp1; cons = ((bnd1, bnd2), comp2) } ->
+            let elem_ty =
+                match ty1 with
+                    | Type.List elem_ty -> elem_ty
+                    | _ -> Gripers.expected_list_type ty1 [pos]
+            in
+            (* Check that scrutinee has annotated list type *)
+            let (term_env, term_constrs) =
+                check_val ienv decl_env term ty1
+            in
+            (* Next, check that comp1 (nil case) has expected return type *)
+            let (comp1_env, comp1_constrs) = chk comp1 ty in
+            (* Next, check that comp2 (cons case) has expected return type *)
+            let (comp2_env, comp2_constrs) = chk comp2 ty in
+            (* Next, check that the inferred types in comp2_env match annotations and that
+               the cons case doesn't contain any troublesome mailbox variables that could 
+               introduce unsafe aliasing *)
+            let var1 = Var.of_binder bnd1 in
+            let var2 = Var.of_binder bnd2 in 
+            let comp2_env_no_binders = Ty_env.delete_many [var1; var2] comp2_env in
+            (* If element type is returnable, we know it's the last lexical occurrence 
+               and we don't need this check. *)
+            let () =
+                if (not (Type.is_returnable elem_ty)) then
+                    Ty_env.check_free_mailbox_variables [elem_ty] comp2_env_no_binders
+            in
+            let env_constrs =
+                Constraint_set.union
+                    (Ty_env.check_type ienv var1 elem_ty comp2_env pos)
+                    (Ty_env.check_type ienv var2 ty1 comp2_env pos)
+            in
+            (* Calculate merge of the branches (sans binders) *)
+            let isect_env, isect_constrs =
+                Ty_env.intersect
+                  comp1_env
+                  comp2_env_no_binders
+                  pos
+            in
+            (* Finally combine the term env with the intersected env *)
+            let env, combine_constrs =
+                Ty_env.combine ienv term_env isect_env pos
+            in
+            let constrs =
+                Constraint_set.union_many
+                    [ comp1_constrs; comp2_constrs; env_constrs;
+                      combine_constrs; isect_constrs; term_constrs ]
+            in
+            (env, constrs)
         | Seq (e1, e2) ->
             (* Check e1 has type unit, check body type *)
             let (e1_env, e1_constrs) = chk e1 Type.unit_type in
@@ -759,47 +825,7 @@ and check_guard :
                   List.fold_right (Ty_env.delete_binder) payload_binders env
                   |> Ty_env.delete_binder mailbox_binder
                 in
-                (* If we are receiving a mailbox variable, without a dependency
-                   graph, we must do some fairly coarse-grained aliasing
-                   control.
-                   There are three strategies:
-                      1. Strict: the environment must be entirely unrestricted
-                          (i.e., no other mailbox variables are free in the receive
-                          block)
-
-                      2. Interface: the environment cannot contain a variable of
-                          the same interface. This means that we know we won't
-                          accidentally alias, without being overly restrictive.
-
-                      3. Nothing: No alias control: permissive, but unsafe.
-                  *)
-                let () =
-                    let mb_iface_tys =
-                        List.filter_map (fun ty ->
-                            if Type.is_mailbox_type ty then
-                                Some (Type.get_interface ty)
-                            else None)
-                        payload_iface_tys
-                    in
-                    let open Settings in
-                    let open ReceiveTypingStrategy in
-                    match get receive_typing_strategy with
-                        | Strict ->
-                            Ty_env.iter (fun v ty ->
-                                if Type.is_lin ty then
-                                    Gripers.unrestricted_recv_env v ty [pos]
-                            ) env
-                        | Interface ->
-                            Ty_env.iter (fun v ty ->
-                                match ty with
-                                    | Mailbox { interface; _ } when (List.mem interface mb_iface_tys) ->
-                                        Gripers.duplicate_interface_receive_env
-                                        v interface 
-                                        [pos]
-                                    | _ -> ()
-                            ) env
-                        | Nothing -> ()
-                in
+                Ty_env.check_free_mailbox_variables payload_iface_tys env;
                 (* Calculate the derivative wrt. the tag, and ensure via a
                    constraint that it is included in the calculated payload
                    type. *)
@@ -889,7 +915,8 @@ let check_decls ienv decls =
        arguments removed), along with generated constraints. *)
     let check_decl d pos =
         let (env, body_constrs) =
-            check_comp ienv decl_env d.decl_body d.decl_return_type in
+            check_comp ienv decl_env d.decl_body d.decl_return_type
+        in
         (* Check arguments; remove from environment *)
         let (env, arg_constrs) =
             (* Each inferred argument type should be a subtype of the
diff --git a/lib/typecheck/gripers.ml b/lib/typecheck/gripers.ml
index 572fad6..21e4d3a 100644
--- a/lib/typecheck/gripers.ml
+++ b/lib/typecheck/gripers.ml
@@ -134,7 +134,7 @@ let unused_parameter v fn_name ty pos_list =
             v fn_name Type.pp ty
     in
     raise (constraint_gen_error ~subsystem:(Errors.GenCheckDecls) msg pos_list )
-   
+
 
 let subtype_linearity_mismatch t1 t2 pos_list =
     let msg =
@@ -228,7 +228,7 @@ let guard_send_return_type ty pos_list =
 let unrestricted_recv_env var ty pos_list =
     let msg =
         Format.asprintf
-            "The body of a receive guard cannot contain free linear capabilities, but variable %a has type %a."
+            "The body of a receive guard or case expression cannot contain free mailbox variables, but variable %a has type %a."
             Ir.Var.pp_name var Type.pp ty
     in
     raise (constraint_gen_error ~subsystem:Errors.GenCheckGuard msg pos_list)
@@ -266,6 +266,14 @@ let expected_sum_type instead pos_list =
     in
     raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
 
+let expected_list_type instead pos_list =
+    let msg =
+        Format.asprintf
+            "Expected a list type, but got %a."
+            Type.pp instead
+    in
+    raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
+
 
 let invalid_ql_sequencing var pos_list =
     let msg =
@@ -295,12 +303,12 @@ let let_not_returnable ty pos_list =
             "The subject of a let-binding must be returnable. However, type %a is only usable."
             Type.pp ty
     in
-    raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list) 
+    raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
 
 let duplicate_interface_receive_env var iface pos_list =
     let msg =
         Format.asprintf
-            "To prevent unsafe aliasing, no other variables of the same interface as a received variable may be present in the body of a receive guard. However, variable %a also has interface name %s."
+            "To prevent unsafe aliasing, no other variables of the same interface as a received variable may be present in the body of a receive guard or a case expression. However, variable %a also has interface name %s."
             Ir.Var.pp_name var
             iface
     in
@@ -314,5 +322,3 @@ let pretype_consistency ty pty pos_list =
             Pretype.pp pty
     in
     raise (constraint_gen_error ~subsystem:Errors.GenCheck msg pos_list)
-
-
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index 334928a..abea6e0 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -8,7 +8,7 @@ open Ir
 open Util.Utility
 open Source_code
 
-let pretype_error msg pos_list = Errors.Pretype_error (msg,pos_list) 
+let pretype_error msg pos_list = Errors.Pretype_error (msg,pos_list)
 
 module Gripers = struct
     open Format
@@ -16,7 +16,7 @@ module Gripers = struct
     let arity_error pos expected_len actual_len =
         let msg =
             asprintf "Arity error. Expects %d arguments, but %d were provided."
-                expected_len 
+                expected_len
                 actual_len
         in
         raise (pretype_error msg [pos])
@@ -24,7 +24,7 @@ module Gripers = struct
     let tuple_arity_error pos expected_len actual_len =
         let msg =
             asprintf "Arity error. Tuple deconstructor has %d binders, but tuple has %d components."
-                expected_len 
+                expected_len
                 actual_len
         in
         raise (pretype_error msg [pos])
@@ -44,7 +44,7 @@ module Gripers = struct
 
     let type_mismatch pos_list expected actual =
         let msg =
-            asprintf "Type mismatch. Expected %a but got %a."                
+            asprintf "Type mismatch. Expected %a but got %a."
                 Pretype.pp expected
                 Pretype.pp actual
         in
@@ -52,7 +52,7 @@ module Gripers = struct
 
     let type_mismatch_with_expected pos expected_msg actual =
         let msg =
-            asprintf "Type mismatch. Expected %s but got %a."                
+            asprintf "Type mismatch. Expected %s but got %a."
                 expected_msg
                 Pretype.pp actual
         in
@@ -60,7 +60,7 @@ module Gripers = struct
 
     let cannot_synth_empty_guards pos () =
         let msg =
-            asprintf "Need at least one non-fail guard to synthesise the type for a 'guard' expression." 
+            asprintf "Need at least one non-fail guard to synthesise the type for a 'guard' expression."
         in
         raise (pretype_error msg [pos])
 
@@ -77,6 +77,15 @@ module Gripers = struct
                 Ir.pp_value term
         in
         raise (pretype_error msg [pos])
+
+    let cannot_synth_nil (term: value) =
+        let pos = WithPos.pos term in
+        let msg =
+            asprintf
+                "Cannot synthesise a type for an empty list %a"
+                Ir.pp_value term
+        in
+        raise (pretype_error msg [pos])
 end
 
 (* Note: This basically works since we only have mailbox subtyping at present.
@@ -140,6 +149,10 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
             let vs_and_tys = List.map (synthesise_val ienv env) vs in
             let (vs, tys) = List.split vs_and_tys in
             wrap (Tuple vs), Pretype.PTuple tys
+        | Cons (v1, v2) ->
+            let (v1, ty1) = synthesise_val ienv env v1 in
+            let v2 = check_val ienv env v2 (Pretype.PList ty1) in
+            wrap (Cons (v1, v2)), Pretype.PList ty1
         | Lam { linear; parameters; result_type; body } ->
             (* Defer linearity checking to constraint generation. *)
             let param_types  = List.map snd parameters in
@@ -157,6 +170,7 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
                 result = result_type 
             }
         | Inl _ | Inr _ -> Gripers.cannot_synth_sum value
+        | Nil -> Gripers.cannot_synth_nil value
 and check_val ienv env value ty =
     let (value_node, pos) = WithPos.(node value, pos value) in
     let wrap = WithPos.make ~pos in
@@ -171,6 +185,12 @@ and check_val ienv env value ty =
             raise
                 (Gripers.type_mismatch_with_expected pos
                     "a sum type" ty)
+        | Nil, (Pretype.PList _) ->
+          wrap Nil
+        | Nil, ty ->
+          raise
+            (Gripers.type_mismatch_with_expected pos
+              "a list type" ty)
         | _ ->
             let value, inferred_ty = synthesise_val ienv env value in
             check_tys [pos] ty inferred_ty;
@@ -247,6 +267,24 @@ and synthesise_comp ienv env comp =
             let cont, cont_ty = synthesise_comp ienv env' cont in
             WithPos.make ~pos
                 (LetTuple { binders; tuple; cont }), cont_ty
+        | CaseL { term = scrutinee; ty = ty1; nil = e1; cons = ((bnd1, bnd2), e2) } ->
+            let prety1 = Pretype.of_type ty1 in
+            let scrutinee =
+              check_val ienv env scrutinee prety1
+            in
+            let ty2 = match prety1 with
+              | Pretype.PList ty2 -> ty2
+              | _ -> raise (Gripers.type_mismatch_with_expected pos "a list type" prety1)
+            in
+            let b1_env = PretypeEnv.bind (Var.of_binder bnd1) ty2 env in
+            let b2_env = PretypeEnv.bind (Var.of_binder bnd2) prety1 b1_env in
+            let e2, b2_ty = synthesise_comp ienv b2_env e2 in
+            let e1 = check_comp ienv b2_env e1 b2_ty in
+            WithPos.make ~pos
+              (CaseL { term = scrutinee;
+                       ty = ty1;
+                       nil = e1;
+                       cons = ((bnd1, bnd2), e2) }), b2_ty
         | Seq (e1, e2) ->
             let e1 = check_comp ienv env e1 (Pretype.unit) in
             let e2, e2_ty = synth e2 in
diff --git a/lib/typecheck/solve_constraints.ml b/lib/typecheck/solve_constraints.ml
index 6128592..3d4583a 100644
--- a/lib/typecheck/solve_constraints.ml
+++ b/lib/typecheck/solve_constraints.ml
@@ -437,6 +437,12 @@ let pipeline constrs =
            to rid ourselves of pattern variables *)
         substitute_solutions lbs
     in
+    Settings.if_debug (fun () ->
+        Printf.printf "=== Simplified constraint set ===\n\n";
+        PVarMap.iter (fun k p ->
+            Format.(fprintf std_formatter "%s: %a\n" k Pattern.pp p)
+        ) resolved_constraints
+    );
     (* Check if solutions are satisfiable *)
     check_satisfiability resolved_constraints (get_upper_bounds constrs);
     (* Ensure that none of the pattern variables have been solved as zero *)
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 0233ed0..2b715c4 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -18,7 +18,7 @@ let lookup_opt = VarMap.find_opt
 let delete = VarMap.remove
 
 let delete_many vars env =
-    List.fold_right (delete) vars env 
+    List.fold_right (delete) vars env
 
 let delete_binder x = VarMap.remove (Ir.Var.of_binder x)
 let singleton = VarMap.singleton
@@ -55,7 +55,7 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                         ((In, pat), constrs)
         in
 
-        let join_types (var: Ir.Var.t) (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
+        let rec join_types (var: Ir.Var.t) (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
             let open Type in
             match (t1, t2) with
                 | Base b1, Base b2 when b1 = b2 ->
@@ -97,6 +97,21 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                               pattern = Some pat;
                               quasilinearity = ql
                           }, constrs
+                | List ty1, List ty2 ->
+                    let ty, constrs = join_types var ty1 ty2 in
+                    List ty, constrs
+                | Sum (t1l, t1r), Sum (t2l, t2r) ->
+                    let tl, constrs1 = join_types var t1l t2l in
+                    let tr, constrs2 = join_types var t1r t2r in
+                    Sum (tl, tr), Constraint_set.union constrs1 constrs2
+                | Tuple ts1, Tuple ts2 ->
+                    let (ts, constrs) =
+                        List.fold_left2 (fun (acc, constrs) t1 t2 ->
+                            let t, t_constrs = join_types var t1 t2 in
+                            t :: acc, Constraint_set.union t_constrs constrs)
+                        ([], Constraint_set.empty) ts1 ts2
+                    in
+                    Tuple ts, constrs
                 | _, _ ->
                     Gripers.type_mismatch true t1 t2 var [pos]
         in
@@ -197,7 +212,7 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                 | _, _ ->
                     Gripers.inconsistent_branch_capabilities var [pos]
         in
-        let intersect_types var (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
+        let rec intersect_types var (t1: Type.t) (t2: Type.t) : (Type.t * Constraint_set.t) =
             match t1, t2 with
                 | Base b1, Base b2 when b1 = b2 ->
                     (Base b1, Constraint_set.empty)
@@ -226,6 +241,21 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
                               (* Must take strongest QL across all branches. *)
                               quasilinearity = Quasilinearity.max ql1 ql2
                           }, constrs
+                | List t1, List t2 ->
+                    let ty, constrs = intersect_types var t1 t2 in
+                    List ty, constrs
+                | Sum (t1l, t1r), Sum (t2l, t2r) ->
+                    let tl, constrs1 = intersect_types var t1l t2l in
+                    let tr, constrs2 = intersect_types var t1r t2r in
+                    Sum (tl, tr), Constraint_set.union constrs1 constrs2
+                | Tuple ts1, Tuple ts2 ->
+                    let (ts, constrs) =
+                        List.fold_left2 (fun (acc, constrs) t1 t2 -> 
+                            let t, t_constrs = intersect_types var t1 t2 in
+                            t :: acc, Constraint_set.union t_constrs constrs)
+                        ([], Constraint_set.empty) ts1 ts2
+                    in
+                    Tuple ts, constrs
                 | _, _ ->
                     Gripers.type_mismatch false t1 t2 var [pos]
         in
@@ -251,24 +281,24 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
             let disjoints =
               let (disjoint_sends, disjoint_others) =
                 List.partition (fun (_, ty) ->
-                  Type.is_output_mailbox ty
+                  Type.contains_output_mailbox ty
                 ) (disjoint1 @ disjoint2)
               in
-              (* !E becomes !(E + 1) *)
-              let disjoint_sends =
-                List.map (fun (var, ty) ->
-                  let ty =
-                    match ty with
-                      | Mailbox { capability = Out; interface; quasilinearity; pattern = Some pat } ->
+              (* Relaxes a mailbox type from !E to !(E+1) *)
+              let rec relax_send_type = function
+                | Mailbox { capability = Out; interface; quasilinearity; pattern = Some pat } ->
                           let pat = Pattern.Plus (pat, Pattern.One) in
                           Mailbox { capability = Out; interface; quasilinearity; pattern = Some pat }
-                      | _ ->
-                          raise (Errors.internal_error "ty_env.ml" "error in disjoint MB combination")
-                  in
+                | List ty -> List (relax_send_type ty)
+                | _ ->
+                  raise (Errors.internal_error "ty_env.ml" "error in disjoint MB combination")
+              in
+              let disjoint_sends =
+                List.map (fun (var, ty) ->
+                  let ty = relax_send_type ty in
                   (var, ty)
                 ) disjoint_sends
               in
-
               let () =
                 List.iter (fun (var, ty) ->
                     if Type.is_lin ty then
@@ -314,3 +344,43 @@ let make_unrestricted env pos =
         Constraint_set.union acc (make_unrestricted ty pos)
     ) Constraint_set.empty (bindings env)
 
+(* If we are receiving a mailbox variable, without a dependency
+   graph, we must do some fairly coarse-grained aliasing
+   control when receiving from a mailbox or deconstructing a list.
+   There are three strategies:
+      1. Strict: the environment must be entirely unrestricted
+          (i.e., no other mailbox variables are free in the receive
+          block)
+
+      2. Interface: the environment cannot contain a variable of
+          the same interface. This means that we know we won't
+          accidentally alias, without being overly restrictive.
+
+      3. Nothing: No alias control: permissive, but unsafe.
+  *)
+let check_free_mailbox_variables bound_variable_types env =
+    let mb_iface_tys =
+        List.filter_map (fun ty ->
+            if Type.is_mailbox_type ty then
+                Some (Type.get_interface ty)
+            else None)
+        bound_variable_types
+    in
+    let open Settings in
+    let open ReceiveTypingStrategy in
+    match get receive_typing_strategy with
+        | Strict ->
+            iter (fun v ty ->
+                if Type.is_lin ty then
+                    Gripers.unrestricted_recv_env v ty []
+            ) env
+        | Interface ->
+            iter (fun v ty ->
+                match ty with
+                    | Type.Mailbox { interface; _ } when (List.mem interface mb_iface_tys) ->
+                        Gripers.duplicate_interface_receive_env
+                        v interface
+                        []
+                    | _ -> ()
+            ) env
+        | Nothing -> ()
diff --git a/lib/typecheck/ty_env.mli b/lib/typecheck/ty_env.mli
index d73323c..378179e 100644
--- a/lib/typecheck/ty_env.mli
+++ b/lib/typecheck/ty_env.mli
@@ -47,3 +47,8 @@ val make_unrestricted : t -> Position.t -> Constraint_set.t
     the environment.
  *)
 val check_type : Interface_env.t -> Ir.Var.t -> Type.t -> t -> Position.t -> Constraint_set.t
+
+(** Checks to see whether the environment contains any free variables with mailbox type,
+    depending on the current typechecking policy (strict, interface, none). Raises an
+    exception if so. *)
+val check_free_mailbox_variables : Type.t list -> t -> unit
diff --git a/lib/typecheck/type_utils.ml b/lib/typecheck/type_utils.ml
index cc3cedc..ddffccf 100644
--- a/lib/typecheck/type_utils.ml
+++ b/lib/typecheck/type_utils.ml
@@ -9,12 +9,11 @@ open Common.Source_code
    type !E can be treated as unrestricted if 1 is included in E (i.e., we could
    choose not to send).
  *)
-let make_unrestricted t pos =
+let rec make_unrestricted t pos =
     let open Type in
     match t with
         (* Trivially unrestricted *)
         | Base _
-        | Tuple []
         | Fun { linear = false; _ } -> Constraint_set.empty
         (* Cannot be unrestricted *)
         | Fun { linear = true; _ }
@@ -24,6 +23,13 @@ let make_unrestricted t pos =
         | Mailbox { capability = Capability.Out; pattern = Some pat; _ } ->
                 Constraint_set.of_list
                     [Constraint.make (Pattern.One) pat]
+        | Tuple tys ->
+            Constraint_set.union_many
+                (List.map (fun t -> make_unrestricted t pos) tys)
+        | Sum (ty1, ty2) ->
+            Constraint_set.union (make_unrestricted ty1 pos) (make_unrestricted ty2 pos)
+        | List ty ->
+            make_unrestricted ty pos
         | _ -> assert false
 
 (* Auxiliary definitions*)
@@ -43,12 +49,13 @@ let rec subtype_type :
             (* Subtyping covariant for tuples and sums *)
             | Tuple tyas, Tuple tybs ->
                 Constraint_set.union_many
-                    (List.map (fun (tya, tyb) -> subtype_type visited ienv tya tyb pos) 
+                    (List.map (fun (tya, tyb) -> subtype_type visited ienv tya tyb pos)
                         (List.combine tyas tybs))
             | Sum (tya1, tya2), Sum (tyb1, tyb2) ->
                 Constraint_set.union
                     (subtype_type visited ienv tya1 tyb1 pos)
                     (subtype_type visited ienv tya2 tyb2 pos)
+            | List ty1, List ty2 -> subtype_type visited ienv ty1 ty2 pos
             | Mailbox { pattern = None; _ }, _
             | _, Mailbox { pattern = None; _ } ->
                     (* Should have been sorted by annotation pass *)
diff --git a/test/errors/uaf_lists.pat b/test/errors/uaf_lists.pat
new file mode 100644
index 0000000..1ab6a12
--- /dev/null
+++ b/test/errors/uaf_lists.pat
@@ -0,0 +1,20 @@
+interface Test { M(Test!1) }
+
+def drain(x: Test?): Unit {
+    guard x : M* {
+        free -> ()
+        receive M(y) from z -> drain(z)
+    }
+}
+
+def go(): Unit {
+    let x = new[Test] in
+    let xs = (x cons (nil: List(Test![U]))) in
+    caseL xs : List(Test!) of {
+          nil -> ()
+        | (a cons as) -> x ! M(a)
+    };
+    drain(x)
+}
+
+go()
diff --git a/test/examples/robotsn-lists.pat b/test/examples/robotsn-lists.pat
new file mode 100644
index 0000000..f1acfa2
--- /dev/null
+++ b/test/examples/robotsn-lists.pat
@@ -0,0 +1,145 @@
+interface Door {
+    Want(Int, Robot!),
+    Inside(Robot!),
+    Prepared(Warehouse!),
+    WantLeave(Robot!),
+    Outside(),
+    TableIdle(Warehouse!)
+}
+
+interface Robot {
+    GoIn(Door!),
+    GoOut(Door!),
+    Busy(),
+    Delivered(Warehouse!, Door!)
+}
+
+interface Warehouse {
+    Prepare(Int, Door!),
+    Deliver(Robot!, Door!),
+    PartTaken()
+}
+
+# Door
+def freeDoor(self: Door?, warehouse: Warehouse!): Unit {
+    guard self : Want* {
+        free -> ()
+        receive Want(part, robot) from self ->
+            robot ! GoIn(self);
+            warehouse ! Prepare(part, self);
+            busyDoor(self)
+    }
+}
+
+def busyDoor(self: Door?): Unit {
+    guard self : Inside . Prepared . Want* {
+        receive Want(partNum, robot) from self ->
+            robot ! Busy();
+            busyDoor(self)
+        receive Inside(robot) from self ->
+            guard self : Prepared . Want* {
+                receive Prepared(warehouse) from self ->
+                    warehouse ! Deliver(robot, self);
+                    guard self : WantLeave . TableIdle . Want* {
+                        receive WantLeave(robot) from self ->
+                            robot ! GoOut(self);
+                            finaliseDoor(self, warehouse)
+                    }
+            }
+    }
+}
+
+def finaliseDoor(self: Door?, warehouse: Warehouse!): Unit {
+    guard self : Outside . TableIdle . Want* {
+        receive Outside() from self ->
+            guard self : TableIdle . Want* {
+                receive TableIdle(warehouse) from self ->
+                    freeDoor(self, warehouse)
+            }
+        receive TableIdle(warehouse) from self ->
+            guard self : Outside . Want* {
+                receive Outside() from self ->
+                    freeDoor(self, warehouse)
+            }
+    }
+}
+
+# Robot
+def idleRobot(self: Robot?, door: Door!): Unit {
+    door ! Want(0, self);
+    guard self : (Busy + GoIn) {
+        receive Busy() from self -> free(self)
+        receive GoIn(door) from self ->
+            door ! Inside(self);
+            insideRobot(self)
+    }
+}
+
+def insideRobot(self: Robot?): Unit {
+    let self =
+        guard self : Delivered {
+            receive Delivered(warehouse, door) from self ->
+                warehouse ! PartTaken();
+                door ! WantLeave(self);
+                self
+        }
+    in
+    guard self : GoOut {
+        receive GoOut(door) from self ->
+            door ! Outside();
+            free(self)
+    }
+}
+
+# Warehouse
+def freeWarehouse(self: Warehouse?): Unit {
+    guard self : Prepare + 1 {
+        free -> ()
+        receive Prepare(partNum, door) from self ->
+            door ! Prepared(self);
+            preparedWarehouse(self)
+    }
+}
+
+def preparedWarehouse(self: Warehouse?): Unit {
+    guard self : Deliver {
+        receive Deliver(robot, door) from self ->
+            robot ! Delivered(self, door);
+            handlePartTaken(self, door)
+    }
+}
+
+def handlePartTaken(self: Warehouse?, door: Door!): Unit {
+    guard self : PartTaken {
+        receive PartTaken() from self ->
+            door ! TableIdle(self);
+            freeWarehouse(self)
+    }
+}
+
+def discardList(xs: List(Robot!)) : Unit {
+    caseL xs : List(Robot!) of {
+        nil -> ()
+        | (a :: as) -> discardList(as)
+    }
+}
+
+def spawnRobots(numRobots: Int, door: Door!, acc: List(Robot!)): Unit {
+    if (numRobots <= 0) {
+        discardList(acc)
+    } else {
+        let newRobot = new[Robot] in
+        spawn { idleRobot(newRobot, door) };
+        spawnRobots(numRobots - 1, door, (newRobot :: acc))
+    }
+}
+
+def main(n: Int): Unit {
+    let door = new[Door] in
+    let warehouse = new[Warehouse] in
+    spawn { freeDoor(door, warehouse) };
+    spawnRobots(n, door, (nil : List(Robot!)));
+    spawn { freeWarehouse(warehouse) }
+}
+
+main(3)
diff --git a/test/examples/savina/banking.pat b/test/examples/savina/banking.pat
index 8c5d2b5..5a92098 100644
--- a/test/examples/savina/banking.pat
+++ b/test/examples/savina/banking.pat
@@ -1,10 +1,10 @@
 ### Adapted from Savina/banking.
 ###
-### A benchmark that implements a request-reply chain passing scenario. Several 
+### A benchmark that implements a request-reply chain passing scenario. Several
 ### account processes are spawned, each of which may be sent a credit request
-### by the central teller process. The benchmark is parameterized by the number 
-### of account processes. Since the array type is not available in Pat, we fix 
-### the number of account processes to 3.
+### by the central teller process. The benchmark is parameterized by the number
+### of account processes. Since the array type is not available in Pat, we fix
+### the number of account processes to 3.
 
 interface TellerMb {
   Start(),
@@ -18,10 +18,10 @@ interface AccountMb {
   Stop()
 }
 
-## Teller process handling the creation of account processes and launching of 
-## main loop.
+## Teller process handling the creation of account processes and launching of
+## main loop.
 def teller(self: TellerMb?, numAccounts: Int): Unit {
-  
+
   # Create accounts.
   let accountMb1 = new [AccountMb] in
   spawn { account(accountMb1, 1, 200) };
@@ -35,7 +35,7 @@ def teller(self: TellerMb?, numAccounts: Int): Unit {
   guard self: Start {
     receive Start() from self ->
 
-      # Note. Even if the randomization of message sending is performed in a 
+      # Note. Even if the randomization of message sending is performed in a
       # different processes, there is no risk of a race condition where the
       # messages are sent to a non-existing mailbox. This is because, as can be
       # gleaned above, mailboxes are created in sequential fashion within this
@@ -47,20 +47,20 @@ def teller(self: TellerMb?, numAccounts: Int): Unit {
 
 ## Randomly chooses the source account.
 def generate_work(tellerMb: TellerMb!, numAccounts: Int, acc1: AccountMb![R], acc2: AccountMb![R], acc3 : AccountMb![R]): Unit {
-  
+
   # Randomly choose source account from which the funds shall be taken.
-  let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
+  let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
   if (sourceId == 0) {
 
-    # First source account.
+    # First source account.
     choose_dst_acc(tellerMb, numAccounts, acc1, acc2, acc3)
   }
-  else { 
+  else {
     if (sourceId == 1) {
 
         # Second source account.
         choose_dst_acc(tellerMb, numAccounts, acc2, acc1, acc3)
-    } 
+    }
     else {
 
         # Third source account.
@@ -69,17 +69,17 @@ def generate_work(tellerMb: TellerMb!, numAccounts: Int, acc1: AccountMb![R], ac
   }
 }
 
-## Randomly chooses the destination account and issues a credit request. The
+## Randomly chooses the destination account and issues a credit request. The
 ## function ensures that the source and destination account are different.
 def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: AccountMb![R], dstAccountMb1: AccountMb![R], dstAccountMb2 : AccountMb![R]): Unit {
-  
-  # Randomly choose destination account to which funds shall be deposited. -2 
-  # because rand() is 0-indexed, and because we do not include the source 
+
+  # Randomly choose destination account to which funds shall be deposited. -2
+  # because rand() is 0-indexed, and because we do not include the source
   # account in the random choice (i.e., the source account is not permitted to
-  # send funds to itself).
-  let dstAccountId = rand(numAccounts - 2) in 
+  # send funds to itself).
+  let dstAccountId = rand(numAccounts - 2) in
 
-  let dstAccount = 
+  let dstAccount =
     if (dstAccountId == 0) {
       dstAccountMb1
     } else {
@@ -91,12 +91,12 @@ def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccountMb: AccountM
   dstAccount ! Credit(tellerMb, amount, srcAccountMb)
 }
 
-## Teller process main loop handling replies from accounts.
+## Teller process main loop handling replies from accounts.
 def teller_loop(self: TellerMb?, accountMb1: AccountMb!, accountMb2: AccountMb!, accountMb3: AccountMb!): Unit {
   guard self: Reply* {
     free -> 
 
-      # All credit requests serviced. Stop accounts.
+      # All credit requests serviced. Stop accounts.
       accountMb1 ! Stop();
       accountMb2 ! Stop();
       accountMb3 ! Stop()
@@ -105,8 +105,8 @@ def teller_loop(self: TellerMb?, accountMb1: AccountMb!, accountMb2: AccountMb!,
   }
 }
 
-## Account process handling credit requests issued by the teller, and debit 
-## requests issued by other accounts.
+## Account process handling credit requests issued by the teller, and debit
+## requests issued by other accounts.
 def account(self: AccountMb?, id: Int, balance: Int): Unit {
   guard self: (Debit + Credit)* . Stop {
     free -> 
@@ -130,13 +130,13 @@ def account(self: AccountMb?, id: Int, balance: Int): Unit {
           tellerMb ! Reply();
           account(self, id, balance - amount)
       }
-      
+
     receive Stop() from self ->
       account_exit(self)
   }
 }
 
-## Actor process exit procedure that flushes potential residual messages.
+## Actor process exit procedure that flushes potential residual messages.
 def account_exit(self: AccountMb?): Unit {
   guard self: (Debit + Credit)*  {
     free -> ()
@@ -147,7 +147,7 @@ def account_exit(self: AccountMb?): Unit {
   }
 }
 
-## Launcher.
+## Launcher.
 def main(): Unit {
   let tellerMb = new [TellerMb] in
   spawn { teller(tellerMb, 3) };
diff --git a/test/examples/savina/big.pat b/test/examples/savina/big.pat
index eb8698a..0f995af 100644
--- a/test/examples/savina/big.pat
+++ b/test/examples/savina/big.pat
@@ -1,9 +1,9 @@
 ### Adapted from Savina/big.
 ###
-### A benchmark that implements a many-to-many message passing scenario. Several 
-### processes are spawned, each of which sends a ping message to the others, and 
-### responds with a pong message to any ping message it receives. The benchmark 
-### is parameterized by the number of processes. Since the array type is not 
+### A benchmark that implements a many-to-many message passing scenario. Several
+### processes are spawned, each of which sends a ping message to the others, and
+### responds with a pong message to any ping message it receives. The benchmark
+### is parameterized by the number of processes. Since the array type is not
 ### available in Pat, we fix the number of processes to 3.
 
 interface ActorMb {
@@ -29,10 +29,10 @@ def actor(self: ActorMb?, exitMb : ExitMb?, id: Int, sinkMb: SinkMb!): Unit {
   }
 }
 
-## Blocks actor process and awaits termination message.
+## Blocks actor process and awaits termination message.
 def await_exit(exitMb: ExitMb?): Unit {
     guard exitMb : Exit {
-        receive Exit() from exitMb -> 
+        receive Exit() from exitMb ->
           free(exitMb)
     }
 }
@@ -54,21 +54,21 @@ def actor_loop(self: ActorMb?, exitMb: ExitMb?,
 
       if (numPings <= 0) {
 
-        # No more pongs to issue. 
+        # No more pongs to issue.
         sinkMb ! Done();
         actor_exit(self);
         await_exit(exitMb)
       }
       else {
 
-        # Issue ping to random participant.
+        # Issue ping to random participant.
         send_ping(id, actorMb1, actorMb2);
         actor_loop(self, exitMb, id, sinkMb, numPings - 1, actorMb1, actorMb2)
       }
   }
 }
 
-## Actor process exit procedure that flushes potential residual messages.
+## Actor process exit procedure that flushes potential residual messages.
 def actor_exit(self: ActorMb?): Unit {
   guard self: Ping* . Pong* {
     free -> ()
@@ -79,9 +79,9 @@ def actor_exit(self: ActorMb?): Unit {
   }
 }
 
-## Replies to ping messages via a pong issued to the specified actor ID.
+## Replies to ping messages via a pong issued to the specified actor ID.
 def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
-  
+
   # We are not synchronising here, but using IDs, which loses information. This
   # makes the type checker think that it might not receive the pong reply. Thus,
   # the type of the mailbox would be ?(Pong + 1).
@@ -95,9 +95,9 @@ def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): U
 
 ## Randomly issues a ping message to one of the participating actors.
 def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
-  
+
   let pongerId = rand(2) in
-  
+
   if (pongerId == 1) {
     actorMb1 ! Ping(id)
   }
@@ -118,7 +118,7 @@ def sink(self: SinkMb?): Unit {
 def sink_loop(self: SinkMb?, exitMb1: ExitMb!, exitMb2: ExitMb!, exitMb3: ExitMb!): Unit {
   guard self: Done* {
     free ->
-      # Notify all actors. Placing the sends in this clause ensures that
+      # Notify all actors. Placing the sends in this clause ensures that
       # each actor is notified once.
         exitMb1 ! Exit();
         exitMb2 ! Exit();
@@ -129,9 +129,9 @@ def sink_loop(self: SinkMb?, exitMb1: ExitMb!, exitMb2: ExitMb!, exitMb3: ExitMb
 }
 
 
-## Launcher.
+## Launcher.
 def main(): Unit {
-  
+
   let sinkMb = new [SinkMb] in
   spawn { sink(sinkMb) };
 
diff --git a/test/examples/savina/cig_smok.pat b/test/examples/savina/cig_smok.pat
index 07f7d10..ed15e78 100644
--- a/test/examples/savina/cig_smok.pat
+++ b/test/examples/savina/cig_smok.pat
@@ -126,4 +126,4 @@ def main(): Unit {
   arbiterMb ! Start()
 }
 
-main()
+main()
\ No newline at end of file
diff --git a/test/examples/savina/kfork.pat b/test/examples/savina/kfork.pat
index bb953a7..b6b1510 100644
--- a/test/examples/savina/kfork.pat
+++ b/test/examples/savina/kfork.pat
@@ -1,15 +1,15 @@
 ### Adapted from Savina/fjthrput.
 ###
-### Models the creation of n actors that are given a number of messages, for 
+### Models the creation of n actors that are given a number of messages, for
 ### each of which, a computation is performed. The benchmark is parameterized by
-### the number of actor processes. Since the array type is not available in 
-### Pat, we fix the number of actor processes to 3.
+### the number of actor processes. Since the array type is not available in
+### Pat, we fix the number of actor processes to 3.
 
 interface ActorMb {
   Packet()
 }
 
-## Actor processes handling the packet requests.
+## Actor processes handling the packet requests.
 def actor(self: ActorMb?): Unit {
   guard self: Packet* {
     free ->
@@ -20,17 +20,17 @@ def actor(self: ActorMb?): Unit {
   }
 }
 
-## Computes the factorial of n.
+## Computes the factorial of n.
 def fact(n: Int): Int {
   if (n <= 0) {
     1
   }
   else {
-    n * (fact(n - 1)) 
+    n * (fact(n - 1))
   }
 }
 
-## Sends the given number of messages to the specified actor mailbox.
+## Sends the given number of messages to the specified actor mailbox.
 def flood(numMessages: Int, actorMb: ActorMb!): Unit {
   if (numMessages <= 0) {
     ()
@@ -41,9 +41,9 @@ def flood(numMessages: Int, actorMb: ActorMb!): Unit {
   }
 }
 
-## Launcher.
+## Launcher.
 def main(): Unit {
-  
+
   let actorMb1 = new [ActorMb] in
   spawn { actor(actorMb1) };
 
diff --git a/test/examples/savina/lists/banking.pat b/test/examples/savina/lists/banking.pat
new file mode 100644
index 0000000..c4e3bd4
--- /dev/null
+++ b/test/examples/savina/lists/banking.pat
@@ -0,0 +1,175 @@
+### Adapted from Savina/banking.
+###
+### A benchmark that implements a request-reply chain passing scenario. Several
+### account processes are spawned, each of which may be sent a credit request
+### by the central teller process. The benchmark is parameterized by the number
+### of account processes.
+
+interface TellerMb {
+  Start(),
+  Reply()
+}
+
+interface AccountMb {
+  Debit(AccountMb!, Int),
+  Credit(TellerMb!, Int, AccountMb!),
+  Done(),
+  Stop()
+}
+
+def spawnAccounts(self: TellerMb?, numsAccounts: List(Int), soFar: Int, acc: List(AccountMb!)) : (TellerMb? * List(AccountMb!)) {
+  caseL numsAccounts : List(Int) of {
+    nil -> (self, acc)
+    | (n :: ns) ->
+        let accountMb = new [AccountMb] in
+        spawn { account(accountMb, soFar, n)};
+        spawnAccounts(self, ns, soFar + 1, (accountMb :: acc))
+    }
+  }
+
+## Teller process handling the creation of account processes and launching of
+## main loop.
+def teller(self: TellerMb?, numAccounts : Int, numsAccounts: List(Int)): Unit {
+
+  let (self, accountMbs) = spawnAccounts(self, numsAccounts, 1, (nil : List(AccountMb!))) in
+
+  guard self: Start {
+    receive Start() from self ->
+
+      # Note. Even if the randomization of message sending is performed in a
+      # different processes, there is no risk of a race condition where the
+      # messages are sent to a non-existing mailbox. This is because, as can be
+      # gleaned above, mailboxes are created in sequential fashion within this
+      # (i.e., the teller) process.
+      spawn { generate_work(self, numAccounts, accountMbs) } ;
+      teller_loop(self, accountMbs)
+  }
+}
+
+## Randomly chooses the source account.
+def generate_work(tellerMb: TellerMb!, numAccounts: Int, accs : List(AccountMb![R])): Unit {
+
+  # Randomly choose source account from which the funds shall be taken.
+  let sourceId = rand(numAccounts - 1) in # -1 because rand() is 0-indexed.
+
+  let (choice, rest) = pick(accs, sourceId, (nil : List(AccountMb![R]))) in
+  choose_dst_acc(tellerMb, numAccounts, choice, rest)
+}
+
+def pick(accs : List(AccountMb![R]), index : Int, rest : List(AccountMb![R])) : ((Unit + AccountMb![R]) * List(AccountMb![R])) {
+if (index == 0) {
+    caseL accs : List(AccountMb![R]) of {
+        nil -> let x = () in (inl(x) : (Unit + AccountMb!), rest)
+        | (a :: as) -> (inr(a) : (Unit + AccountMb!), append(rest, as))
+    }}
+else {
+    caseL accs : List(AccountMb![R]) of {
+        nil ->  let x = () in (inl(x) : (Unit + AccountMb!), rest)
+        | (a :: as) -> pick(as, index - 1, (a :: rest))
+    }}
+}
+
+def append(l1 : List(AccountMb![R]), l2: List(AccountMb![R])) : List(AccountMb![R]) {
+    caseL l1 : List(AccountMb![R]) of {
+        nil -> l2
+        | (a :: as) -> append(as, (a :: l2))
+    }
+}
+
+## Randomly chooses the destination account and issues a credit request. The
+## function ensures that the source and destination account are different.
+def choose_dst_acc(tellerMb: TellerMb!, numAccounts: Int, srcAccount: (Unit + AccountMb![R]), dstAccountMbs : List(AccountMb![R])) : Unit {
+
+  (# Randomly choose destination account to which funds shall be deposited. -2
+    # because rand() is 0-indexed, and because we do not include the source
+    # account in the random choice (i.e., the source account is not permitted to
+    # send funds to itself).
+    let dstAccountId = rand(numAccounts - 2) in
+  
+    let (dstAccount, rest) = (pick(dstAccountMbs, dstAccountId, (nil : List(AccountMb![R]))) : ((Unit + AccountMb!Credit[R]) * List(AccountMb!1[R])))
+    in
+  
+    (let amount = rand(200) in
+          case srcAccount : (Unit + AccountMb!) of {
+          inl(u1) : Unit -> case dstAccount : (Unit + AccountMb!) of {
+              inl(u2) : Unit -> ()
+              | inr(d) : AccountMb! -> ()
+          }
+          | inr(a) : AccountMb! -> case dstAccount : (Unit + AccountMb!) of {
+              inl(u) : Unit -> ()
+              | inr(d) : AccountMb! -> d ! Credit(tellerMb, amount, a)
+          }
+        }))
+}
+
+## Teller process main loop handling replies from accounts.
+def teller_loop(self: TellerMb?, accountMbs : List(AccountMb!)): Unit {
+  guard self: Reply* {
+    free ->
+      # All credit requests serviced. Stop accounts.
+      stopAccounts(accountMbs)
+    receive Reply() from self ->
+      teller_loop(self, accountMbs)
+  }
+}
+
+def stopAccounts(accs: List(AccountMb!)) : Unit {
+    caseL accs : List(AccountMb!) of {
+        nil -> ()
+        | (a :: as) ->
+            a ! Stop();
+            stopAccounts(as)
+        }
+}
+
+## Account process handling credit requests issued by the teller, and debit
+## requests issued by other accounts.
+def account(self: AccountMb?, id: Int, balance: Int): Unit {
+  guard self: (Debit + Credit)* . Stop {
+    free ->
+      ()
+    receive Debit(accountMb, amount) from self ->
+
+      accountMb ! Done();
+      account(self, id, balance + amount)
+    receive Credit(tellerMb, amount, accountMb) from self ->
+
+      # A more uglier implementation would have been to use the 'global mailbox
+      # way' where all messages are collected in one mailbox.
+      let transMb = new [AccountMb] in
+      accountMb ! Debit(transMb, amount);
+
+      guard transMb: Done + 1{
+        free ->
+          account(self, id, balance)
+        receive Done() from transMb ->
+          free(transMb);
+          tellerMb ! Reply();
+          account(self, id, balance - amount)
+      }
+
+    receive Stop() from self ->
+      account_exit(self)
+  }
+}
+
+## Actor process exit procedure that flushes potential residual messages.
+def account_exit(self: AccountMb?): Unit {
+  guard self: (Debit + Credit)*  {
+    free -> ()
+    receive Debit(accountMb, amount) from self ->
+      account_exit(self)
+    receive Credit(tellerMb, amount, accountMb) from self ->
+      account_exit(self)
+  }
+}
+
+## Launcher.
+def main(): Unit {
+  let tellerMb = new [TellerMb] in
+  spawn { teller(tellerMb, 3, (200 :: (150 :: (50 :: (nil : List(Int)))))) };
+
+  tellerMb ! Start()
+}
+
+main()
diff --git a/test/examples/savina/lists/barber.pat b/test/examples/savina/lists/barber.pat
new file mode 100644
index 0000000..1615169
--- /dev/null
+++ b/test/examples/savina/lists/barber.pat
@@ -0,0 +1,187 @@
+### Adapted from savina/barber. 
+###
+### A barber is waiting for customers. When there are no customers the barber sleeps. When a customer
+### arrives, he wakes the barber or sits in one of the waiting chairs in the waiting room. If all chairs
+### are occupied, the customer leaves. Customers repeatedly visit the barber shop until they get a haircut.
+### The key element of the solution is to make sure that whenever a customer or a barber checks the state
+### of the waiting room, they always see a valid state. The problem is implemented using a Selector actor
+### that decides which is the next customer, Customer actors, a Barber actor and a Room actor.
+
+interface RoomMb {
+    Enter(CustomerMb!),
+    Next(),
+    Exit()
+}
+
+interface BarberMb {
+    Enter(CustomerMb!, RoomMb!),
+    Exit()
+}
+
+interface SelectorMb {
+    Start(),
+    Returned(CustomerMb!)
+}
+
+interface CustomerMb {
+    Full(RoomMb!),
+    Start(RoomMb!),
+    Done(),
+    Exit()
+}
+
+def room(self: RoomMb?, capacity: Int, waiters: List(CustomerMb!), waiting: Int, barber: BarberMb!): Unit {
+    guard self: (Enter + Next + Exit)* {
+        free -> ()
+        receive Enter(customerMb) from self ->
+            if (waiting == capacity) {
+                customerMb ! Full(self);
+                room(self, capacity, waiters, waiting, barber)
+            }
+            else {
+                sleep(5);
+                room(self, capacity, (customerMb :: waiters), (waiting + 1), barber)
+            }
+        receive Next() from self ->
+            caseL waiters : List(CustomerMb!) of {
+                nil ->
+                    sleep(5);
+                    room(self, capacity, (nil : List(CustomerMb!)), waiting, barber)
+                | (a :: as) -> 
+                    barber ! Enter(a, self);
+                    room(self, capacity, as, (waiting - 1), barber)
+            }
+        receive Exit() from self ->
+            barber ! Exit();
+            roomExit(self)
+    }
+}
+
+def roomExit(self : RoomMb?) : Unit {
+    guard self: (Enter + Next + Exit)* {
+        free -> ()
+        receive Enter(customerMb) from self -> roomExit(self)
+        receive Next() from self -> roomExit(self)
+        receive Exit() from self -> roomExit(self)
+    }
+}
+
+def barber(self: BarberMb?): Unit {
+    guard self: (Enter + Exit)* {
+        free -> ()
+        receive Enter(customerMb, roomMb) from self ->
+            sleep(10);
+            customerMb ! Done();
+            roomMb ! Next();
+            barber(self)
+        receive Exit() from self ->
+            barberExit(self)
+    }
+}
+
+def barberExit(self : BarberMb?) : Unit {
+    guard self: (Enter + Exit)* {
+        free -> ()
+        receive Enter(customerMb, roomMb) from self -> barberExit(self)
+        receive Exit() from self -> barberExit(self)
+    }
+}
+
+def spawnCustomers(self: SelectorMb?, generator: Int, soFar: Int, acc : List(CustomerMb!)): (SelectorMb? * List(CustomerMb!)) {
+    if (soFar == generator) {
+            (self, acc)
+        }
+    else {
+        let customerMb = new [CustomerMb] in
+        spawn { customer(customerMb, self)};
+        spawnCustomers(self, generator, (soFar + 1), (customerMb :: acc))
+    }
+}
+
+def startCustomers(customerMbs : List(CustomerMb!), room : RoomMb!) : Unit {
+    caseL customerMbs : List(CustomerMb!) of {
+        nil -> ()
+        | (a :: as) ->
+            a ! Start(room);
+            startCustomers(as, room)
+    } 
+}
+
+def doneCustomers(customerMbs : List(CustomerMb!)) : Unit {
+    caseL customerMbs : List(CustomerMb!) of {
+        nil -> ()
+        | (a :: as) ->
+            a ! Done();
+            doneCustomers(as)
+    } 
+}
+
+def selector(self: SelectorMb?, generator: Int, haircuts: Int, target: Int, customers : List(CustomerMb!), room: RoomMb!): Unit {
+    guard self: (Start + Returned)* {
+        free -> ()
+        receive Start() from self ->
+            let (self, newCustomers) = spawnCustomers(self, generator, 0, (nil : List(CustomerMb!))) in
+            startCustomers(customers, room);
+            selector(self, generator, haircuts, target, newCustomers, room)
+        receive Returned(customerMb) from self ->
+            let newHaircuts = haircuts + 1 in
+            if (newHaircuts == target) {
+                doneCustomers(customers);
+                room ! Exit();
+                selectorExit(self)
+            }
+            else {
+                customerMb ! Start(room);
+                selector(self, generator, newHaircuts, target, customers, room)
+            }
+    }
+}
+
+def selectorExit(self : SelectorMb?) : Unit {
+    guard self: (Start + Returned)* {
+        free -> ()
+        receive Start() from self -> selectorExit(self)
+        receive Returned(customerMb) from self -> selectorExit(self)
+    }
+}
+
+def customer(self: CustomerMb?, selector: SelectorMb!): Unit {
+    guard self: (Full + Start + Done + Exit)* {
+        free -> ()
+        receive Full(room) from self ->
+            sleep(10);
+            self ! Start(room);
+            customer(self, selector)
+        receive Start(room) from self ->
+            room ! Enter(self);
+            customer(self, selector)
+        receive Done() from self ->
+            selector ! Returned(self);
+            customer(self, selector)
+        receive Exit() from self ->
+            customerExit(self)
+    }
+}
+
+def customerExit(self : CustomerMb?) : Unit {
+    guard self: (Full + Start + Done + Exit)* {
+        free -> ()
+        receive Full(room) from self -> customerExit(self)
+        receive Start(room) from self -> customerExit(self)
+        receive Done() from self -> customerExit(self)
+        receive Exit() from self -> customerExit(self)
+    }
+}
+
+def main() : Unit {
+    let barberMb = new [BarberMb] in
+    spawn {barber(barberMb)};
+
+    let roomMb = new [RoomMb] in
+    spawn {room(roomMb, 2, (nil : List(CustomerMb!)), 0, barberMb)};
+
+    let selectorMb = new [SelectorMb] in
+    spawn {selector(selectorMb, 4, 0, 6, (nil : List(CustomerMb!)), roomMb)};
+
+    selectorMb ! Start()
+}
diff --git a/test/examples/savina/lists/big.pat b/test/examples/savina/lists/big.pat
new file mode 100644
index 0000000..c26ae95
--- /dev/null
+++ b/test/examples/savina/lists/big.pat
@@ -0,0 +1,164 @@
+### Adapted from Savina/big.
+###
+### A benchmark that implements a many-to-many message passing scenario. Several
+### processes are spawned, each of which sends a ping message to the others, and
+### responds with a pong message to any ping message it receives. The benchmark
+### is parameterized by the number of processes.
+
+interface ActorMb {
+  Ping(Int),
+  Pong(Int),
+  Neighbors(ActorMb!, ActorMb!)
+}
+
+interface ExitMb {
+  Exit()
+}
+
+interface SinkMb {
+  Done(),
+  Actors(List(ExitMb!))
+}
+
+## Actor process handling the launching of main loop.
+def actor(self: ActorMb?, exitMb : ExitMb?, id: Int, sinkMb: SinkMb!): Unit {
+  guard self: Neighbors . (Pong + Ping)*  {
+    receive Neighbors(actorMb1, actorMb2) from self ->
+      actor_loop(self, exitMb, id, sinkMb, 100, actorMb1, actorMb2)
+  }
+}
+
+## Blocks actor process and awaits termination message.
+def await_exit(exitMb: ExitMb?): Unit {
+    guard exitMb : Exit {
+        receive Exit() from exitMb ->
+          free(exitMb)
+    }
+}
+
+## Actor process main loop issuing ping requests and handling pong replies.
+def actor_loop(self: ActorMb?, exitMb: ExitMb?, id: Int, sinkMb: SinkMb!, numPings: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+  guard self: (Ping + Pong)* {
+    free ->
+      await_exit(exitMb)
+    receive Ping(pingerId) from self ->
+
+      # Reply to ping.
+      send_pong(id, pingerId, actorMb1, actorMb2);
+      actor_loop(self, exitMb, id, sinkMb, numPings, actorMb1, actorMb2)
+
+    receive Pong(pongerId) from self ->
+
+      if (numPings <= 0) {
+
+        # No more pongs to issue.
+        sinkMb ! Done();
+        actor_exit(self);
+        await_exit(exitMb)
+      }
+      else {
+
+        # Issue ping to random participant.
+        send_ping(id, actorMb1, actorMb2);
+        actor_loop(self, exitMb, id, sinkMb, numPings - 1, actorMb1, actorMb2)
+      }
+  }
+}
+
+## Actor process exit procedure that flushes potential residual messages.
+def actor_exit(self: ActorMb?): Unit {
+  guard self: (Ping*) . (Pong*) {
+    free -> ()
+    receive Ping(pingerId) from self ->
+      actor_exit(self)
+    receive Pong(pongerId) from self ->
+      actor_exit(self)
+  }
+}
+
+## Replies to ping messages via a pong issued to the specified actor ID.
+def send_pong(id: Int, pingerId: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+
+  # We are not synchronising here, but using IDs, which loses information. This
+  # makes the type checker think that it might not receive the pong reply. Thus,
+  # the type of the mailbox would be ?(Pong + 1).
+  if (pingerId == 1) {
+    actorMb1 ! Pong(id)
+  }
+  else {
+    actorMb2 ! Pong(id)
+  }
+}
+
+## Randomly issues a ping message to one of the participating actors.
+def send_ping(id: Int, actorMb1: ActorMb!, actorMb2: ActorMb!): Unit {
+
+  let pongerId = rand(2) in
+
+  if (pongerId == 1) {
+    actorMb1 ! Ping(id)
+  }
+  else {
+    actorMb2 ! Ping(id)
+  }
+}
+
+## Sink process that coordinates actor termination.
+def sink(self: SinkMb?): Unit {
+  guard self: Actors . (Done*) {
+    receive Actors(exitMbs) from self ->
+      sink_loop(self, exitMbs)
+  }
+}
+
+## Sink process main loop issuing termination messages.
+def sink_loop(self: SinkMb?, exitMbs : List(ExitMb!)): Unit {
+  guard self: Done* {
+    free ->
+      # Notify all actors. Placing the sends in this clause ensures that
+      # each actor is notified once.
+      notifyExits(exitMbs)
+    receive Done() from self ->
+        sink_loop(self, exitMbs)
+  }
+}
+
+def notifyExits(exitMbs : List(ExitMb!)): Unit {
+    caseL exitMbs : List(ExitMb!) of {
+    nil -> ()
+  | (y :: ys) ->
+        y ! Exit();
+        notifyExits(ys)
+    }
+}
+
+
+## Launcher.
+def main(): Unit {
+
+  let sinkMb = new [SinkMb] in
+  spawn { sink(sinkMb) };
+
+  let actorMb1 = new [ActorMb] in # actorMb1: ?1
+  let actorMb2 = new [ActorMb] in # actorMb2: ?1
+  let actorMb3 = new [ActorMb] in # actorMb3: ?1
+  let exitMb1 = new [ExitMb] in # exitMb1: ?1
+  let exitMb2 = new [ExitMb] in # exitMb2: ?1
+  let exitMb3 = new [ExitMb] in # exitMb3: ?1
+
+  spawn { actor(actorMb1, exitMb1, 1, sinkMb) };
+  spawn { actor(actorMb2, exitMb2, 2, sinkMb) };
+  spawn { actor(actorMb3, exitMb3, 3, sinkMb) };
+
+  let xs = (exitMb1 :: (exitMb2 :: (exitMb3 :: (nil : List(ExitMb!))))) in sinkMb ! Actors(xs);
+
+  actorMb1 ! Neighbors(actorMb2, actorMb3); # actorMb1: ?Neighbors
+  actorMb2 ! Neighbors(actorMb1, actorMb3); # actorMb2: ?Neighbors
+  actorMb3 ! Neighbors(actorMb1, actorMb2); # actorMb3: ?Neighbors
+
+  actorMb1 ! Pong(0); # actorMb1: ?Neighbors . Pong
+  actorMb2 ! Pong(0); # actorMb2: ?Neighbors . Pong
+  actorMb3 ! Pong(0) # actorMb2: ?Neighbors . Pong
+}
+
+main()
diff --git a/test/examples/savina/lists/cig_smok.pat b/test/examples/savina/lists/cig_smok.pat
new file mode 100644
index 0000000..83c8cd3
--- /dev/null
+++ b/test/examples/savina/lists/cig_smok.pat
@@ -0,0 +1,149 @@
+### Adapted from Savina/cigsmok.
+###
+### A benchmark modelling n smokers and one arbiter that decides which smoker to
+### allow to smoke. The benchmark is parameterized by the number of smoker
+### processes.
+
+interface ArbiterMb {
+  Start(Int),
+  StartedSmoking()
+}
+
+interface SmokerMb {
+  StartSmoking(Int),
+  Exit()
+}
+
+def create_smokers(self: ArbiterMb?, moreSmokers: Int, acc: List(SmokerMb!)): (ArbiterMb? * List(SmokerMb!)) {
+    if (moreSmokers == 0) {
+        (self, acc)
+    }
+    else {
+        let newSmoker = new [SmokerMb] in
+            spawn { smoker(newSmoker, self) };
+            create_smokers(self, moreSmokers - 1, (newSmoker :: acc))
+        }
+}
+
+## Arbiter process handling the creation of smokers and launching of main loop.
+def arbiter(self: ArbiterMb?, numRounds: Int): Unit {
+
+  guard self: Start . (StartedSmoking*) {
+    receive Start(numSmokers) from self ->
+
+       let (self, smokerMbs) = create_smokers(self, numSmokers, (nil : List(SmokerMb!))) in
+
+        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
+        arbiter_loop(self, numSmokers, numRounds, smokerMbs)
+  }
+}
+
+## Randomly chooses the smoker and requests it to smoke.
+def notify_smoker(numSmokers: Int, smokerMbs: List(SmokerMb!)): List(SmokerMb!) {
+
+  let smokerId = rand(numSmokers - 1) in
+  let sleepTimeMs = 1000 in
+
+  notify_aux(smokerId, sleepTimeMs, smokerMbs)
+}
+
+def notify_aux(choice: Int, time: Int, smokerMbs: List(SmokerMb!)): List(SmokerMb!) {
+if (choice == 0) {
+    caseL smokerMbs : List(SmokerMb!)  of {
+        nil -> nil
+        | (mb :: mbs) ->
+            mb ! StartSmoking(rand(time));
+            (mb :: mbs)
+    }
+}
+else {
+    caseL smokerMbs : List(SmokerMb!) of {
+        nil -> nil
+        | (mb :: mbs) ->
+            let smokerMbs = notify_aux(choice - 1, time, mbs) in
+            (mb :: smokerMbs)
+    }
+}
+}
+
+## Notifies all smokers to terminate.
+def notify_smoker_exit(smokerMbs: List(SmokerMb!)): List(SmokerMb!) {
+    caseL smokerMbs : List(SmokerMb!) of {
+        nil -> nil
+        | (mb :: mbs) ->
+            mb ! Exit();
+            notify_smoker_exit(mbs)
+        }
+}
+
+## Arbiter process main loop issuing start smoking requests and handling started
+## smoking replies.
+def arbiter_loop(self: ArbiterMb?, numSmokers: Int, numRounds: Int, smokerMbs: List(SmokerMb!)): Unit {
+  guard self: StartedSmoking* {
+    free ->
+      caseL smokerMbs : List(SmokerMb!) of {
+      nil -> ()
+      | (a :: as) -> ()
+  }
+    receive StartedSmoking() from self ->
+
+      # The if here introduces the internal choice, which means that on the
+      # receiver side I might or might not receive the message. In this case,
+      # the smoker might or might nor receive the Exit message, and must either
+      # use (Exit + 1) or (*Exit) in its pattern.
+
+      if (numRounds <= 0) {
+        let smokerMbs = notify_smoker_exit(smokerMbs) in
+            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
+      }
+      else {
+        let smokerMbs = notify_smoker(numSmokers, smokerMbs) in
+            arbiter_loop(self, numSmokers, numRounds - 1, smokerMbs)
+      }
+
+      # Arbiter needs to service all requests before, even if it has sent the
+      # Exit messages to smokers. Remember that smokers may still be processing
+      # StartSmoking messages, but the arbiter has already issued Exit messages
+      # and it still needs to await all the StartedSmoking replies before
+      # terminating. This is why we do not have an exit_arbiter flush function.
+
+  }
+}
+
+## Smoker process main loop handling start smoking requests and issuing started
+## smoking replies to/from the arbiter.
+def smoker(self: SmokerMb?, arbiterMb: ArbiterMb!): Unit {
+  # Smoker may be asked to smoke more than once, or none. This is why the *.
+  guard self: (StartSmoking*) . (Exit*) {
+    free ->
+      () # Since the smoker might not even receive an Exit/StartSmoking message due to the if condition above.
+    receive StartSmoking(ms) from self ->
+      arbiterMb ! StartedSmoking();
+      sleep(ms);
+      smoker(self, arbiterMb)
+    receive Exit() from self ->
+      smoker_exit(self)
+  }
+}
+
+## Smoker process exit procedure that flushes potential residual messages.
+def smoker_exit(self: SmokerMb?): Unit {
+  guard self: (StartSmoking*) . (Exit*) {
+    free -> () # In case I have one or more Exit/StartSmoking messages due to the if condition above.
+    receive StartSmoking(ms) from self ->
+      smoker_exit(self)
+    receive Exit() from self ->
+      smoker_exit(self)
+  }
+}
+
+## Launcher.
+def main(numSmokers : Int): Unit {
+
+  let arbiterMb = new [ArbiterMb] in
+  spawn { arbiter(arbiterMb, 10) };
+
+  arbiterMb ! Start(numSmokers)
+}
+
+main(5)
diff --git a/test/examples/savina/lists/kfork.pat b/test/examples/savina/lists/kfork.pat
new file mode 100644
index 0000000..944e23e
--- /dev/null
+++ b/test/examples/savina/lists/kfork.pat
@@ -0,0 +1,69 @@
+### Adapted from Savina/fjthrput.
+###
+### Models the creation of n actors that are given a number of messages, for
+### each of which, a computation is performed. The benchmark is parameterized by
+### the number of actor processes.
+
+interface ActorMb {
+  Packet()
+}
+
+## Actor processes handling the packet requests.
+def actor(self: ActorMb?): Unit {
+  guard self: Packet* {
+    free ->
+      ()
+    receive Packet() from self ->
+      let dummy = fact(rand(100000)) in
+      actor(self)
+  }
+}
+
+## Computes the factorial of n.
+def fact(n: Int): Int {
+  if (n <= 0) {
+    1
+  }
+  else {
+    n * (fact(n - 1))
+  }
+}
+
+## Sends the given number of messages to the specified actor mailbox.
+def flood(numMessages: Int, actorMb: ActorMb!): Unit {
+  if (numMessages <= 0) {
+    ()
+  }
+  else {
+    actorMb ! Packet();
+    flood(numMessages - 1, actorMb)
+  }
+}
+
+def spawnActors(numActors: Int, acc: List(ActorMb!)): List(ActorMb!) {
+    if (numActors <= 0) {
+        acc
+    } else {
+        let newActor = new[ActorMb] in
+        spawn { actor(newActor) };
+        spawnActors(numActors - 1, (newActor :: acc))
+    }
+}
+
+def floodActors(numMessages: Int, actorMbs: List(ActorMb!)): Unit {
+    caseL actorMbs : List(ActorMb!) of {
+        nil -> ()
+      | (a :: as) ->
+            flood(numMessages, a);
+            floodActors(numMessages, as)
+        }
+}
+
+## Launcher.
+def main(numActors: Int): Unit {
+
+  let actorMbs = spawnActors(numActors, (nil : List(ActorMb!))) in
+    floodActors(1000, actorMbs)
+}
+
+main(3)
diff --git a/test/pat-tests/list-1.pat b/test/pat-tests/list-1.pat
new file mode 100644
index 0000000..996c699
--- /dev/null
+++ b/test/pat-tests/list-1.pat
@@ -0,0 +1,9 @@
+def main() : Unit {
+    let xs = (5 :: (nil : List(Int))) in
+    caseL xs : List(Int) of {
+          nil -> print("nil")
+        | (y :: ys) -> print(intToString(y))
+    }
+}
+
+main()
diff --git a/test/pat-tests/list-2.pat b/test/pat-tests/list-2.pat
new file mode 100644
index 0000000..d290227
--- /dev/null
+++ b/test/pat-tests/list-2.pat
@@ -0,0 +1,23 @@
+def snoc(xs : List(Int), x : Int): List(Int) {
+    caseL xs : List(Int) of {
+        nil -> (x :: (nil : List(Int)))
+      | (y :: ys) -> (y :: snoc(ys, x))
+    }
+}
+
+def reverse(xs : List(Int)): List(Int) {
+    caseL xs : List(Int) of {
+          nil -> nil
+        | (y :: ys) -> snoc(reverse(ys), y)
+    }
+}
+
+def main(): Unit {
+    let xs = (1 :: (2 :: (3 :: (nil : List(Int))))) in
+    caseL reverse(xs) : List(Int) of {
+        nil -> print("nil")
+      | (y :: ys) -> print(intToString(y))
+  }
+}
+
+main()
diff --git a/test/pat-tests/list-mb.pat b/test/pat-tests/list-mb.pat
new file mode 100644
index 0000000..95a6006
--- /dev/null
+++ b/test/pat-tests/list-mb.pat
@@ -0,0 +1,16 @@
+interface Test {
+  Ping()
+}
+
+def spawnMbs(acc : List(Test!)) : List(Test!) {
+    acc
+}
+
+def test(mbs : List(Test!)) : Unit {
+    ()
+}
+
+def main() : Unit {
+    let mbs = spawnMbs(nil : List(Test!)) in
+    test(mbs)
+}
diff --git a/test/tests.json b/test/tests.json
index ce43bae..5958e0a 100644
--- a/test/tests.json
+++ b/test/tests.json
@@ -103,6 +103,21 @@
                     "name": "n-tuples, bad (2)",
                     "filename": "pat-tests/n-tuples-bad-2.pat",
                     "exit_code": 1
+                },
+                {
+                    "name": "Lists (1)",
+                    "filename": "pat-tests/list-1.pat",
+                    "exit_code": 0
+                },
+                {
+                    "name": "Lists (2)",
+                    "filename": "pat-tests/list-2.pat",
+                    "exit_code": 0
+                },
+                {
+                    "name": "Lists (with mailboxes)",
+                    "filename": "pat-tests/list-mb.pat",
+                    "exit_code": 0
                 }
             ]
         },
@@ -136,10 +151,21 @@
                 {"name": "Thread Ring", "filename": "examples/savina/thread_ring.pat", "exit_code": 0}
             ]
         },
+        { "group": "Correct examples (Savina with lists)",
+          "tests":
+            [
+                {"name": "Banking (lists)", "filename": "examples/savina/lists/banking.pat", "exit_code": 0},
+                {"name": "Big (lists)", "filename": "examples/savina/lists/big.pat", "exit_code": 0},
+                {"name": "Cigarette Smoker (lists)", "filename": "examples/savina/lists/cig_smok.pat", "exit_code": 0},
+                {"name": "kfork (lists)", "filename": "examples/savina/lists/kfork.pat", "exit_code": 0},
+                {"name": "Sleeping Barber", "filename": "examples/savina/lists/barber.pat", "exit_code": 0}
+            ]
+        },
         { "group": "Correct examples (Others)",
           "tests":
             [
                 {"name": "n-Robots", "filename": "examples/robotsn.pat", "exit_code": 0},
+                {"name": "n-Robots (lists)", "filename": "examples/robotsn-lists.pat", "exit_code": 0},
                 {"name": "Guard annotation is a subpattern", "filename": "examples/pat_constr.pat", "exit_code": 0}
             ]
         },
@@ -179,6 +205,11 @@
                     "filename": "errors/uaf3.pat",
                     "exit_code": 1
                 },
+                {
+                    "name": "Use after free (lists)",
+                    "filename": "errors/uaf_lists.pat",
+                    "exit_code": 1
+                },
                 {"name": "Insufficient type information", "filename": "errors/pat_constr.pat", "exit_code": 1},
                 {"name": "Non-exhaustive guards", "filename": "errors/pat_constr2.pat", "exit_code": 1},
                 {"name": "Additional non-supported non-fail guard with nontrivial continuation", "filename": "errors/pat_constr3.pat", "exit_code": 1},