diff --git a/base-types.sml b/base-types.sml
index de6d25ac..f01df4a6 100644
--- a/base-types.sml
+++ b/base-types.sml
@@ -1,16 +1,18 @@
 structure BaseTypes = struct
 datatype base_type =
          Int
-         | String
          | Bool
+         | Byte
+         (* | String *)
            
 fun eq_base_type (t : base_type, t') = t = t'
         
 fun str_bt bt =
   case bt of
       Int => "int"
-    | String => "string"
     | Bool => "bool"
+    | Byte => "byte"
+    (* | String => "string" *)
 
 end
 
diff --git a/elaborate.sml b/elaborate.sml
index 96f96f91..9618da8c 100644
--- a/elaborate.sml
+++ b/elaborate.sml
@@ -165,10 +165,12 @@ local
                   Unit r
                 else if x = "int" then
                   BaseType (Int, r)
-                else if x = "string" then
-                  BaseType (String, r)
                 else if x = "bool" then
                   BaseType (Bool, r)
+                else if x = "byte" then
+                  BaseType (Byte, r)
+                (* else if x = "string" then *)
+                (*   BaseType (String, r) *)
                 else if x = "_" then
                   UVar ((), r)
                 else
@@ -293,7 +295,7 @@ local
                 (* else if x = "never" andalso eia = false then *)
                 (*   ENever (elab_mt (S.VarT (NONE, ("_", r))), r) *)
                 else if x = "__&empty_array" andalso eia = false then
-                  ET (ETEmptyArray, elab_mt (S.VarT (NONE, ("_", r))), r)
+                  EEmptyArray (elab_mt (S.VarT (NONE, ("_", r))), r)
                 else if x = "__&builtin" then raise Error (r, "should be '__&builtin \"name\"'")
                 else
                   def ()
@@ -330,24 +332,26 @@ local
 	| S.Let (return, decs, e, r) =>
           ELet (elab_return return, Unbound.Bind (Teles $ map elab_decl decs, elab e), r)
 	| S.Const (c, r) =>
-          let
-            fun unescape s =
-              let
-                val ls = String.explode s
-                fun loop (ls, acc) =
-                  case ls of
-                      #"\\" :: #"n" :: ls => loop (ls, #"\n" :: acc)
-                    | c :: ls => loop (ls, c :: acc)
-                    | [] => acc
-              in
-                String.implode $ rev $ loop (ls, [])
-              end
-          in
-            case c of
+            (case c of
                 S.ECInt n => EConstInt (n, r)
 	      | S.ECNat n => EConstNat (n, r)
-	      | S.ECString s => EConstString (unescape s, r)
-          end
+	      | S.ECString s =>
+                let
+                  fun unescape s =
+                    let
+                      val ls = String.explode s
+                      fun loop (ls, acc) =
+                        case ls of
+                            #"\\" :: #"n" :: ls => loop (ls, #"\n" :: acc)
+                          | c :: ls => loop (ls, c :: acc)
+                          | [] => acc
+                    in
+                      String.implode $ rev $ loop (ls, [])
+                    end
+                  val s = unescape s
+                in
+                  ENewArrayValues (BaseType (Byte, r), map (fn c => EByte (c, r)) $ String.explode s, r)
+                end)
 	| S.BinOp (EBApp, e1, e2, r) =>
 	  let 
 	    fun default () = EApp (elab e1, elab e2)
@@ -359,10 +363,11 @@ local
 		     if x = "__&fst" then EFst (elab e2, r)
 		     else if x = "__&snd" then ESnd (elab e2, r)
 		     else if x = "__&not" then EUnOp (EUPrim EUPBoolNeg, elab e2, r)
-		     else if x = "__&int2str" then EUnOp (EUInt2Str, elab e2, r)
+		     (* else if x = "__&int2str" then EUnOp (EUInt2Str, elab e2, r) *)
 		     else if x = "__&nat2int" then EUnOp (EUNat2Int, elab e2, r)
 		     else if x = "__&array_length" then EUnOp (EUArrayLen, elab e2, r)
-		     else if x = "__&print" then EUnOp (EUPrint, elab e2, r)
+		     (* else if x = "__&print" then EUnOp (EUPrint, elab e2, r) *)
+		     else if x = "__&printc" then EUnOp (EUPrintc, elab e2, r)
                      else if x = "__&builtin" then
                        (case e2 of
                             S.Const (S.ECString s, _) =>
diff --git a/examples/pervasive.timl b/examples/pervasive.timl
new file mode 100644
index 00000000..b9a664ef
--- /dev/null
+++ b/examples/pervasive.timl
@@ -0,0 +1,5 @@
+structure Pervasive = struct
+
+datatype some_nat = SomeNat {n : Nat} of nat {n}
+
+end
diff --git a/examples/stdlib.pkg b/examples/stdlib.pkg
index a496898a..47b89ca9 100644
--- a/examples/stdlib.pkg
+++ b/examples/stdlib.pkg
@@ -1,4 +1,5 @@
 (* standard library *)
+pervasive.timl
 basic.timl
 nat.timl
 list.timl
diff --git a/examples/string.timl b/examples/string.timl
index 719c980f..4ad7866f 100644
--- a/examples/string.timl
+++ b/examples/string.timl
@@ -5,7 +5,7 @@ structure String = struct
                 
 open Array
        
-datatype string = String {len : Nat} of array char {len}
+datatype string = String {len : Nat} of array byte {len}
 
 new_string "abc" == String (new_array {'a', 'b', 'c'})
     
@@ -45,15 +45,15 @@ fun print s =
     ()
 end
 
-fun nat2chars {d : Nat} {i : Nat | 10 ** d <= i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list char {d+1} using d =
-  ifdec i #< #10 then [nat2char i]
-  else int2char (nat2int i mod 10) :: @nat2chars {d-1} {_} (i #/ 10)
+fun nat2bytes {d : Nat} {i : Nat | 10 ** d <= i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list byte {d+1} using d =
+  ifdec i #< #10 then [nat2byte i]
+  else int2byte (nat2int i mod 10) :: @nat2bytes {d-1} {_} (i #/ 10)
 
 fun int2str i return using 20 =
   let
     val Nat n = int2nat i
   in
-    String (fromList $ rev $ list2ilist chars)
+    String (fromList $ rev $ nat2bytes n)
   end
 
 end
diff --git a/expr-fn.sml b/expr-fn.sml
index 2de8aa09..eca286e5 100644
--- a/expr-fn.sml
+++ b/expr-fn.sml
@@ -39,6 +39,7 @@ datatype expr =
          | EEI of expr_EI * expr * idx
          | EET of expr_ET * expr * mtype
          | ET of expr_T * mtype * region
+         | ENewArrayValues of mtype * expr list * region
 	 | EAbs of (ptrn, expr) bind
 	 | EAbsI of (sort, expr) ibind_anno * region
 	 | EAppConstr of (cvar * bool) * mtype list * idx list * expr * (int * mtype) option
diff --git a/expr-util.sml b/expr-util.sml
index 8e0401dd..2c2cee12 100644
--- a/expr-util.sml
+++ b/expr-util.sml
@@ -10,14 +10,15 @@ infixr 0 $
 
 val EUFst = EUProj ProjFst
 val EUSnd = EUProj ProjSnd
-val EUInt2Str = EUPrim EUPInt2Str
+(* val EUInt2Str = EUPrim EUPInt2Str *)
 val EBAdd = EBPrim EBPIntAdd
 val EBNatAdd = EBNat EBNAdd
                    
 fun ETT r = EConst (ECTT, r)
 fun EConstInt (n, r) = EConst (ECInt n, r)
 fun EConstNat (n, r) = EConst (ECNat n, r)
-fun EConstString (n, r) = EConst (ECString n, r)
+(* fun EConstString (n, r) = EConst (ECString n, r) *)
+fun EByte (c, r) = EConst (ECByte c, r)
 fun EFst (e, r) = EUnOp (EUFst, e, r)
 fun ESnd (e, r) = EUnOp (EUSnd, e, r)
 fun EApp (e1, e2) = EBinOp (EBApp, e1, e2)
@@ -33,6 +34,7 @@ fun EBuiltin (name, t, r) = ET (ETBuiltin name, t, r)
 fun ENew (e1, e2) = EBinOp (EBNew, e1, e2)
 fun ERead (e1, e2) = EBinOp (EBRead, e1, e2)
 fun EWrite (e1, e2, e3) = ETriOp (ETWrite, e1, e2, e3)
+fun EEmptyArray (t, r) = ENewArrayValues (t, [], r)
   
 fun collect_Pair e =
   case e of
diff --git a/expr.sig b/expr.sig
index 2f7f7c24..1531988b 100644
--- a/expr.sig
+++ b/expr.sig
@@ -30,6 +30,7 @@ signature EXPR = sig
            | EEI of Operators.expr_EI * expr * idx
            | EET of Operators.expr_ET * expr * mtype
            | ET of Operators.expr_T * mtype * Region.region
+           | ENewArrayValues of mtype * expr list * Region.region
 	   | EAbs of (ptrn, expr) Unbound.bind
 	   | EAbsI of (sort, expr) Binders.ibind_anno * Region.region
 	   | EAppConstr of (cvar * bool) * mtype list * idx list * expr * (int * mtype) option
diff --git a/get-region.sml b/get-region.sml
index f576d292..87d2312f 100644
--- a/get-region.sml
+++ b/get-region.sml
@@ -132,6 +132,7 @@ fun get_region_e e =
     | EEI (_, e, i) => combine_region (get_region_e e) (get_region_i i)
     | EET (_, e, t) => combine_region (get_region_e e) (get_region_mt t)
     | ET (_, _, r) => r
+    | ENewArrayValues (_, _, r) => r
     | EAbs bind => get_region_bind get_region_pn get_region_e bind
     | EAbsI (_, r) => r
     | EAppConstr ((x, _), _, _, e, _) => combine_region (get_region_cvar x) (get_region_e e)
diff --git a/micro-timl/cc.sml b/micro-timl/cc.sml
index f370370d..e076a18c 100644
--- a/micro-timl/cc.sml
+++ b/micro-timl/cc.sml
@@ -569,7 +569,6 @@ fun cc e =
       | EAscTime (e, i) => EAscTime (cc e, i)
       | ENever t => ENever (cc_t t)
       | EBuiltin (name, t) => EBuiltin (name, cc_t t)
-      | EEmptyArray t => EEmptyArray (cc_t t)
       | ETriOp (ETWrite, e1, e2, e3) => EWrite (cc e1, cc e2, cc e3)
       | EHalt e => EHalt (cc e)
       | _ => raise Unimpl $ "cc(): " ^ (ExportPP.pp_e_to_string (NONE, NONE) $ ExportPP.export (NONE, NONE) ([], [], [], []) e)
diff --git a/micro-timl/code-gen.sml b/micro-timl/code-gen.sml
index 64a000d0..500f6cf7 100644
--- a/micro-timl/code-gen.sml
+++ b/micro-timl/code-gen.sml
@@ -86,7 +86,7 @@ fun cg_c c =
     | ECNat n => WCNat n
     | ECInt n => WCInt n
     | ECBool n => WCBool n
-    | ECString s => raise Impossible $ "cg_c() on ECString"
+    (* | ECString s => raise Impossible $ "cg_c() on ECString" *)
                                 
 fun cg_v ectx v =
   case v of
@@ -198,16 +198,14 @@ fun cg_e reg_counter (params as (ectx, itctx, rctx)) e =
                 end
               | EUnOp (EUInj (inj, t), v) =>
                 [IInj' (r, inj, cg_v ectx v, cg_t t)]
-              | EConst (ECString s) =>
-                [IString (r, s)]
+              (* | EConst (ECString s) => *)
+              (*   [IString (r, s)] *)
               | EUnOp (EUUnfold, v) =>
                 [IUnfold' (r, cg_v ectx v)]
               | EUnOp (EUTiML opr, v) =>
                 [IUnOp' (cg_expr_un_op opr, r, cg_v ectx v)]
               | EMallocPair (v1, v2) =>
                 [IMallocPair' (r, (cg_v ectx v1, cg_v ectx v2))]
-              | EEmptyArray t =>
-                [IEmptyArray (r, Inner $ cg_t t)]
               | EPairAssign (v1, proj, v2) =>
                 let
                   val r' = fresh_reg ()
diff --git a/micro-timl/cps.sml b/micro-timl/cps.sml
index 851d7ca8..8429ae4f 100644
--- a/micro-timl/cps.sml
+++ b/micro-timl/cps.sml
@@ -310,9 +310,6 @@ fun cps (e, t_e) (k, j_k) =
     | S.EBuiltin (name, t) =>
       (* [[ builtin ]](k) = k(builtin) *)
       (k $$ EBuiltin (name, cps_t t), j_k %+ T_1)
-    | S.EEmptyArray t =>
-      (* [[ empty_array ]](k) = let x = empty_array in k(x) *)
-      (k $$ EEmptyArray (cps_t t), j_k %+ T_1)
     | S.ERec bind =>
       (* [[ fix x.e ]](k) = k (fix x. [[e]](id)) *)
       let
@@ -564,8 +561,10 @@ fun cps (e, t_e) (k, j_k) =
                 in
                   (t_e, opr)
                 end
-              | EUTiML EUPrint =>
-                (TString, opr)
+              | EUTiML EUPrintc =>
+                (TByte, opr)
+              (* | EUTiML EUPrint => *)
+              (*   (TString, opr) *)
               | EUTiML EUInt2Str =>
                 (TInt, opr)
       in
@@ -846,7 +845,6 @@ and check_decl e =
          check_value e2;
          check_value e3)
       | EMallocPair _ => ()
-      | EEmptyArray _ => ()
       | EPairAssign (e1, _, e2) =>
         (check_value e1;
          check_value e2)
diff --git a/micro-timl/micro-timl-ex-pp.sml b/micro-timl/micro-timl-ex-pp.sml
index b4f6109b..d7868c16 100644
--- a/micro-timl/micro-timl-ex-pp.sml
+++ b/micro-timl/micro-timl-ex-pp.sml
@@ -636,16 +636,6 @@ fun pp_e (params as (str_var, str_i, str_s, str_k, pp_t)) s (depth_t, depth) e =
           str ")";
           close_box ()
         )
-      | EEmptyArray t =>
-        (
-          open_hbox ();
-          str "EEmptyArray";
-          space ();
-          str "(";
-          pp_t t;
-          str ")";
-          close_box ()
-        )
       | ENewArrayValues (t, es) =>
         (
           open_vbox ();
diff --git a/micro-timl/micro-timl-ex-util.sml b/micro-timl/micro-timl-ex-util.sml
index 69cdae48..7bb15077 100644
--- a/micro-timl/micro-timl-ex-util.sml
+++ b/micro-timl/micro-timl-ex-util.sml
@@ -22,14 +22,16 @@ fun MakeTUni (name, k, t) = TUni $ TBindAnno ((name, k), t)
 fun TUniKind (name, t) = MakeTUni (name, KType, t)
 fun TUniKind_Many (names, t) = foldr TUniKind t names
 
-val TCString = TCTiML BaseTypes.String
+(* val TCString = TCTiML BaseTypes.String *)
 val TCInt = TCTiML BaseTypes.Int
 val TCBool = TCTiML BaseTypes.Bool
+val TCByte = TCTiML BaseTypes.Byte
 val TUnit = TConst TCUnit
 val TEmpty = TConst TCEmpty
-val TString = TConst TCString
+(* val TString = TConst TCString *)
 val TInt = TConst TCInt
 val TBool = TConst TCBool
+val TByte = TConst TCByte
 fun TSum (t1, t2) = TBinOp (TBSum, t1, t2)
 fun TProd (t1, t2) = TBinOp (TBProd, t1, t2)
 fun TAppIs (t, is) = foldl (swap TAppI) t is
diff --git a/micro-timl/micro-timl-ex.sml b/micro-timl/micro-timl-ex.sml
index bf1453e5..96971855 100644
--- a/micro-timl/micro-timl-ex.sml
+++ b/micro-timl/micro-timl-ex.sml
@@ -31,7 +31,6 @@ datatype ('var, 'idx, 'sort, 'kind, 'ty) expr =
          | ENever of 'ty
          | EBuiltin of string * 'ty
          | ELet of ('var, 'idx, 'sort, 'kind, 'ty) expr * ('var, 'idx, 'sort, 'kind, 'ty) expr ebind
-         | EEmptyArray of 'ty
          | ENewArrayValues of 'ty * ('var, 'idx, 'sort, 'kind, 'ty) expr list
          (* extensions from MicroTiML *)
          | ELetIdx of 'idx * ('var, 'idx, 'sort, 'kind, 'ty) expr ibind
@@ -1132,7 +1131,6 @@ fun default_expr_visitor_vtable
           | EPairAssign data => #visit_EPairAssign vtable this env data
           | EProjProtected data => #visit_EProjProtected vtable this env data
           | EHalt data => #visit_EHalt vtable this env data
-          | EEmptyArray t => EEmptyArray $ #visit_ty vtable this env t
           | ENewArrayValues (t, es) => ENewArrayValues (#visit_ty vtable this env t, visit_list (#visit_expr vtable this) env es)
       end
     fun visit_EVar this env data =
@@ -1932,7 +1930,6 @@ fun is_value e =
     | EVar _ => true (* variables denote values *)
     | ENever _ => true
     | EBuiltin _ => true
-    | EEmptyArray _ => false
     | _ => false
     (* | _ => *)
     (*   case fst $ collect_EAscTypeTime $ fst $ collect_EAppIT e of *)
diff --git a/micro-timl/micro-timl-typecheck.sml b/micro-timl/micro-timl-typecheck.sml
index fac5e785..bba425a4 100644
--- a/micro-timl/micro-timl-typecheck.sml
+++ b/micro-timl/micro-timl-typecheck.sml
@@ -571,22 +571,22 @@ fun get_expr_const_type c =
       ECTT => TUnit
     | ECNat n => TNat $ INat n
     | ECInt _ => TInt
-    | ECString _ => TString
     | ECBool _ => TBool
+    (* | ECString _ => TString *)
 
 fun get_prim_expr_un_op_arg_ty opr =
   case opr of
       EUPIntNeg => TInt
     | EUPBoolNeg => TBool
-    | EUPInt2Str => TInt
-    | EUPStrLen => TString
+    (* | EUPInt2Str => TInt *)
+    (* | EUPStrLen => TString *)
                
 fun get_prim_expr_un_op_res_ty opr =
   case opr of
       EUPIntNeg => TInt
     | EUPBoolNeg => TBool
-    | EUPInt2Str => TString
-    | EUPStrLen => TInt
+    (* | EUPInt2Str => TString *)
+    (* | EUPStrLen => TInt *)
                
 fun get_prim_expr_bin_op_arg1_ty opr =
   case opr of
@@ -602,7 +602,7 @@ fun get_prim_expr_bin_op_arg1_ty opr =
     | EBPIntNEq => TInt
     | EBPBoolAnd => TBool
     | EBPBoolOr => TBool
-    | EBPStrConcat => TString
+    (* | EBPStrConcat => TString *)
       
 fun get_prim_expr_bin_op_arg2_ty opr =
   case opr of
@@ -618,7 +618,7 @@ fun get_prim_expr_bin_op_arg2_ty opr =
     | EBPIntNEq => TInt
     | EBPBoolAnd => TBool
     | EBPBoolOr => TBool
-    | EBPStrConcat => TString
+    (* | EBPStrConcat => TString *)
       
 fun get_prim_expr_bin_op_res_ty opr =
   case opr of
@@ -634,7 +634,7 @@ fun get_prim_expr_bin_op_res_ty opr =
     | EBPIntNEq => TBool
     | EBPBoolAnd => TBool
     | EBPBoolOr => TBool
-    | EBPStrConcat => TString
+    (* | EBPStrConcat => TString *)
 
 val T0 = T0 dummy
 val T1 = T1 dummy
@@ -813,12 +813,18 @@ fun tc (ctx as (ictx, tctx, ectx : econtext)) e_input =
         in
           (EProj (proj, e), choose (t1, t2) proj, i)
         end
-      | EUnOp (EUTiML EUPrint, e) =>
+      | EUnOp (EUTiML EUPrintc, e) =>
         let
-          val (e, i) = tc_against_ty ctx (e, TString)
+          val (e, i) = tc_against_ty ctx (e, TByte)
         in
-          (EUnOp (EUTiML EUPrint, e), TUnit, i)
+          (EUnOp (EUTiML EUPrintc, e), TUnit, i)
         end
+      (* | EUnOp (EUTiML EUPrint, e) => *)
+      (*   let *)
+      (*     val (e, i) = tc_against_ty ctx (e, TString) *)
+      (*   in *)
+      (*     (EUnOp (EUTiML EUPrint, e), TUnit, i) *)
+      (*   end *)
       | EUnOp (EUTiML (EUPrim opr), e) =>
         let
           val (e, i) = tc_against_ty ctx (e, get_prim_expr_un_op_arg_ty opr)
@@ -1288,12 +1294,6 @@ fun tc (ctx as (ictx, tctx, ectx : econtext)) e_input =
         in
           (EBuiltin (name, t), t, T0)
         end
-      | EEmptyArray t =>
-        let
-          val t = kc_against_kind itctx (t, KType)
-        in
-          (EEmptyArray t, TArr (t, N0 dummy), T0)
-        end
       (* | ELet data => *)
       (*   let *)
       (*     val (e1, (name, e2)) = unELet data *)
diff --git a/micro-timl/pair-alloc.sml b/micro-timl/pair-alloc.sml
index 02004866..1143a314 100644
--- a/micro-timl/pair-alloc.sml
+++ b/micro-timl/pair-alloc.sml
@@ -168,10 +168,10 @@ fun anf_decls_expr_visitor_vtable cast output =
             | ERec bind => false
             | ECase _ => false
             | ETriOp (ETIte, _, _, _) => false
-            | EConst c =>
-              (case c of
-                   ECString s => true (* string literal needs a standalone command *)
-                 | _ => false)
+            | EConst c => false
+              (* (case c of *)
+              (*      ECString s => true (* string literal needs a standalone command *) *)
+              (*    | _ => false) *)
             | EVar _ => false
             | EAscType _ => false
             | EAscTime _ => false
diff --git a/micro-timl/timl-to-micro-timl.sml b/micro-timl/timl-to-micro-timl.sml
index 91e86743..02770279 100644
--- a/micro-timl/timl-to-micro-timl.sml
+++ b/micro-timl/timl-to-micro-timl.sml
@@ -142,7 +142,6 @@ fun on_e (e : S.expr) =
       (case opr of
            Op.ETNever => ENever (on_mt t)
          | Op.ETBuiltin name => EBuiltin (name, on_mt t)
-         | Op.ETEmptyArray => EEmptyArray (on_mt t)
       )
     | S.ECaseSumbool (e, bind1, bind2, r) =>
       let
diff --git a/micro-timl/tital-eval.sml b/micro-timl/tital-eval.sml
index 25634bc3..c358f3b8 100644
--- a/micro-timl/tital-eval.sml
+++ b/micro-timl/tital-eval.sml
@@ -387,12 +387,6 @@ fun step (H, R, I) =
             in
               (H @+ (l, HVArray $ repeat n $ R @^ unInner v), R @+ (rd, WVLabel l), I')
             end
-          | IEmptyArray (rd, t) =>
-            let
-              val l = fresh_label H
-            in
-              (H @+ (l, HVArray []), R @+ (rd, WVLabel l), I')
-            end
           | IBinOp (IBRead, rd, rs, v) =>
             let
               val l = assert_WVLabel $ R @!! rs
diff --git a/micro-timl/tital-pp.sml b/micro-timl/tital-pp.sml
index 480840de..d034734b 100644
--- a/micro-timl/tital-pp.sml
+++ b/micro-timl/tital-pp.sml
@@ -322,18 +322,6 @@ fun pp_inst (params as (str_i, pp_t, pp_v)) s inst =
           str ")";
           close_box ()
         )
-      | IEmptyArray (r, t) =>
-        (
-          open_hbox ();
-          str "empty_array";
-          space ();
-          str "(";
-          str $ str_reg r;
-          comma ();
-          pp_t $ unInner t;
-          str ")";
-          close_box ()
-        )
       | IString (r, s) =>
         (
           open_hbox ();
diff --git a/micro-timl/tital-tc.sml b/micro-timl/tital-tc.sml
index 60edeb0a..370cb346 100644
--- a/micro-timl/tital-tc.sml
+++ b/micro-timl/tital-tc.sml
@@ -193,13 +193,20 @@ fun tc_insts (ctx as (hctx, itctx as (ictx, tctx), rctx)) insts =
             in
               i %+ T1
             end
-          | IUnOp (IUPrint, rd, v) =>
+          | IUnOp (IUPrintc, rd, v) =>
             let
-              val () = tc_v_against_ty ctx (unInner v, TString)
+              val () = tc_v_against_ty ctx (unInner v, TByte)
               val i = tc_insts (add_r (rd, TUnit) ctx) I
             in
               i %+ T1
             end
+          (* | IUnOp (IUPrint, rd, v) => *)
+          (*   let *)
+          (*     val () = tc_v_against_ty ctx (unInner v, TString) *)
+          (*     val i = tc_insts (add_r (rd, TUnit) ctx) I *)
+          (*   in *)
+          (*     i %+ T1 *)
+          (*   end *)
           | IUnOp (IUArrayLen, rd, v) =>
             let
               val t1 = tc_v ctx $ unInner v
@@ -355,12 +362,12 @@ fun tc_insts (ctx as (hctx, itctx as (ictx, tctx), rctx)) insts =
             in
               i %+ T1
             end
-          | IString (rd, s) =>
-            let
-              val i = tc_insts (add_r (rd, TString) ctx) I
-            in
-              i %+ T1
-            end
+          (* | IString (rd, s) => *)
+          (*   let *)
+          (*     val i = tc_insts (add_r (rd, TString) ctx) I *)
+          (*   in *)
+          (*     i %+ T1 *)
+          (*   end *)
           | IAscTime i =>
             let
               val i = sc_against_sort ictx (unInner i, STime)
@@ -369,14 +376,6 @@ fun tc_insts (ctx as (hctx, itctx as (ictx, tctx), rctx)) insts =
             in
               i
             end
-          | IEmptyArray (rd, t) =>
-            let
-              val t = kc_against_kind itctx (unInner t, KType)
-              val t = TArr (t, N0 dummy)
-              val i = tc_insts (add_r (rd, t) ctx) I
-            in
-              i %+ T1
-            end
       end
     fun extra_msg () = "\nwhen typechecking\n" ^ ((* substr 0 300 $  *)TiTALExportPP.pp_insts_to_string $ TiTALExportPP.export_insts (SOME 2, SOME 5) (itctx_names itctx) insts)
     val ret = main ()
diff --git a/micro-timl/tital-visitor.sml b/micro-timl/tital-visitor.sml
index eb5d65a3..2e453a36 100644
--- a/micro-timl/tital-visitor.sml
+++ b/micro-timl/tital-visitor.sml
@@ -237,7 +237,6 @@ fun default_tital_visitor_vtable
           | IInj data => #visit_IInj vtable this env data
           | IString data => #visit_IString vtable this env data
           | IAscTime data => #visit_IAscTime vtable this env data
-          | IEmptyArray (r, t) => IEmptyArray (r, visit_inner (#visit_ty vtable this) env t)
       end
     fun visit_IUnOp this env (opr, r, v) = 
       let
diff --git a/micro-timl/tital.sml b/micro-timl/tital.sml
index a55ab81f..5f5b93ad 100644
--- a/micro-timl/tital.sml
+++ b/micro-timl/tital.sml
@@ -61,7 +61,6 @@ datatype ('idx, 'ty) inst =
          | IUnpackI of ibinder * reg * ('idx, 'ty) value outer
          | IInj of reg * injector * ('idx, 'ty) value inner * 'ty inner
          | IString of reg * string
-         | IEmptyArray of reg * 'ty inner
          | IAscTime of 'idx inner
 
 datatype ('idx, 'ty) insts =
diff --git a/micro-timl/to-evm1.sml b/micro-timl/to-evm1.sml
index ffc8cdca..7c50d207 100644
--- a/micro-timl/to-evm1.sml
+++ b/micro-timl/to-evm1.sml
@@ -138,7 +138,7 @@ fun cg_c c =
     | ECNat n => WCNat n
     | ECInt n => WCInt n
     | ECBool n => WCBool n
-    | ECString s => raise Impossible $ "cg_c() on ECString"
+    (* | ECString s => raise Impossible $ "cg_c() on ECString" *)
                                 
 fun impl_prim_expr_un_opr opr =
   case opr of
@@ -230,8 +230,6 @@ fun compile ectx e =
       in
         compile e @ malloc_tuple [TiBoolConst b, t_e] @ [PUSH1 $ WiBool b, DUP2, MSTORE, SWAP1, DUP2, PUSH1nat 32, ADD, MSTORE, PACK_SUM (inj, t_other)]
       end
-    | EEmptyArray t =>
-      PUSH1nat 0 :: malloc_array (cg_t t)
     | ENewArrayValues (t, es) =>
       let
         val t = cg_t t
diff --git a/operators.sml b/operators.sml
index 8627ab2b..45024c1e 100644
--- a/operators.sml
+++ b/operators.sml
@@ -60,8 +60,9 @@ datatype expr_const =
          ECTT
          | ECNat of nat
          | ECInt of int
-         | ECString of string
          | ECBool of bool
+         | ECByte of String.char
+         (* | ECString of string *)
 
 (* projector for product type *)
 datatype projector =
@@ -72,23 +73,28 @@ datatype projector =
 datatype prim_expr_un_op =
          EUPIntNeg
          | EUPBoolNeg
-         | EUPInt2Str
-         | EUPStrLen
+         | EUPInt2Byte
+         | EUPByte2Int
+         (* | EUPInt2Str *)
+         (* | EUPStrLen *)
                          
 datatype expr_un_op =
          EUProj of projector
          | EUPrim of prim_expr_un_op
-         | EUPrint
          | EUArrayLen
          | EUNat2Int
+         | EUPInt2Nat
+         | EUPrintc
+         (* | EUPrint *)
 
 fun str_expr_const c =
   case c of
       ECTT => "()"
     | ECInt n => str_int n
     | ECNat n => sprintf "#$" [str_int n]
-    | ECString s => surround "\"" "\"" s
     | ECBool b => str_bool b
+    | ECByte c => Char.toCString c
+    (* | ECString s => surround "\"" "\"" s *)
                                 
 fun str_proj opr =
   case opr of
@@ -99,16 +105,17 @@ fun str_prim_expr_un_op opr =
   case opr of
       EUPIntNeg => "int_neg"
     | EUPBoolNeg => "not"
-    | EUPInt2Str => "int2str"
-    | EUPStrLen => "str_len"
+    (* | EUPInt2Str => "int2str" *)
+    (* | EUPStrLen => "str_len" *)
                    
 fun str_expr_un_op opr = 
   case opr of
       EUProj opr => str_proj opr
     | EUPrim opr => str_prim_expr_un_op opr
-    | EUPrint => "print"
     | EUArrayLen => "array_len"
     | EUNat2Int => "nat2int"
+    | EUPrintc => "printc"
+    (* | EUPrint => "print" *)
 
 (* primitive binary term operators *)
 datatype prim_expr_bin_op =
@@ -124,7 +131,7 @@ datatype prim_expr_bin_op =
          | EBPIntNEq
          | EBPBoolAnd
          | EBPBoolOr
-         | EBPStrConcat
+         (* | EBPStrConcat *)
 
 (* binary nat operators *)
 datatype nat_expr_bin_op =
@@ -164,7 +171,7 @@ fun str_prim_expr_bin_op opr =
     | EBPIntNEq => "neq"
     | EBPBoolAnd => "and"
     | EBPBoolOr => "or"
-    | EBPStrConcat => "str_concat"
+    (* | EBPStrConcat => "str_concat" *)
 
 fun str_nat_expr_bin_op opr =
   case opr of
@@ -206,7 +213,7 @@ fun pretty_str_prim_expr_bin_op opr =
     | EBPIntNEq => "<>"
     | EBPBoolAnd => "$$"
     | EBPBoolOr => "||"
-    | EBPStrConcat => "^"
+    (* | EBPStrConcat => "^" *)
 
 fun pretty_str_nat_expr_bin_op opr =
   case opr of
@@ -254,7 +261,7 @@ datatype expr_ET =
 datatype expr_T =
          ETNever
          | ETBuiltin of string
-         | ETEmptyArray
+         (* | ETEmptyArray *)
              
 fun str_idx_const c =
   case c of
@@ -330,6 +337,5 @@ fun str_expr_T opr =
   case opr of
       ETNever => "ETNever"
     | ETBuiltin name => sprintf "ETBuiltin($)" [name]
-    | ETEmptyArray => "ETEmptyArray"
                   
 end
diff --git a/parser/ast.sml b/parser/ast.sml
index f0e328ab..8ff2ff89 100644
--- a/parser/ast.sml
+++ b/parser/ast.sml
@@ -113,6 +113,7 @@ datatype exp =
          | BinOp of expr_bin_op * exp * exp * region
          | ETriOp of expr_tri_op * exp * exp * exp * region
          | ENever of region
+         | EStrConcat of exp * exp * region
 
      and decl =
          Val of id list * ptrn * exp * region
diff --git a/parser/timl.grm b/parser/timl.grm
index f122518f..471dca63 100644
--- a/parser/timl.grm
+++ b/parser/timl.grm
@@ -287,7 +287,7 @@ exp : aexp (aexp)
      | exp NAT_NEQ exp (BinOp (EBNatCmp NCNEq, exp1, exp2, (exp1left, exp2right)))
      | exp DOUBLE_POND exp (BinOp (EBPrim EBPBoolAnd, exp1, exp2, (exp1left, exp2right)))
      | exp DOUBLE_BAR exp (BinOp (EBPrim EBPBoolOr, exp1, exp2, (exp1left, exp2right)))
-     | exp STR_CONCAT exp (BinOp (EBPrim EBPStrConcat, exp1, exp2, (exp1left, exp2right)))
+     | exp STR_CONCAT exp (EStrConcat (exp1, exp2, (exp1left, exp2right)))
      | exp LTRI exp (App (exp1, exp2, (exp1left, exp2right)))
      | exp SEMI_COLON exp (ESemiColon (exp1, exp2, (exp1left, exp2right)))
      | exp DCOLON exp (ECons (exp1, exp2, (exp1left, exp2right)))
diff --git a/typecheck-main.sml b/typecheck-main.sml
index c7ab77d2..7392380b 100644
--- a/typecheck-main.sml
+++ b/typecheck-main.sml
@@ -902,27 +902,29 @@ fun get_expr_const_type (c, r) =
       else
 	raise Error (r, ["Natural number constant must be non-negative"])
     | ECTT => 
-      Unit dummy
+      Unit r
     | ECInt n => 
-      BaseType (Int, dummy)
-    | ECString s => 
-      BaseType (String, dummy)
+      BaseType (Int, r)
     | ECBool _ => 
-      BaseType (Bool, dummy)
+      BaseType (Bool, r)
+    | ECByte _ =>
+      BaseType (Byte, r)
+    (* | ECString s =>  *)
+    (*   BaseType (String, r) *)
 
 fun get_prim_expr_un_op_arg_ty opr =
   case opr of
       EUPIntNeg => Int
     | EUPBoolNeg => Bool
-    | EUPInt2Str => Int
-    | EUPStrLen => String
+    (* | EUPInt2Str => Int *)
+    (* | EUPStrLen => String *)
                
 fun get_prim_expr_un_op_res_ty opr =
   case opr of
       EUPIntNeg => Int
     | EUPBoolNeg => Bool
-    | EUPInt2Str => String
-    | EUPStrLen => Int
+    (* | EUPInt2Str => String *)
+    (* | EUPStrLen => Int *)
                
 fun get_prim_expr_bin_op_arg1_ty opr =
   case opr of
@@ -938,7 +940,7 @@ fun get_prim_expr_bin_op_arg1_ty opr =
     | EBPIntNEq => Int
     | EBPBoolAnd => Bool
     | EBPBoolOr => Bool
-    | EBPStrConcat => String
+    (* | EBPStrConcat => String *)
       
 fun get_prim_expr_bin_op_arg2_ty opr =
   case opr of
@@ -954,7 +956,7 @@ fun get_prim_expr_bin_op_arg2_ty opr =
     | EBPIntNEq => Int
     | EBPBoolAnd => Bool
     | EBPBoolOr => Bool
-    | EBPStrConcat => String
+    (* | EBPStrConcat => String *)
       
 fun get_prim_expr_bin_op_res_ty opr =
   case opr of
@@ -970,7 +972,7 @@ fun get_prim_expr_bin_op_res_ty opr =
     | EBPIntNEq => Bool
     | EBPBoolAnd => Bool
     | EBPBoolOr => Bool
-    | EBPStrConcat => String
+    (* | EBPStrConcat => String *)
 
 fun get_mtype gctx (ctx as (sctx : scontext, kctx : kcontext, cctx : ccontext, tctx : tcontext), e_all : U.expr) : expr * mtype * idx =
   let
@@ -1067,23 +1069,29 @@ fun get_mtype gctx (ctx as (sctx : scontext, kctx : kcontext, cctx : ccontext, t
                in 
                  (ESnd (e, r), t2, d)
 	       end
-             | EUPrint =>
+             | EUPrintc =>
                let
-                 val (e, _, d) = check_mtype (ctx, e, BaseType (String, dummy)) 
+                 val (e, _, d) = check_mtype (ctx, e, BaseType (Byte, r)) 
                in
-                 (EUnOp (EUPrint, e, r), Unit dummy, d)
+                 (EUnOp (EUPrintc, e, r), Unit r, d)
                end
+             (* | EUPrint => *)
+             (*   let *)
+             (*     val (e, _, d) = check_mtype (ctx, e, BaseType (String, dummy))  *)
+             (*   in *)
+             (*     (EUnOp (EUPrint, e, r), Unit dummy, d) *)
+             (*   end *)
              | EUPrim opr =>
                let
-                 val (e, _, d) = check_mtype (ctx, e, BaseType (get_prim_expr_un_op_arg_ty opr, dummy)) 
+                 val (e, _, d) = check_mtype (ctx, e, BaseType (get_prim_expr_un_op_arg_ty opr, r)) 
                in
-                 (EUnOp (EUPrim opr, e, r), BaseType (get_prim_expr_un_op_res_ty opr, dummy), d)
+                 (EUnOp (EUPrim opr, e, r), BaseType (get_prim_expr_un_op_res_ty opr, r), d)
                end
 	     | EUArrayLen =>
                let
                  val r = U.get_region_e e_all
                  val t = fresh_mt gctx (sctx, kctx) r
-                 val i = fresh_i gctx sctx (Base Time) r
+                 val i = fresh_i gctx sctx (Base Time(*bug*)) r
                  val (e, _, d) = check_mtype (ctx, e, TyArray (t, i))
                in
                  (EUnOp (opr, e, r), TyNat (i, r), d)
@@ -1091,11 +1099,20 @@ fun get_mtype gctx (ctx as (sctx : scontext, kctx : kcontext, cctx : ccontext, t
 	     | EUNat2Int =>
                let
                  val r = U.get_region_e e_all
-                 val i = fresh_i gctx sctx (Base Time) r
+                 val i = fresh_i gctx sctx (Base Time(*bug*)) r
                  val (e, _, d) = check_mtype (ctx, e, TyNat (i, r))
                in
                  (EUnOp (opr, e, r), BaseType (Int, r), d)
                end
+	     | EUInt2Nat =>
+               let
+                 val r = U.get_region_e e_all
+                 val (e, _, d) = check_mtype (ctx, e, BaseType (Int, r))
+                 fun add_r r (name, x) = ((name, r), (x, r))
+                 val SOME_NAT_ID = ("Pervasive", 0)
+               in
+                 (EUnOp (opr, e, r), MtVar $ QID $ add_r r SOME_NAT_ID, d)
+               end
           )
 	| U.EBinOp (opr, e1, e2) =>
           (case opr of