diff --git a/lib/common/interface.ml b/lib/common/interface.ml
index dd770c8..ad3b116 100644
--- a/lib/common/interface.ml
+++ b/lib/common/interface.ml
@@ -1,7 +1,11 @@
 open Common_types
 open Util.Utility
 
-type t = { name: string; env: (string * (Type.t[@name "ty"]) list) list }
+type t = {
+  name: string;
+  typarams: (Type.t[@name "ty"]) list;
+  env: (string * (Type.t[@name "ty"]) list) list
+}
 [@@name "interface"]
 [@@deriving visitors {
     variety = "map";
@@ -19,11 +23,13 @@ let lookup ?(pos_list=[]) (x: tag) (iface: t) =
             in
             raise (Errors.Type_error (msg, pos_list))
 
-let make name env =
-    { name; env }
+let make name typarams env =
+    { name; typarams; env }
 
 let name x = x.name
 
+let typarams x = x.typarams
+
 let bindings x = x.env
 
 let pp ppf x =
@@ -33,7 +39,8 @@ let pp ppf x =
             pp_print_string name
             (pp_print_comma_list Type.pp) tys
     in
-    fprintf ppf "interface %a { %a }"
+    fprintf ppf "interface %a <%a> { %a }"
         pp_print_string x.name
+        (pp_print_list Type.pp) x.typarams
         (pp_print_comma_list pp_message)
         x.env
diff --git a/lib/common/ir.ml b/lib/common/ir.ml
index c659c71..32935d6 100644
--- a/lib/common/ir.ml
+++ b/lib/common/ir.ml
@@ -66,6 +66,7 @@ type program = {
 }
 and decl = {
     decl_name: (Binder.t[@name "binder"]);
+    typarams : (Type.t[@name "ty"]) list;
     decl_parameters: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) list;
     decl_return_type: (Type.t[@name "ty"]);
     decl_body: comp
@@ -82,6 +83,7 @@ and comp_node =
     | Return of value
     | App of {
         func: value;
+        tyargs: (Type.t[@name "ty"]) list;
         args: value list
       }
     | If of { test: value; then_expr: comp; else_expr: comp }
@@ -97,19 +99,19 @@ and comp_node =
         branch1: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp;
         branch2: ((Binder.t[@name "binder"]) * (Type.t[@name "ty"])) * comp
     }
-    | New of string
+    | New of (string * (Type.t[@name "ty"]) list)
     | Spawn of comp
     | Send of {
         target: value;
         message: (message[@name "msg"]);
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
       }
-    | Free of (value * string option)
+    | Free of (value * (string * (Type.t[@name "ty"]) list) option)
     | Guard of {
         target: value;
         pattern: (Type.Pattern.t[@name "pattern"]);
         guards: guard list;
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
       }
 and value = (value_node WithPos.t [@name "withP"])
 and value_node =
@@ -170,9 +172,10 @@ and pp_interface ppf iface =
         (pp_print_comma_list pp_msg_ty) xs
 (* Declarations *)
 and pp_decl ppf decl_with_pos =
-    let { WithPos.node = { decl_name; decl_parameters; decl_return_type; decl_body }; _ } = decl_with_pos in
-    fprintf ppf "def %a(%a): %a {@,@[<v 2>  %a@]@,}"
+  let { WithPos.node = { decl_name; typarams; decl_parameters; decl_return_type; decl_body }; _ } = decl_with_pos in
+    fprintf ppf "def %a<%a>(%a): %a {@,@[<v 2>  %a@]@,}"
         Binder.pp decl_name
+        (pp_print_list Type.pp) typarams
         (pp_print_comma_list pp_param) decl_parameters
         Type.pp decl_return_type
         pp_comp decl_body
@@ -210,11 +213,12 @@ and pp_comp ppf comp_with_pos =
             pp_value test
             pp_comp then_expr
             pp_comp else_expr
-    | App { func; args } ->
-        fprintf ppf "%a(%a)"
+    | App { func; tyargs; args } ->
+        fprintf ppf "%a<%a>(%a)"
             pp_value func
+            (pp_print_list Type.pp) tyargs
             (pp_print_comma_list pp_value) args
-    | New iname -> fprintf ppf "new[%s]" iname
+    | New (iname, _) -> fprintf ppf "new[%s]" iname
     | Spawn e -> fprintf ppf "spawn {@[<v>@,%a@]@,}" pp_comp e
     | Send { target; message; _ (* iname *) } ->
         (* Special-case the common case of sending to a variable.
diff --git a/lib/common/lib_types.ml b/lib/common/lib_types.ml
index 6366726..11688dc 100644
--- a/lib/common/lib_types.ml
+++ b/lib/common/lib_types.ml
@@ -6,9 +6,9 @@ open Common_types
 let signatures =
     let open Type in
     let open Base in
-    let int_op_type = function_type false [Base Int; Base Int] (Base Int) in
-    let int_rel_op_type = function_type false [Base Int; Base Int] (Base Bool) in
-    let bool_rel_op_type = function_type false [Base Bool; Base Bool] (Base Bool) in
+    let int_op_type = function_type false [] [Base Int; Base Int] (Base Int) in
+    let int_rel_op_type = function_type false [] [Base Int; Base Int] (Base Bool) in
+    let bool_rel_op_type = function_type false [] [Base Bool; Base Bool] (Base Bool) in
     let int_ops =
         List.map (fun x -> (x, int_op_type)) ["+"; "-"; "/"; "*"]
     in
@@ -20,9 +20,9 @@ let signatures =
     in
     int_ops @ int_rel_ops @ bool_rel_ops @
     [
-        ("print", function_type false [Base Base.String] Type.unit_type);
-        ("concat", function_type false [Base Base.String; Base Base.String] Type.string_type);
-        ("rand", function_type false [Base Base.Int] (Base Base.Int));
-        ("sleep", function_type false [Base Base.Int] Type.unit_type);
-        ("intToString", function_type false [Base Base.Int] (Base Base.String))
+      ("print", function_type false [] [Base Base.String] Type.unit_type);
+      ("concat", function_type false [] [Base Base.String; Base Base.String] Type.string_type);
+      ("rand", function_type false [] [Base Base.Int] (Base Base.Int));
+      ("sleep", function_type false [] [Base Base.Int] Type.unit_type);
+      ("intToString", function_type false [][Base Base.Int] (Base Base.String))
     ]
diff --git a/lib/common/pretype.ml b/lib/common/pretype.ml
index 16d5af8..bd17eea 100644
--- a/lib/common/pretype.ml
+++ b/lib/common/pretype.ml
@@ -9,8 +9,9 @@ open Util.Utility
 
 type t =
     | PBase of base
-    | PFun of { linear: bool; args: (Type.t[@name "ty"]) list; result: (Type.t[@name "ty"]) }
-    | PInterface of string
+    | PVar of string
+    | PFun of { linear: bool; typarams: (Type.t[@name "ty"]) list; args: (Type.t[@name "ty"]) list; result: (Type.t[@name "ty"]) }
+    | PInterface of (string * (Type.t[@name "ty"]) list)
     | PSum of (t * t)
     | PTuple of t list
     [@@name "pretype"]
@@ -21,12 +22,13 @@ let unit = PTuple []
 
 let rec pp ppf =
   let open Format in
-  let ps = pp_print_string ppf in
   function
     | PBase b -> Common_types.Base.pp ppf b
-    | PFun { linear; args; result } ->
+    | PVar s -> fprintf ppf "%s" s
+    | PFun { linear; typarams; args; result } ->
         let arrow = if linear then "-o" else "->" in
-        fprintf ppf "(%a) %s %a"
+        fprintf ppf "<%a> (%a) %s %a"
+            (pp_print_list Type.pp) typarams
             (pp_print_comma_list Type.pp) args
             arrow
             Type.pp result
@@ -38,7 +40,10 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
-    | PInterface name -> ps name
+    | PInterface (iname, tyargs) ->
+        fprintf ppf "%s<%a>"
+            iname
+            (pp_print_list Type.pp) tyargs
 
 let show t =
   let open Format in
@@ -47,8 +52,9 @@ let show t =
 
 let rec of_type = function
     | Type.Base b -> PBase b
-    | Type.Fun { linear; args; result } ->
-        PFun { linear; args; result = result }
+    | Type.TVar s -> PVar s
+    | Type.Fun { linear; typarams; args; result } ->
+        PFun { linear; typarams; args; result = result }
     | Type.Tuple ts -> PTuple (List.map of_type ts)
     | Type.Sum (t1, t2) -> PSum (of_type t1, of_type t2)
     | Type.Mailbox { interface; _ } -> PInterface interface
@@ -59,8 +65,9 @@ let rec of_type = function
     when trying to type an application in synthesis mode). *)
 let rec to_type = function
     | PBase b -> Some (Type.Base b)
-    | PFun { linear; args; result } ->
-        Some (Type.Fun { linear; args; result })
+    | PVar s -> Some (Type.TVar s)
+    | PFun { linear; typarams; args; result } ->
+        Some (Type.Fun { linear; typarams; args; result })
     | PTuple ts ->
         let rec go acc =
             function
diff --git a/lib/common/sugar_ast.ml b/lib/common/sugar_ast.ml
index ebd1d1a..a37c3d0 100644
--- a/lib/common/sugar_ast.ml
+++ b/lib/common/sugar_ast.ml
@@ -28,6 +28,7 @@ and expr_node =
     | Seq of expr * expr
     | App of {
         func: expr;
+        tyargs: (Type.t[@name "ty"]) list;
         args: expr list
     }
     | If of { test: expr; then_expr: expr; else_expr: expr }
@@ -51,20 +52,20 @@ and expr_node =
        not wired to their continuations. I've experimented with the
        bidirectional rules and it seems that this does not pose any problems. *)
     (* That said, we may revisit this later when we look at deadlock detection. *)
-    | New of string (* interface name *)
+    | New of (string * (Type.t[@name "ty"]) list) (* interface name *)
     | Spawn of expr
     (* interface names for Send and Guard will be added after pre-type checking *)
     | Send of {
         target: expr;
         message: (string * (expr list));
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
     }
     | Guard of {
         target: expr;
         (* At least at the moment, each guard must be annotated with a pattern *)
         pattern: (Type.Pattern.t [@name "pattern"]);
         guards: guard list;
-        iname: string option
+        iface: (string * (Type.t[@name "ty"]) list) option
     }
     | Free of expr
     (* fail(e)[A], desugars to (guard e : 0 { fail } : A) *)
@@ -91,6 +92,7 @@ and guard_node =
     | Fail of (Type.t[@name "ty"])
 and decl = {
     decl_name: string;
+    typarams: (Type.t[@name "ty"]) list;
     decl_parameters: (string * (Type.t[@name "ty"])) list;
     decl_return_type: (Type.t[@name "ty"]);
     decl_body: expr
@@ -141,11 +143,12 @@ and pp_interface ppf iface =
         (pp_print_comma_list pp_msg_ty) xs
 (* Declarations *)
 and pp_decl ppf decl =
-    let  { decl_name; decl_parameters; decl_return_type; decl_body } =
+  let  { decl_name; typarams; decl_parameters; decl_return_type; decl_body } =
         WithPos.node decl
     in
-    fprintf ppf "def %s(%a): %a {@,@[<v 2>  %a@]@,}"
+    fprintf ppf "def %s<%a>(%a): %a {@,@[<v 2>  %a@]@,}"
       decl_name
+      (pp_print_list Type.pp) typarams
       (pp_print_comma_list pp_param) decl_parameters
       Type.pp decl_return_type
       pp_expr decl_body
@@ -193,11 +196,12 @@ and pp_expr ppf expr_with_pos =
             pp_expr else_expr
     | Seq (e1, e2) ->
         fprintf ppf "(%a;@,%a)" pp_expr e1 pp_expr e2
-    | App { func; args } ->
-        fprintf ppf "%a(%a)"
+    | App { func; tyargs; args } ->
+        fprintf ppf "%a<%a>(%a)"
             pp_expr func
+            (pp_print_list Type.pp) tyargs
             (pp_print_comma_list pp_expr) args
-    | New iname -> fprintf ppf "new[%s]" iname
+    | New (iname, _) -> fprintf ppf "new[%s]" iname
     | Spawn e -> fprintf ppf "spawn {@[<v>@,%a@]@,}" pp_expr e
     | Send { target; message; _ (* iname *) } ->
         (* Special-case the common case of sending to a variable.
diff --git a/lib/common/type.ml b/lib/common/type.ml
index 7e5097f..27ca449 100644
--- a/lib/common/type.ml
+++ b/lib/common/type.ml
@@ -249,13 +249,14 @@ module Pattern = struct
 end
 
 type t =
+    | TVar of string
     | Base of base
-    | Fun of { linear: bool; args: t list; result: t }
+    | Fun of { linear: bool; typarams: t list; args: t list; result: t }
     | Tuple of t list
     | Sum of (t * t)
     | Mailbox of {
         capability: (Capability.t [@name "capability"]);
-        interface: string;
+        interface: (string * t list);
         (* A mailbox type can either be returnable or usable.
            A returnable mailbox name can be used for all purposes (can be
            returned from subexpressions, can be sent upon, can be received
@@ -296,8 +297,8 @@ let string_type = Base Base.String
 let bool_type = Base Base.Bool
 let unit_type = Tuple []
 let atom = Base Base.Atom
-let function_type linear args result =
-    Fun { linear; args; result }
+let function_type linear typarams args result =
+    Fun { linear; typarams; args; result }
 
 let mailbox_send_unit interface quasilinearity =
     Mailbox {
@@ -311,9 +312,11 @@ let rec pp ppf =
   let open Format in
   function
     | Base b -> Base.pp ppf b
-    | Fun { linear; args; result } ->
+    | TVar s -> fprintf ppf "%s" s
+    | Fun { linear; typarams; args; result } ->
         let arrow = if linear then "-o" else "->" in
-        fprintf ppf "(%a) %s %a"
+        fprintf ppf "<%a> (%a) %s %a"
+            (pp_print_list pp) typarams
             (pp_print_comma_list pp) args
             arrow
             pp result
@@ -325,7 +328,7 @@ let rec pp ppf =
         fprintf ppf "(%a + %a)"
             pp t1
             pp t2
-    | Mailbox { capability; interface; pattern; quasilinearity } ->
+    | Mailbox { capability; interface=(iname, tyargs); pattern; quasilinearity } ->
         let ql =
             match quasilinearity with
                 | Quasilinearity.Returnable -> "R"
@@ -336,8 +339,9 @@ let rec pp ppf =
                 | Capability.In -> "?"
                 | Capability.Out -> "!"
         in
-        fprintf ppf "%s%s(%a)[%s]"
-            interface
+        fprintf ppf "%s<%a>%s(%a)[%s]"
+            iname
+            (pp_print_list pp) tyargs
             op
             (pp_print_option pp_pattern) pattern
             ql
@@ -353,6 +357,7 @@ let show t =
 
 let rec is_lin = function
     | Base _ -> false
+    | TVar _ -> false
     | Fun { linear; _ } -> linear
     (* !1 is unrestricted... *)
     | Mailbox { capability = Out; pattern = Some One; _ } -> false
@@ -411,8 +416,8 @@ let rec is_returnable = function
     | Sum  (t1, t2) -> is_returnable t1 && is_returnable t2
     | _ -> true
 
-let make_function_type linear args result =
-    Fun { linear; args; result }
+let make_function_type linear typarams args result =
+    Fun { linear; typarams; args; result }
 
 let make_tuple_type tys =
     Tuple (List.map make_returnable tys)
diff --git a/lib/frontend/desugar_sugared_guards.ml b/lib/frontend/desugar_sugared_guards.ml
index 19c5ab2..a2b29bb 100644
--- a/lib/frontend/desugar_sugared_guards.ml
+++ b/lib/frontend/desugar_sugared_guards.ml
@@ -30,7 +30,7 @@ let visitor =
                 target = new_target;
                 pattern = Type.Pattern.Zero;
                 guards = [WithPos.make ~pos:(WithPos.pos new_target) (Fail ty)];
-                iname = None
+                iface = None
               } in
               let new_expr_node = Annotate (WithPos.make ~pos:(WithPos.pos new_target) new_guard, ty) in
               { expr_with_pos with node = new_expr_node }
diff --git a/lib/frontend/insert_pattern_variables.ml b/lib/frontend/insert_pattern_variables.ml
index a18f9d6..22d60f2 100644
--- a/lib/frontend/insert_pattern_variables.ml
+++ b/lib/frontend/insert_pattern_variables.ml
@@ -12,9 +12,11 @@ let rec annotate_type =
     let open Type in
     function
         | Base t -> Base t
-        | Fun { linear; args; result } ->
+        | TVar s -> TVar s
+        | Fun { linear; typarams; args; result } ->
             Fun {
                 linear;
+                typarams;
                 args = List.map annotate_type args;
                 result = annotate_type result
             }
@@ -49,7 +51,7 @@ let annotate_interface_type =
 let annotate_interface iface =
     Interface.bindings iface
     |> List.map (fun (tag, tys) -> (tag, List.map annotate_interface_type tys))
-    |> Interface.(make (name iface))
+    |> Interface.(make (name iface) (typarams iface))
 
 (* The visitor traverses the AST to annotate parameters of higher-order
    functions. *)
diff --git a/lib/frontend/parser.mly b/lib/frontend/parser.mly
index 8971b26..413e9eb 100644
--- a/lib/frontend/parser.mly
+++ b/lib/frontend/parser.mly
@@ -31,7 +31,7 @@ let with_pos_from_positions p1 p2 newE = ParserPosition.with_pos (p1, p2) newE
 
 let parse_error x pos_list = Errors.Parse_error (x,pos_list)
 
-let binary_op op_name x1 x2 = App { func = ParserPosition.with_pos ((get_start_pos x1),(get_end_pos x2)) (Primitive op_name); args = [x1; x2] }
+let binary_op op_name x1 x2 = App { func = ParserPosition.with_pos ((get_start_pos x1),(get_end_pos x2)) (Primitive op_name); tyargs=[]; args = [x1; x2] }
 
 
 %}
@@ -153,7 +153,7 @@ basic_expr:
     | 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} )}
     (* New *)
-    | NEW LEFT_BRACK interface_name RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( New $3 )}
+    | NEW LEFT_BRACK param_interface RIGHT_BRACK { with_pos_from_positions $startpos $endpos ( New $3 )}
     (* Spawn *)
     | SPAWN LEFT_BRACE expr RIGHT_BRACE { with_pos_from_positions $startpos $endpos ( Spawn $3 )}
     (* Free *)
@@ -162,10 +162,11 @@ basic_expr:
     | 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 ) }
     (* App *)
-    | fact LEFT_PAREN expr_list RIGHT_PAREN
+    | fact typarams? LEFT_PAREN expr_list RIGHT_PAREN
         { with_pos_from_positions $startpos $endpos (
             App {   func = with_pos_from_positions $startpos $endpos ($1);
-                    args = $3 } 
+                    tyargs = (match $2 with Some ts -> ts | None -> []);
+                    args = $4 } 
         )}
     (* Lam *)
     | linearity LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr RIGHT_BRACE
@@ -175,7 +176,7 @@ basic_expr:
         { with_pos_from_positions $startpos $endpos( 
             Send {  target = with_pos_from_positions $startpos $endpos ($1); 
                     message = $3; 
-                    iname = None 
+                    iface = None 
             }
         )}
     (* If-Then-Else *)
@@ -188,7 +189,7 @@ basic_expr:
                 target = $2;
                 pattern = $4;
                 guards = $6;
-                iname = None
+                iface = None
             }
         )}
     | op { with_pos_from_positions $startpos $endpos ( $1 )}
@@ -251,46 +252,49 @@ parenthesised_datatypes:
     | LEFT_PAREN ty_list RIGHT_PAREN { $2 }
 
 ty:
-    | parenthesised_datatypes RIGHTARROW simple_ty  { Type.Fun { linear = false; args = $1; result = $3} }
-    | parenthesised_datatypes LOLLI simple_ty       { Type.Fun { linear = true;  args = $1; result = $3} }
+    | parenthesised_datatypes RIGHTARROW simple_ty  { Type.Fun { linear = false; typarams = []; args = $1; result = $3} }
+    | parenthesised_datatypes LOLLI simple_ty       { Type.Fun { linear = true; typarams = []; 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 }
     | simple_ty { $1 }
 
-interface_name:
-    | CONSTRUCTOR { $1 }
+typarams:
+| LEFT_BRACK separated_list(COMMA, ty) RIGHT_BRACK { $2 }
+
+param_interface:
+| CONSTRUCTOR typarams? { match $2 with Some ts -> ($1, ts) | None -> ($1, []) }
 
 pat:
-    | star_pat PLUS pat { Type.Pattern.Plus ($1, $3) }
-    | star_pat DOT pat  { Type.Pattern.Concat ($1, $3) }
-    | star_pat          { $1 }
+| star_pat PLUS pat { Type.Pattern.Plus ($1, $3) }
+| star_pat DOT pat  { Type.Pattern.Concat ($1, $3) }
+| star_pat          { $1 }
 
 star_pat:
-    | simple_pat STAR   { Type.Pattern.Many $1 }
-    | simple_pat        { $1 }
+| simple_pat STAR   { Type.Pattern.Many $1 }
+| simple_pat        { $1 }
 
 simple_pat:
-    | CONSTRUCTOR { Type.Pattern.Message $1 }
-    | INT {
-            match $1 with
-                | 0 -> Type.Pattern.Zero
-                | 1 -> Type.Pattern.One
-                | _ -> 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 }
-
-ql:
-    | LEFT_BRACK CONSTRUCTOR RIGHT_BRACK {
-        match $2 with
-            | "R" -> Type.Quasilinearity.Returnable
-            | "U" -> Type.Quasilinearity.Usable
-            | _ -> raise (parse_error "Invalid usage: expected U or R." 
+| CONSTRUCTOR { Type.Pattern.Message $1 }
+| INT {
+        match $1 with
+            | 0 -> Type.Pattern.Zero
+            | 1 -> Type.Pattern.One
+            | _ -> 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 }
+
+ql:
+| LEFT_BRACK CONSTRUCTOR RIGHT_BRACK {
+    match $2 with
+        | "R" -> Type.Quasilinearity.Returnable
+        | "U" -> Type.Quasilinearity.Usable
+        | _ -> raise (parse_error "Invalid usage: expected U or R." 
+                        [Position.make ~start:$startpos ~finish:$endpos ~code:!source_code_instance])
+}
 
 mailbox_ty:
-    | CONSTRUCTOR BANG simple_pat? ql? {
+| param_interface BANG simple_pat? ql? {
         let quasilinearity =
             Option.value $4 ~default:(Type.Quasilinearity.Usable)
         in
@@ -301,7 +305,7 @@ mailbox_ty:
             quasilinearity
         })
     }
-    | CONSTRUCTOR QUERY simple_pat? ql? {
+    | param_interface QUERY simple_pat? ql? {
         let quasilinearity =
             Option.value $4 ~default:(Type.Quasilinearity.Returnable)
         in
@@ -325,8 +329,7 @@ base_ty:
             | "Int" -> Type.Base Base.Int
             | "Bool" -> Type.Base Base.Bool
             | "String" -> Type.Base Base.String
-            | _ -> raise (parse_error "Expected Atom, Int, Bool, or String"
-                            [Position.make ~start:$startpos ~finish:$endpos ~code:!source_code_instance])
+            | s -> Type.TVar s
     }
 
 message_ty:
@@ -342,18 +345,19 @@ annotated_var_list:
     | separated_list(COMMA, annotated_var)  { $1 }
 
 interface:
-    | INTERFACE interface_name LEFT_BRACE message_list RIGHT_BRACE 
-        { with_pos_from_positions $startpos $endpos ( Interface.make $2 $4)  }
+    | INTERFACE param_interface LEFT_BRACE message_list RIGHT_BRACE 
+        { with_pos_from_positions $startpos $endpos ( Interface.make (fst $2) (snd $2) $4)  }
 
 decl:
-    | DEF VARIABLE LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr
+    | DEF VARIABLE typarams? LEFT_PAREN annotated_var_list RIGHT_PAREN COLON ty LEFT_BRACE expr
     RIGHT_BRACE {
         with_pos_from_positions $startpos $endpos ( 
         {
           decl_name = $2;
-          decl_parameters = $4;
-          decl_return_type = $7;
-          decl_body = $9
+          typarams = (match $3 with Some ts -> ts | None -> []);
+          decl_parameters = $5;
+          decl_return_type = $8;
+          decl_body = $10
         })
     }
 
diff --git a/lib/frontend/sugar_to_ir.ml b/lib/frontend/sugar_to_ir.ml
index 38e31a4..7b205c7 100644
--- a/lib/frontend/sugar_to_ir.ml
+++ b/lib/frontend/sugar_to_ir.ml
@@ -67,10 +67,11 @@ and transform_decl :
     Sugar_ast.decl ->
     Ir.Binder.t ->
         (env -> Ir.decl -> Ir.decl) -> Ir.decl =
-            fun env {decl_parameters; decl_return_type; decl_body; _} decl_binder k ->
+      fun env {decl_parameters; typarams; decl_return_type; decl_body; _} decl_binder k ->
     let (bnds, env') = add_names env fst decl_parameters in
     {
         decl_name = decl_binder;
+        typarams;
         decl_parameters = List.combine bnds (List.map snd decl_parameters);
         decl_return_type;
         decl_body = transform_expr env' decl_body id
@@ -175,10 +176,10 @@ and transform_expr :
                 | Ir.Return ({ node = Ir.Tuple []; _ }) ->
                     transform_expr env e2 k
                 | _ -> WithPos.make ~pos:pos' (Ir.Seq (c1, transform_expr env e2 k)))
-        | App {func; args} ->
+        | App {func; tyargs; args} ->
             transform_subterm env func (fun env funcv ->
             transform_list env args (fun argvs ->
-                with_same_pos (Ir.App { func = funcv; args = argvs })) k)
+                  with_same_pos (Ir.App { func = funcv; tyargs; args = argvs })) k)
         | If {test; then_expr; else_expr} ->
                 transform_subterm env test (fun env v ->
                 with_same_pos (
@@ -186,11 +187,11 @@ and transform_expr :
                     test = v;
                     then_expr = transform_expr env then_expr id;
                     else_expr = transform_expr env else_expr id }) |> k env)
-        | New i -> with_same_pos (Ir.New i) |> k env
+        | New iface -> with_same_pos (Ir.New iface) |> k env
         | Spawn e -> with_same_pos (Ir.Spawn (transform_expr env e id)) |> k env
         | Free e ->
             transform_subterm env e (fun _ v -> with_same_pos (Ir.Free (v, None))) |> k env
-        | Send {target; message; iname} ->
+        | Send {target; message; iface} ->
             let (tag, payloads) = message in
             transform_subterm env target (fun env pid ->
                 transform_list env payloads (fun payload_vs ->
@@ -198,8 +199,8 @@ and transform_expr :
                     Ir.Send {
                         target = pid;
                         message = (tag, payload_vs);
-                        iname })) k)
-        | Guard {target; pattern; guards; iname} ->
+                        iface })) k)
+        | Guard {target; pattern; guards; iface} ->
             transform_subterm env target (fun env v ->
                 let gs = List.map (fun x -> transform_guard env x) guards in
                 with_same_pos (
@@ -207,7 +208,7 @@ and transform_expr :
                     target = v;
                     pattern;
                     guards = gs;
-                    iname
+                    iface
                 }) |> k env )
         |  SugarFail (_, _) -> (* shouldn't ever match *)
                 raise (Errors.internal_error "sugar_to_ir.ml" "Encountered SugarFree/SugarFail expression during the IR translation stage")
diff --git a/lib/typecheck/gen_constraints.ml b/lib/typecheck/gen_constraints.ml
index 5c9a344..2c2ee38 100644
--- a/lib/typecheck/gen_constraints.ml
+++ b/lib/typecheck/gen_constraints.ml
@@ -60,8 +60,8 @@ let rec synthesise_val :
                         ty, Ty_env.singleton v ty, Constraint_set.empty
                     (* In limited circumstances we can use a pretype annotation to
                        synthesise a function *)
-                    | _, PFun { linear; args; result } ->
-                        let ty = Type.function_type linear args result in
+                    | _, PFun { linear; typarams; args; result } ->
+                        let ty = Type.function_type linear typarams args result in
                         ty, Ty_env.singleton v ty, Constraint_set.empty
                     | _, _ ->
                         Gripers.synth_variable v [pos]
@@ -134,7 +134,7 @@ let rec synthesise_val :
             let constrs = Constraint_set.union_many
                 [body_constrs; parameter_constrs; unr_constrs]
             in
-            let ty = Type.function_type linear parameter_tys result_type in
+            let ty = Type.function_type linear [] parameter_tys result_type in
             (ty, returnable_env, constrs)
         | _ -> Gripers.cannot_synthesise_value v [pos]
 and check_val :
@@ -146,7 +146,8 @@ and check_val :
         let open Type in
         let open Pretype in
         match ty, pty with
-            | Mailbox { interface; _ }, PInterface iname when interface = iname -> ()
+            | TVar s1, PVar s2 when s1 = s2 -> ()
+            | Mailbox { interface; _ }, PInterface iface when interface = iface -> ()
             | Base b1, PBase b2 when b1 = b2 -> ()
             | Fun _, PFun _ -> 
                 (* Function pretypes are now fully typed, so any errors will be
@@ -241,14 +242,17 @@ and synthesise_comp :
             (Type.unit_type, env, constrs)
         | Free (_, None) -> assert false
         (* Application is a synthesis case, since functions are always annotated. *)
-        | App { func; args } ->
+        | App { func; tyargs; args } ->
             (* Synthesise the type for the function.
                Note that the function will always be annotated. *)
+            let _ = tyargs in
             let fun_ty, fun_env, fun_constrs = synthesise_val ienv decl_env func in
             let arg_tys, result_ty =
                 match fun_ty with
-                    | Type.Fun { args; result; _ } ->
-                        (args, result)
+                    | Type.Fun { typarams; args; result; _ } ->
+                        let args' = List.map (Type_utils.substitute_types typarams tyargs) args in
+                        let result' = Type_utils.substitute_types typarams tyargs result in
+                        (args', result')
                     | ty -> Gripers.expected_function func ty [pos]
             in
             (* Check that all argument types are compatible with the annotation *)
@@ -276,20 +280,22 @@ and synthesise_comp :
                 [fun_constrs; arg_constrs; env_constrs]
             in
             (result_ty, env, constrs)
-        | Send { target; message = (tag, payloads) ; iname } ->
+        | Send { target; message = (tag, payloads) ; iface } ->
             let open Type in
             (* Option.get safe since interface name will have been filled in
                by pre-type checking *)
-            let iname = Option.get iname in
+            let (iname, tyargs) = Option.get iface in
             let interface_withPos = IEnv.lookup iname ienv [pos] in
+            let typarams = Interface.typarams (WithPos.node interface_withPos) in
             let payload_types =
                 Interface.lookup ~pos_list:[WithPos.pos interface_withPos; pos] tag (WithPos.node interface_withPos)
+                |> List.map (Type_utils.substitute_types typarams tyargs)
             in
             (* Check target has correct output type *)
             let target_ty =
                 Mailbox {
                     capability = Out;
-                    interface = iname;
+                    interface = (iname, tyargs);
                     pattern = Some (Message tag);
                     (* 'Send' gives the MB type the least specific
                        quasilinearity (Usable). It can be coerced to Returnable
@@ -601,18 +607,18 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
             in
             let env = Ty_env.delete_many bnd_vars env in
             (env, constrs)
-        | Guard { iname = None; _ } -> (* Should have been filled in by pre-typing *)
+        | Guard { iface = None; _ } -> (* Should have been filled in by pre-typing *)
             assert false
-        | Guard { target; pattern; guards; iname = Some iname } ->
+        | Guard { target; pattern; guards; iface = Some (iname, tyargs) } ->
             let open Type in
             (* Check guard types, and generate constraints, and pattern for guards *)
             let (guards_env, guards_pat, guards_constrs) =
-                check_guards ienv decl_env iname pattern guards ty in
+                check_guards ienv decl_env (iname, tyargs) pattern guards ty in
             (* Check to see whether the MB handle can be given a type that's
                compatible with the synthesised pattern. *)
             let target_ty = Mailbox {
                 capability = In;
-                interface = iname;
+                interface = (iname, tyargs);
                 pattern = Some guards_pat;
                 (* We can only receive on a Returnable guard (since the name
                    goes out of scope afterwards) *)
@@ -655,9 +661,9 @@ and check_comp : IEnv.t -> Ty_env.t -> Ir.comp -> Type.t -> Ty_env.t * Constrain
 (* Synthesises types for all guards, checks that their types are compatible, and
  * returns the intersection of the resulting environments and generated pattern. *)
 and check_guards :
-    IEnv.t -> Ty_env.t -> interface_name -> Type.Pattern.t -> Ir.guard list ->
+    IEnv.t -> Ty_env.t -> (interface_name * Type.t list) -> Type.Pattern.t -> Ir.guard list ->
         Type.t -> Nullable_env.t * Type.Pattern.t * Constraint_set.t =
-        fun ienv decl_env iname guard_pat gs ty ->
+        fun ienv decl_env (iname, typarams) guard_pat gs ty ->
           let open Ir in
           let open Type in
           (* Do a duplication check on guards *)
@@ -688,7 +694,7 @@ and check_guards :
           List.fold_left (fun (env, pat, acc_constrs) g ->
             (* TC Guard *)
             let (g_env, g_pat, g_constrs) =
-              check_guard ienv decl_env iname guard_pat g ty
+              check_guard ienv decl_env (iname, typarams) guard_pat g ty
             in
             (* Calculate environment intersection *)
             let (env, env_constrs) = Nullable_env.intersect g_env env (WithPos.pos g) in
@@ -701,9 +707,9 @@ and check_guards :
 (* Checks the type for a single guard, returning type, environment, pattern,
    and constraint set. *)
 and check_guard :
-    IEnv.t -> Ty_env.t -> interface_name -> Type.Pattern.t -> Ir.guard -> Type.t ->
+    IEnv.t -> Ty_env.t -> (interface_name * Type.t list) -> Type.Pattern.t -> Ir.guard -> Type.t ->
         Nullable_env.t * Type.Pattern.t * Constraint_set.t =
-        fun ienv decl_env iname pat g ty ->
+        fun ienv decl_env (iname, typarams) pat g ty ->
           let open Ir in
           let open Type in
           let pos = WithPos.pos g in
@@ -794,7 +800,7 @@ and check_guard :
                                 match ty with
                                     | Mailbox { interface; _ } when (List.mem interface mb_iface_tys) ->
                                         Gripers.duplicate_interface_receive_env
-                                        v interface 
+                                        v (fst interface)
                                         [pos]
                                     | _ -> ()
                             ) env
@@ -822,7 +828,7 @@ and check_guard :
                 let goal =
                     Type.Mailbox {
                         capability = Capability.In;
-                        interface = iname;
+                        interface = (iname, typarams);
                         pattern = Some One;
                         quasilinearity = Quasilinearity.Returnable;
                     }
@@ -865,7 +871,7 @@ let check_decls ienv decls =
         let decl_entry d =
             let args = List.map snd d.decl_parameters in
             Var.of_binder d.decl_name,
-            Type.make_function_type false args d.decl_return_type
+            Type.make_function_type false d.typarams args d.decl_return_type
         in
         List.map decl_entry decl_nodes
         |> Ty_env.from_list
diff --git a/lib/typecheck/gripers.ml b/lib/typecheck/gripers.ml
index 572fad6..8f16c73 100644
--- a/lib/typecheck/gripers.ml
+++ b/lib/typecheck/gripers.ml
@@ -182,6 +182,20 @@ let env_interface_mismatch is_join t1 t2 var iface1 iface2 pos_list =
     in
     raise (constraint_gen_error ~subsystem msg pos_list )
 
+let env_tyargs_mismatch is_join t1 t2 var iface tyargs1 tyargs2 pos_list =
+    let subsystem =
+        if is_join then Errors.GenJoin else Errors.GenIntersect
+    in
+    let msg =
+        Format.asprintf
+            "Unable to combine types %a and %a for variable %a as they have type arguments (%a and %a) for interface %s."
+            Type.pp t1 Type.pp t2 Ir.Var.pp_name var
+            (Format.pp_print_list Type.pp) tyargs1
+            (Format.pp_print_list Type.pp) tyargs2
+            iface
+    in
+    raise (constraint_gen_error ~subsystem msg pos_list )
+
 let type_mismatch is_join t1 t2 var pos_list =
     let subsystem =
         if is_join then Errors.GenJoin else Errors.GenIntersect
diff --git a/lib/typecheck/pretypecheck.ml b/lib/typecheck/pretypecheck.ml
index 334928a..b5ae084 100644
--- a/lib/typecheck/pretypecheck.ml
+++ b/lib/typecheck/pretypecheck.ml
@@ -109,6 +109,128 @@ end
 
 module IEnv = Interface_env
 
+(* Check that typaram contains only typing variables *)
+let check_typarams pos typarams =
+    List.for_all
+      (fun (t : (Type.t[@name "ty"])) ->
+        match t with
+        TVar _ -> true
+        | _ -> Gripers.type_mismatch_with_expected pos
+                        "type variable" (Pretype.of_type t))
+      typarams
+
+(* Check that all type variables occuring in t are in typarams *)
+let check_tvar_in_params pos typarams (t : (Type.t[@name "ty"])) =
+    let rec aux (t : (Type.t[@name "ty"])) =
+        match t with
+        TVar s ->
+            if List.mem t typarams
+            then true
+            else Gripers.unbound_variable pos s
+            | Base _ -> true
+        | Fun { typarams=fun_typarams; args; result; _ } ->
+            (List.for_all aux fun_typarams)
+            && (List.for_all aux args)
+            && (aux result)
+        | Tuple ts ->
+            List.for_all aux ts
+        | Sum (t1, t2) ->
+            (aux t1) && (aux t2)
+        | Mailbox _ -> true
+    in aux t
+
+(* Check that all type variables occuring in interface are bound *)
+let check_iface_is_closed (iface_with_pos : Interface.t WithPos.t) : bool =
+    let iface = WithPos.node iface_with_pos in
+    let pos = WithPos.pos iface_with_pos in
+    let typarams = iface.typarams in
+    (check_typarams pos typarams)
+    && (List.for_all
+        (fun (_, ts) -> List.for_all (check_tvar_in_params pos typarams) ts)
+        iface.env)
+
+(* Check that all type variables occuring in declaration are bound *)
+let check_decl_is_closed (decl_with_pos : Ir.decl WithPos.t) =
+    let decl = WithPos.node decl_with_pos in
+    let pos = WithPos.pos decl_with_pos in
+    let typarams = decl.typarams in
+    let iface_aux pos typarams iface =
+        match iface with
+        None -> true
+        | Some (_, ts) ->
+            List.for_all (check_tvar_in_params pos typarams) ts
+    in
+    (* check that value is type-closed *)
+    let rec value_aux (v : Ir.value) : bool =
+        let vn = WithPos.node v in
+        let pos = WithPos.pos v in
+        match vn with
+        VAnnotate (v, t) ->
+            (check_tvar_in_params pos typarams t)
+            && (value_aux v)
+        | Atom _ | Constant _ | Primitive _ | Variable _ -> true
+        | Tuple vs -> List.for_all value_aux vs
+        | Inl v | Inr v -> value_aux v
+        | Lam { parameters; result_type; body; _ } ->
+            (List.for_all (fun (_, t) -> check_tvar_in_params pos typarams t) parameters)
+            && (check_tvar_in_params pos typarams result_type)
+            && (comp_aux body)
+    (* check that guard is type-closed *)
+    and guard_aux (g : Ir.guard) : bool =
+        let gn = WithPos.node g in
+        match gn with
+        Receive { cont; _ } -> comp_aux cont
+        | Empty (_, c) -> comp_aux c
+        | Fail -> true
+    (* check that comp is type-closed *)
+    and comp_aux (c : Ir.comp) : bool =
+        let cn = WithPos.node c in
+        let pos = WithPos.pos c in
+        match cn with
+        Annotate (c, t) ->
+            (check_tvar_in_params pos typarams t)
+            && (comp_aux c)
+        | Let { term; cont; _ } ->
+            (comp_aux term)
+            && (comp_aux cont)
+        | Seq (c1, c2) ->
+            (comp_aux c1)
+            && (comp_aux c2)
+        | Return v -> value_aux v
+        | App { tyargs; func; args; } ->
+            (value_aux func)
+            && (List.for_all value_aux args)
+            && (List.for_all (check_tvar_in_params pos typarams) tyargs)
+        | If { then_expr; else_expr; _ } ->
+            (comp_aux then_expr)
+            && (comp_aux else_expr)
+        | LetTuple { tuple; cont; _ } ->
+            (value_aux tuple) && (comp_aux cont)
+        | Case { term; branch1=((_, t1), c1); branch2=((_, t2), c2); _ } ->
+            (value_aux term)
+            && (check_tvar_in_params pos typarams t1)
+            && (check_tvar_in_params pos typarams t2)
+            && (comp_aux c1)
+            && (comp_aux c2)
+        | New (_, ts) ->
+            List.for_all (check_tvar_in_params pos typarams) ts
+        | Spawn c ->
+            comp_aux c
+        | Send { target; iface; _ } ->
+            (value_aux target) && (iface_aux pos typarams iface)
+        | Free (v, iface) ->
+            (value_aux v) && (iface_aux pos typarams iface)
+        | Guard { target; guards; iface; _} ->
+            (value_aux target)
+            && (iface_aux pos typarams iface)
+            && (List.for_all guard_aux guards)
+    in
+    (check_typarams pos typarams)
+    && (List.for_all (fun (_, t) -> check_tvar_in_params pos typarams t) decl.decl_parameters)
+    && (check_tvar_in_params pos typarams decl.decl_return_type)
+    && (comp_aux decl.decl_body)
+
+
 (* We take a bidirectional approach. Unlike in gen_constraints,
    as with most bidirectional systems, we try and synthesise as much
    as we can, since we carry around the type environment with us and
@@ -153,6 +275,7 @@ let rec synthesise_val ienv env value : (value * Pretype.t) =
             wrap (Lam { linear; parameters; body; result_type }),
             Pretype.PFun {
                 linear = linear;
+                typarams = [];
                 args = param_types;
                 result = result_type 
             }
@@ -251,15 +374,22 @@ and synthesise_comp ienv env comp =
             let e1 = check_comp ienv env e1 (Pretype.unit) in
             let e2, e2_ty = synth e2 in
             WithPos.make ~pos(Seq (e1, e2)), e2_ty
-        | App { func; args } ->
+        | App { func; tyargs; args } ->
             let open Pretype in
             (* Synthesise type for function; ensure it is a function type *)
             let (func, f_ty) = synthv func in
             let arg_anns, result_ann =
                 begin
                     match f_ty with
-                        | PFun { args; result; _ } ->
-                            List.map Pretype.of_type args, result
+                        | PFun { typarams; args; result; _ } ->
+                          begin
+                          try
+                            let args' = List.map (Type_utils.substitute_types typarams tyargs) args in
+                            let result' = Type_utils.substitute_types typarams tyargs result in
+                            List.map Pretype.of_type args', result'
+                          with Invalid_argument _ ->
+                            Gripers.arity_error pos (List.length typarams) (List.length tyargs)
+                          end
                         | t ->
                             Gripers.type_mismatch_with_expected pos "a function type" t
                 end
@@ -278,7 +408,7 @@ and synthesise_comp ienv env comp =
                     check_val ienv env arg arg_ty)
             in
             (* Synthesise result type *)
-            WithPos.make ~pos(App { func; args }), Pretype.of_type result_ann
+            WithPos.make ~pos(App { func; tyargs; args }), Pretype.of_type result_ann
         | Send { target; message = (tag, vals); _ } ->
             let open Pretype in
             (* Typecheck target *)
@@ -286,15 +416,20 @@ and synthesise_comp ienv env comp =
             (* Ensure target has interface type *)
             begin
                 match target_ty with
-                    | PInterface iname ->
+                    | PInterface (iname, tyargs) ->
                         (* Check that:
                             - Message tag is contained within interface
                             - Message payload pretype matches that of the interface *)
                         let interface_withPos = IEnv.lookup iname ienv [(WithPos.pos comp)] in
+                        let typarams = Interface.typarams (WithPos.node interface_withPos) in
                         let payload_target_tys =
+                          try
                             WithPos.node interface_withPos
-                            |> Interface.lookup ~pos_list:(WithPos.extract_pos_pair interface_withPos comp)  tag
+                            |> Interface.lookup ~pos_list:(WithPos.extract_pos_pair interface_withPos comp) tag
+                            |> List.map (Type_utils.substitute_types typarams tyargs)
                             |> List.map Pretype.of_type
+                          with Invalid_argument _ ->
+                            Gripers.arity_error pos (List.length typarams) (List.length tyargs)
                         in
                         let () =
                             let iface_len = List.length payload_target_tys in
@@ -312,7 +447,7 @@ and synthesise_comp ienv env comp =
                         Send {
                             target;
                             message = (tag, vals);
-                            iname = Some iname
+                            iface = Some (iname, tyargs)
                          }), Pretype.unit
                     | ty -> Gripers.type_mismatch_with_expected pos "an interface type" ty
             end
@@ -326,9 +461,9 @@ and synthesise_comp ienv env comp =
             WithPos.make ~pos(Free (v, Some iface)), Pretype.unit
         | Guard { target; pattern; guards; _ } ->
             let (target, target_ty) = synthv target in
-            let iname =
+            let iface =
                 match target_ty with
-                    | PInterface iname -> iname
+                    | PInterface iface -> iface
                     | t -> Gripers.type_mismatch_with_expected pos "an interface type" t
             in
             (* We can synthesise the type of a guard expression as long as it is
@@ -340,13 +475,13 @@ and synthesise_comp ienv env comp =
                     | [] ->
                         Gripers.cannot_synth_empty_guards pos ()
                     | g :: gs ->
-                        let g, g_ty = synth_guard ienv env iname g in
+                        let g, g_ty = synth_guard ienv env iface g in
                         let gs =
-                            List.map (fun g -> check_guard pos ienv env iname g g_ty) gs
+                            List.map (fun g -> check_guard pos ienv env iface g g_ty) gs
                         in
                         g :: gs, g_ty
             in
-            WithPos.make ~pos(Guard { target; pattern; guards; iname = Some iname }), g_ty
+            WithPos.make ~pos(Guard { target; pattern; guards; iface = Some iface }), g_ty
 and check_comp ienv env comp ty  =
     let pos = WithPos.pos comp in
     match WithPos.node comp with
@@ -355,17 +490,17 @@ and check_comp ienv env comp ty  =
             WithPos.make ~pos (Return v)
         | Guard { target; pattern; guards; _ } when guards = [(WithPos.make ~pos Fail)] ->
             let target, target_ty = synthesise_val ienv env target in
-            let iname =
+            let iface =
                 match target_ty with
-                    | PInterface iname -> iname
+                    | PInterface iface -> iface
                     | t -> Gripers.type_mismatch_with_expected pos "an interface type" t
             in
-            WithPos.make ~pos (Guard { target; pattern; guards = [(WithPos.make ~pos Fail)]; iname = Some iname })
+            WithPos.make ~pos (Guard { target; pattern; guards = [(WithPos.make ~pos Fail)]; iface = Some iface })
         | _ ->
             let comp, inferred_ty = synthesise_comp ienv env comp in
             check_tys [pos] ty inferred_ty;
             comp
-and synth_guard ienv env iname g =
+and synth_guard ienv env ((iname, typarams) : (string * (Type.t[@name "ty"]) list)) g =
     let interface_withPos = IEnv.lookup iname ienv [(WithPos.pos g)] in
     let iface = WithPos.node interface_withPos in
     let pos = WithPos.pos g in
@@ -390,24 +525,28 @@ and synth_guard ienv env iname g =
                 |> PretypeEnv.bind_many payload_entries
                 |> PretypeEnv.bind
                     (Var.of_binder mailbox_binder)
-                    (Pretype.PInterface iname)
+                    (Pretype.PInterface (iname, typarams))
             in
             let cont, cont_ty = synthesise_comp ienv env cont in
             WithPos.make ~pos (Receive { tag; payload_binders; mailbox_binder; cont }), cont_ty
         | Empty (x, e) ->
-            let env = PretypeEnv.bind (Var.of_binder x) (Pretype.PInterface iname) env in
+            let env = PretypeEnv.bind (Var.of_binder x) (Pretype.PInterface (iname, typarams)) env in
             let e, e_ty = synthesise_comp ienv env e in
             WithPos.make ~pos (Empty (x, e)), e_ty
         | Fail ->
             Gripers.cannot_synth_fail pos ()
-and check_guard pos ienv env iname g ty =
-    let g, inferred_ty = synth_guard ienv env iname g in
+and check_guard pos ienv env (iface : string * (Type.t[@name "ty"]) list) g ty =
+    let g, inferred_ty = synth_guard ienv env iface g in
     check_tys [pos] ty inferred_ty;
     g
 
 (* Top-level typechecker *)
 let check { prog_interfaces; prog_decls; prog_body } =
 
+    (* Check that interface and definitions are type-closed.
+       Unbound_variable is raised otherwiser. *)
+    let _ = List.for_all check_iface_is_closed prog_interfaces in
+    let _ = List.for_all check_decl_is_closed prog_decls in
     (* Construct interface environment from interface list *)
     let ienv = IEnv.from_list prog_interfaces in
     let param_pretypes =
@@ -426,6 +565,7 @@ let check { prog_interfaces; prog_decls; prog_body } =
             (Var.of_binder d.decl_name,
                 Pretype.PFun {
                     linear = false;
+                    typarams = d.typarams;
                     args = param_tys;
                     result = d.decl_return_type
                 })) (WithPos.extract_list_node prog_decls)
diff --git a/lib/typecheck/ty_env.ml b/lib/typecheck/ty_env.ml
index 0233ed0..5fd86b8 100644
--- a/lib/typecheck/ty_env.ml
+++ b/lib/typecheck/ty_env.ml
@@ -60,26 +60,31 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
             match (t1, t2) with
                 | Base b1, Base b2 when b1 = b2 ->
                     (Base b1, Constraint_set.empty)
-                | Fun { linear = linear1; args = dom1; result = cod1 },
-                  Fun { linear = linear2; args = dom2; result = cod2 }
+                | TVar s1, TVar s2 when s1 = s2 ->
+                    (TVar s1, Constraint_set.empty)
+                | Fun { linear = linear1; args = dom1; result = cod1; typarams=typarams1 },
+                  Fun { linear = linear2; args = dom2; result = cod2; _ }
                     when (not linear1) && (not linear2) && dom1 = dom2 && cod1 = cod2 ->
                         let subty_constrs =
                             Constraint_set.union
                                 (subtype ienv t1 t2 pos)
                                 (subtype ienv t2 t1 pos)
                         in
-                        (Fun { linear = false; args = dom1; result = cod1 }, subty_constrs)
+                        (Fun { linear = false; typarams=typarams1; args = dom1; result = cod1 }, subty_constrs)
                 | Mailbox { pattern = None; _ }, _ | _, Mailbox { pattern = None; _ } ->
                     assert false (* Set by pre-typing *)
-                | Mailbox { capability = cap1; interface = iface1; pattern =
+                | Mailbox { capability = cap1; interface = (iname1, tyargs1); pattern =
                     Some pat1; quasilinearity = ql1 },
-                  Mailbox { capability = cap2; interface = iface2; pattern =
+                  Mailbox { capability = cap2; interface = (iname2, tyargs2); pattern =
                       Some pat2; quasilinearity = ql2 } ->
                       (* We can only join variables with the same interface
-                         name. If these match, we can join the types. *)
-                      if iface1 <> iface2 then
+                         name and type arguments. If these match, we can join the types. *)
+                      if iname1 <> iname2 then
                           Gripers.env_interface_mismatch true
-                            t1 t2 var iface1 iface2 [pos]
+                            t1 t2 var iname1 iname2 [pos]
+                      else if tyargs1 <> tyargs2 then
+                          Gripers.env_tyargs_mismatch true
+                            t1 t2 var iname1 tyargs1 tyargs2 [pos]
                       else
                           (* Check sequencing of QL *)
                           let ql =
@@ -93,7 +98,7 @@ let join : Interface_env.t -> t -> t -> Position.t -> t * Constraint_set.t =
                                 (cap1, pat1) (cap2, pat2) in
                           Mailbox {
                               capability = cap;
-                              interface = iface1;
+                              interface = (iname1, tyargs1);
                               pattern = Some pat;
                               quasilinearity = ql
                           }, constrs
@@ -201,27 +206,33 @@ let intersect : t -> t -> Position.t -> t * Constraint_set.t =
             match t1, t2 with
                 | Base b1, Base b2 when b1 = b2 ->
                     (Base b1, Constraint_set.empty)
-                | Fun { linear = linear1; args = dom1; result = cod1 },
-                  Fun { linear = linear2; args = dom2; result = cod2 }
+                | TVar s1, TVar s2 when s1 = s2 ->
+                    (TVar s1, Constraint_set.empty)
+                | Fun { linear = linear1; typarams=typarams1; args = dom1; result = cod1 },
+                  Fun { linear = linear2; args = dom2; result = cod2; _ }
                     when (linear1 = linear2) && dom1 = dom2 && cod1 = cod2 ->
-                        (Fun { linear = linear1; args = dom1; result = cod1 }, Constraint_set.empty)
+                    (Fun { linear = linear1; typarams=typarams1; args = dom1; result = cod1 }, Constraint_set.empty)
                 | Mailbox { pattern = None; _ }, _ | _, Mailbox { pattern = None; _ } ->
                     assert false (* Set by pre-typing *)
-                | Mailbox { capability = cap1; interface = iface1; pattern =
+                | Mailbox { capability = cap1; interface = (iname1, tyargs1); pattern =
                     Some pat1; quasilinearity = ql1 },
-                  Mailbox { capability = cap2; interface = iface2; pattern =
+                  Mailbox { capability = cap2; interface = (iname2, tyargs2); pattern =
                       Some pat2; quasilinearity = ql2 } ->
                       (* As before -- interface names must be the same*)
-                      if iface1 <> iface2 then
+                      if iname1 <> iname2 then
                           Gripers.env_interface_mismatch
-                            false t1 t2 var iface1 iface2 [pos]
+                            false t1 t2 var iname1 iname2 [pos]
+                      (* as well as type arguments *)
+                      else if tyargs1 <> tyargs2 then
+                          Gripers.env_tyargs_mismatch true
+                            t1 t2 var iname1 tyargs1 tyargs2 [pos]
                       else
                           let ((cap, pat), constrs) =
                               intersect_mailbox_types var
                                 (cap1, pat1) (cap2, pat2) in
                           Mailbox {
                               capability = cap;
-                              interface = iface1;
+                              interface = (iname1, tyargs1);
                               pattern = Some pat;
                               (* Must take strongest QL across all branches. *)
                               quasilinearity = Quasilinearity.max ql1 ql2
diff --git a/lib/typecheck/type_utils.ml b/lib/typecheck/type_utils.ml
index a64bcba..60d4a83 100644
--- a/lib/typecheck/type_utils.ml
+++ b/lib/typecheck/type_utils.ml
@@ -14,6 +14,7 @@ let make_unrestricted t pos =
         (* Trivially unrestricted *)
         | Base _
         | Tuple []
+        | TVar _
         | Fun { linear = false; _ } -> Constraint_set.empty
         (* Cannot be unrestricted *)
         | Fun { linear = true; _ }
@@ -26,6 +27,29 @@ let make_unrestricted t pos =
         | _ -> assert false
 
 (* Auxiliary definitions*)
+let substitute_types xs ys =
+  let rec subst_aux varmap t =
+    match t with
+    | Type.TVar _ ->
+      begin match List.assoc_opt t varmap with
+        | None -> t
+        | Some t' -> t'
+      end
+    | Base _ -> t
+    | Fun { linear; typarams; args; result } ->
+      Fun { linear;
+            typarams;
+            args=(List.map (subst_aux varmap) args);
+            result=(subst_aux varmap result)
+          }
+    | Tuple ts -> Tuple (List.map (subst_aux varmap) ts)
+    | Sum (t1, t2) ->
+        Sum (subst_aux varmap t1, subst_aux varmap t2)
+    | Mailbox { capability; interface=(iname, tyargs); pattern; quasilinearity } ->
+      let tyargs' = List.map (subst_aux varmap) tyargs in
+      Mailbox { capability; interface=(iname, tyargs'); pattern; quasilinearity }
+
+  in subst_aux (List.combine xs ys)
 
 (* Checks whether t1 is a subtype of t2, and produces the necessary constraints.
    We need to take a coinductive view of subtyping to avoid infinite loops, so
@@ -36,9 +60,10 @@ let rec subtype_type :
         Interface_env.t -> Type.t -> Type.t -> Position.t -> Constraint_set.t =
     fun visited ienv t1 t2 pos ->
         match t1, t2 with
-            | Base b1, Base b2 when b1 = b2->
-                        Constraint_set.empty
-
+            | Base b1, Base b2 when b1 = b2 ->
+              Constraint_set.empty
+            | TVar s1, TVar s2 when s1 = s2 ->
+              Constraint_set.empty
             (* Subtyping covariant for tuples and sums *)
             | Tuple tyas, Tuple tybs ->
                 Constraint_set.union_many
@@ -53,9 +78,9 @@ let rec subtype_type :
                     (* Should have been sorted by annotation pass *)
                     assert false
             | Fun { linear = lin1; args = args1;
-                    result = body1 },
+                    result = body1; _ },
               Fun { linear = lin2; args = args2;
-                    result = body2 } ->
+                    result = body2; _ } ->
                     let () =
                         if lin1 <> lin2 then
                             Gripers.subtype_linearity_mismatch t1 t2 [pos]
@@ -68,13 +93,13 @@ let rec subtype_type :
                     Constraint_set.union args_constrs body_constrs
             | Mailbox {
                 capability = capability1;
-                interface = iname1;
+                interface = (iname1, _);
                 pattern = Some pat1;
                 quasilinearity = ql1
               },
               Mailbox {
                 capability = capability2;
-                interface = iname2;
+                interface = (iname2, _);
                 pattern = Some pat2;
                 quasilinearity = ql2
               } ->
diff --git a/test/examples/parametrized_interfaces/0_basic_recv.pat b/test/examples/parametrized_interfaces/0_basic_recv.pat
new file mode 100644
index 0000000..af32e24
--- /dev/null
+++ b/test/examples/parametrized_interfaces/0_basic_recv.pat
@@ -0,0 +1,17 @@
+interface Recv {
+	Put(Bool)
+}
+
+def boolRecv(self : Recv?) : Unit {
+	guard self : Put {
+		receive Put(b) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def boolClient() : Unit {
+	let mb = new[Recv] in
+	spawn { boolRecv(mb) };
+	mb ! Put(true)
+}
diff --git a/test/examples/parametrized_interfaces/1_param_recv.pat b/test/examples/parametrized_interfaces/1_param_recv.pat
new file mode 100644
index 0000000..c3f2e4b
--- /dev/null
+++ b/test/examples/parametrized_interfaces/1_param_recv.pat
@@ -0,0 +1,31 @@
+interface Recv[A] {
+	Put(A)
+}
+
+def boolRecv(self : Recv[Bool]?) : Unit {
+	guard self : Put {
+		receive Put(b) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def boolClient() : Unit {
+	let mb = new[Recv[Bool]] in
+	spawn { boolRecv(mb) };
+	mb ! Put(true)
+}
+
+def intRecv(self : Recv[Int]?) : Unit {
+	guard self : Put {
+		receive Put(b) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def intClient() : Unit {
+	let mb = new[Recv[Int]] in
+	spawn { intRecv(mb) };
+	mb ! Put(0)
+}
diff --git a/test/examples/parametrized_interfaces/2_param_send.pat b/test/examples/parametrized_interfaces/2_param_send.pat
new file mode 100644
index 0000000..664962a
--- /dev/null
+++ b/test/examples/parametrized_interfaces/2_param_send.pat
@@ -0,0 +1,47 @@
+interface User[A] {
+	Reply(A)
+}
+
+interface Mirror[A] {
+	Put(A, User[A]!)
+}
+
+def boolMirror(self : Mirror[Bool]?) : Unit {
+	guard self : Put {
+		receive Put(msg, sender) from self ->
+			free(self);
+			sender ! Reply(msg)
+	}
+}
+
+def boolClient() : Unit {
+	let mirrorBox = new[Mirror[Bool]] in
+	let self = new[User[Bool]] in
+	spawn { boolMirror(mirrorBox) };
+	mirrorBox ! Put(true, self);
+	guard self : Reply {
+		receive Reply(x) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def intMirror(self : Mirror[Int]?) : Unit {
+	guard self : Put {
+		receive Put(msg, sender) from self ->
+			free(self);
+			sender ! Reply(msg)
+	}
+}
+
+def intClient() : Unit {
+	let mirrorBox = new[Mirror[Int]] in
+	let self = new[User[Int]] in
+	spawn { intMirror(mirrorBox) };
+	mirrorBox ! Put(0, self);
+	guard self : Reply {
+		receive Reply(x) from self ->
+			free(self);
+			print("received")
+	}
+}
diff --git a/test/examples/parametrized_interfaces/3_param_mirror_def.pat b/test/examples/parametrized_interfaces/3_param_mirror_def.pat
new file mode 100644
index 0000000..ce15cb6
--- /dev/null
+++ b/test/examples/parametrized_interfaces/3_param_mirror_def.pat
@@ -0,0 +1,36 @@
+interface User[A] {
+	Reply(A)
+}
+
+interface Mirror[A] {
+	Put(A, User[A]!)
+}
+
+def mirror[A](self : Mirror[A]?) : Unit {
+	guard self : Put {
+		receive Put(msg, sender) from self ->
+			free(self);
+			sender ! Reply(msg)
+	}
+}
+
+def client() : Unit {
+	let boolMirrorBox = new[Mirror[Bool]] in
+	let self = new[User[Bool]] in
+	spawn { mirror[Bool](boolMirrorBox) };
+	boolMirrorBox ! Put(true, self);
+	guard self : Reply {
+		receive Reply(x) from self ->
+			free(self);
+			print("received")
+	};
+	let intMirrorBox = new[Mirror[Int]] in
+	let self = new[User[Int]] in
+	spawn { mirror[Int](intMirrorBox) };
+	intMirrorBox ! Put(0, self);
+	guard self : Reply {
+		receive Reply(x) from self ->
+			free(self);
+			print("received")
+	}
+}
diff --git a/test/examples/parametrized_interfaces/4_param_client_def.pat b/test/examples/parametrized_interfaces/4_param_client_def.pat
new file mode 100644
index 0000000..e399d0e
--- /dev/null
+++ b/test/examples/parametrized_interfaces/4_param_client_def.pat
@@ -0,0 +1,31 @@
+interface User[A] {
+	Reply(A)
+}
+
+interface Mirror[A] {
+	Put(A, User[A]!)
+}
+
+def mirror[A](self : Mirror[A]?) : Unit {
+	guard self : Put {
+		receive Put(msg, sender) from self ->
+			free(self);
+			sender ! Reply(msg)
+	}
+}
+
+def client[A](value : A) : Unit {
+	let mirrorBox = new[Mirror[A]] in
+	let self = new[User[A]] in
+	spawn { mirror[A](mirrorBox) };
+	mirrorBox ! Put(value, self);
+	guard self : Reply {
+		receive Reply(v) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def intClient() : Unit {
+	client[Int](0)
+}
diff --git a/test/examples/parametrized_interfaces/5_param_future.pat b/test/examples/parametrized_interfaces/5_param_future.pat
new file mode 100644
index 0000000..3d277c1
--- /dev/null
+++ b/test/examples/parametrized_interfaces/5_param_future.pat
@@ -0,0 +1,49 @@
+interface User[A] {
+	Reply(A)
+}
+
+interface Future[A] {
+	Put(A),
+	Get(User[A]!)
+}
+
+def emptyFuture[A](self : Future[A]?) : Unit {
+	guard self : Put . Get* {
+		receive Put(value) from self ->
+			fullFuture[A](value, self)
+	}
+}
+
+def fullFuture[A](value : A, self : Future[A]?) : Unit {
+	guard self : Get* {
+		free -> ()
+		receive Get(sender) from self ->
+			sender ! Reply(value);
+			fullFuture[A](value, self)
+	}
+}
+
+def client[A](value : A) : Unit {
+	let futureBox = new[Future[A]] in
+	let self = new[User[A]] in
+	spawn { emptyFuture[A](futureBox) };
+	futureBox ! Put(value);
+	futureBox ! Get(self);
+	futureBox ! Get(self);
+	futureBox ! Get(self);
+	guard self : Reply . Reply . Reply {
+		receive Reply(v1) from self ->
+			print("1st receive");
+			guard self : Reply . Reply {
+				receive Reply(v2) from self ->
+					print("2nd receive");
+					guard self : Reply {
+						receive Reply(v3) from self ->
+							free(self);
+							print("3rd receive")
+					}
+			}
+	}
+}
+
+let test = spawn { client[Int](10) }; spawn { client[Int](5) }; spawn { client[Bool](true) } in ()
diff --git a/test/examples/parametrized_interfaces/wrong/0_unboundable_type.pat b/test/examples/parametrized_interfaces/wrong/0_unboundable_type.pat
new file mode 100644
index 0000000..3d82c59
--- /dev/null
+++ b/test/examples/parametrized_interfaces/wrong/0_unboundable_type.pat
@@ -0,0 +1,17 @@
+interface Recv[A, Int] {
+	Put(Int),
+	PutOpen(A)
+}
+
+def intRecv(self : Recv[Int, Int]?) : Unit {
+	guard self : Put {
+		receive Put(x) from self->
+			free(self)
+	}
+}
+
+def client() : Unit {
+	let mb = new[Recv[Int, Int]] in
+	spawn { intRecv(mb) };
+	mb ! Put(2)
+}
diff --git a/test/examples/parametrized_interfaces/wrong/0_unclosed_definition.pat b/test/examples/parametrized_interfaces/wrong/0_unclosed_definition.pat
new file mode 100644
index 0000000..f1f7912
--- /dev/null
+++ b/test/examples/parametrized_interfaces/wrong/0_unclosed_definition.pat
@@ -0,0 +1,7 @@
+interface Recv {
+	Put(Int)
+}
+
+def f(x : A) : Unit {
+	()
+}
diff --git a/test/examples/parametrized_interfaces/wrong/0_unclosed_interface.pat b/test/examples/parametrized_interfaces/wrong/0_unclosed_interface.pat
new file mode 100644
index 0000000..b995a0a
--- /dev/null
+++ b/test/examples/parametrized_interfaces/wrong/0_unclosed_interface.pat
@@ -0,0 +1,17 @@
+interface Recv {
+	Put(Int),
+	PutOpen(A)
+}
+
+def intRecv(self : Recv?) : Unit {
+	guard self : Put {
+		receive Put(x) from self->
+			free(self)
+	}
+}
+
+def client() : Unit {
+	let mb = new[Recv] in
+	spawn { intRecv(mb) };
+	mb ! Put(2)
+}
diff --git a/test/examples/parametrized_interfaces/wrong/1_send_mismatch.pat b/test/examples/parametrized_interfaces/wrong/1_send_mismatch.pat
new file mode 100644
index 0000000..ef7e326
--- /dev/null
+++ b/test/examples/parametrized_interfaces/wrong/1_send_mismatch.pat
@@ -0,0 +1,17 @@
+interface Recv[A] {
+	Put(A)
+}
+
+def boolRecv(self : Recv[Bool]?) : Unit {
+	guard self : Put {
+		receive Put(b) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def boolClient() : Unit {
+	let mb = new[Recv[Bool]] in
+	spawn { boolRecv(mb) };
+	mb ! Put(1)
+}
diff --git a/test/examples/parametrized_interfaces/wrong/1_spawn_mismatch.pat b/test/examples/parametrized_interfaces/wrong/1_spawn_mismatch.pat
new file mode 100644
index 0000000..497dc84
--- /dev/null
+++ b/test/examples/parametrized_interfaces/wrong/1_spawn_mismatch.pat
@@ -0,0 +1,17 @@
+interface Recv[A] {
+	Put(A)
+}
+
+def boolRecv(self : Recv[Bool]?) : Unit {
+	guard self : Put {
+		receive Put(b) from self ->
+			free(self);
+			print("received")
+	}
+}
+
+def boolClient() : Unit {
+	let mb = new[Recv[Int]] in
+	spawn { boolRecv(mb) };
+	mb ! Put(true)
+}
diff --git a/test/tests.json b/test/tests.json
index ce43bae..5cb8360 100644
--- a/test/tests.json
+++ b/test/tests.json
@@ -184,6 +184,28 @@
                 {"name": "Additional non-supported non-fail guard with nontrivial continuation", "filename": "errors/pat_constr3.pat", "exit_code": 1},
                 {"name": "Additional non-supported free guard", "filename": "errors/pat_constr4.pat", "exit_code": 1}
             ]
+        },
+        { "group": "Parametrized interfaces (Good)",
+          "tests":
+            [
+                {"name": "Basic send", "filename": "examples/parametrized_interfaces/0_basic_recv.pat", "exit_code": 0},
+                {"name": "Receive interface", "filename": "examples/parametrized_interfaces/1_param_recv.pat", "exit_code": 0},
+                {"name": "Mirror with mutually recursive interfaces", "filename": "examples/parametrized_interfaces/2_param_send.pat", "exit_code": 0},
+                {"name": "Parametrized mirror definition", "filename": "examples/parametrized_interfaces/3_param_mirror_def.pat", "exit_code": 0},
+                {"name": "Parametrized mirror definition and client", "filename": "examples/parametrized_interfaces/4_param_client_def.pat", "exit_code": 0},
+                {"name": "Parametrized mirror definition and client", "filename": "examples/parametrized_interfaces/4_param_client_def.pat", "exit_code": 0},
+                {"name": "Fully parametrized future", "filename": "examples/parametrized_interfaces/5_param_future.pat", "exit_code": 0}
+            ]
+        },
+        { "group": "Parametrized interfaces (Wrong)",
+          "tests":
+            [
+                {"name": "Type is not boundable", "filename": "examples/parametrized_interfaces/wrong/0_unboundable_type.pat", "exit_code": 1},
+                {"name": "Interface is not type closed", "filename": "examples/parametrized_interfaces/wrong/0_unclosed_interface.pat", "exit_code": 1},
+                {"name": "Definition is not type closed", "filename": "examples/parametrized_interfaces/wrong/0_unclosed_definition.pat", "exit_code": 1},
+                {"name": "Send payload mismatch", "filename": "examples/parametrized_interfaces/wrong/1_send_mismatch.pat", "exit_code": 1},
+                {"name": "Spawn wrong arity", "filename": "examples/parametrized_interfaces/wrong/1_spawn_mismatch.pat", "exit_code": 1}
+            ]
         }
     ]
 }