diff --git a/src/ast_typed/combinators.ml b/src/ast_typed/combinators.ml
index 78aa8a4a6..32e25f2ec 100644
--- a/src/ast_typed/combinators.ml
+++ b/src/ast_typed/combinators.ml
@@ -138,16 +138,15 @@ let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value'
   | _ -> simple_fail "not a record type"
 
 let get_t_map (t:type_value) : (type_value * type_value) result =
-  match t.type_value' with
-  | T_constant ("map", [k;v]) -> ok (k, v)
-  | T_constant ("big_map", [k;v]) -> ok (k, v)
-  | _ -> simple_fail "get: not a map or a big_map"
-
-let get_t_map_not_big_map (t:type_value) : (type_value * type_value) result =
   match t.type_value' with
   | T_constant ("map", [k;v]) -> ok (k, v)
   | _ -> simple_fail "get: not a map"
 
+let get_t_big_map (t:type_value) : (type_value * type_value) result =
+  match t.type_value' with
+  | T_constant ("big_map", [k;v]) -> ok (k, v)
+  | _ -> simple_fail "get: not a big_map"
+
 let get_t_map_key : type_value -> type_value result = fun t ->
   let%bind (key , _) = get_t_map t in
   ok key
@@ -156,11 +155,20 @@ let get_t_map_value : type_value -> type_value result = fun t ->
   let%bind (_ , value) = get_t_map t in
   ok value
 
+let get_t_big_map_key : type_value -> type_value result = fun t ->
+  let%bind (key , _) = get_t_big_map t in
+  ok key
+
+let get_t_big_map_value : type_value -> type_value result = fun t ->
+  let%bind (_ , value) = get_t_big_map t in
+  ok value
+
 let assert_t_map = fun t ->
   let%bind _ = get_t_map t in
   ok ()
 
-let is_t_map_not_big_map = Function.compose to_bool get_t_map_not_big_map
+let is_t_map = Function.compose to_bool get_t_map
+let is_t_big_map = Function.compose to_bool get_t_big_map
 
 let assert_t_tez : type_value -> unit result = get_t_tez
 let assert_t_key = get_t_key
diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml
index 789000391..83d80e1b9 100644
--- a/src/compiler/compiler_program.ml
+++ b/src/compiler/compiler_program.ml
@@ -35,7 +35,7 @@ let get_predicate : string -> type_value -> expression list -> predicate result
       | "MAP_REMOVE" ->
           let%bind v = match lst with
             | [ _ ; expr ] ->
-                let%bind (_, v) = Mini_c.Combinators.(get_t_map (Expression.get_type expr)) in
+                let%bind (_, v) = Mini_c.Combinators.(bind_map_or (get_t_map , get_t_big_map) (Expression.get_type expr)) in
                 ok v
             | _ -> simple_fail "mini_c . MAP_REMOVE" in
           let%bind v_ty = Compiler_type.type_ v in
@@ -107,6 +107,15 @@ let rec translate_value (v:value) ty : michelson result = match v with
       let aux (a, b) = prim ~children:[a;b] D_Elt in
       ok @@ seq @@ List.map aux sorted
     )
+  | D_big_map lst -> (
+      let%bind (k_ty , v_ty) = get_t_big_map ty in
+      let%bind lst' =
+        let aux (k , v) = bind_pair (translate_value k k_ty , translate_value v v_ty) in
+        bind_map_list aux lst in
+      let sorted = List.sort (fun (x , _) (y , _) -> compare x y) lst' in
+      let aux (a, b) = prim ~children:[a;b] D_Elt in
+      ok @@ seq @@ List.map aux sorted
+    )
   | D_list lst -> (
       let%bind e_ty = get_t_list ty in
       let%bind lst' = bind_map_list (fun x -> translate_value x e_ty) lst in
diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml
index c7eab992d..46f39f766 100644
--- a/src/mini_c/PP.ml
+++ b/src/mini_c/PP.ml
@@ -62,6 +62,7 @@ let rec value ppf : value -> unit = function
   | D_none -> fprintf ppf "None"
   | D_some s -> fprintf ppf "Some (%a)" value s
   | D_map m -> fprintf ppf "Map[%a]" (list_sep_d value_assoc) m
+  | D_big_map m -> fprintf ppf "Big_map[%a]" (list_sep_d value_assoc) m
   | D_list lst -> fprintf ppf "List[%a]" (list_sep_d value) lst
   | D_set lst -> fprintf ppf "Set[%a]" (list_sep_d value) lst
 
diff --git a/src/mini_c/combinators.ml b/src/mini_c/combinators.ml
index 5cc9d2ae4..f2639ebf6 100644
--- a/src/mini_c/combinators.ml
+++ b/src/mini_c/combinators.ml
@@ -62,6 +62,10 @@ let get_map (v:value) = match v with
   | D_map lst -> ok lst
   | _ -> simple_fail "not a map"
 
+let get_big_map (v:value) = match v with
+  | D_big_map lst -> ok lst
+  | _ -> simple_fail "not a big_map"
+
 let get_list (v:value) = match v with
   | D_list lst -> ok lst
   | _ -> simple_fail "not a list"
@@ -88,9 +92,12 @@ let get_t_or (t:type_value) = match t with
 
 let get_t_map (t:type_value) = match t with
   | T_map kv -> ok kv
-  | T_big_map kv -> ok kv
   | _ -> simple_fail "not a type map"
 
+let get_t_big_map (t:type_value) = match t with
+  | T_big_map kv -> ok kv
+  | _ -> simple_fail "not a type big_map"
+
 let get_t_list (t:type_value) = match t with
   | T_list t -> ok t
   | _ -> simple_fail "not a type list"
diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml
index 8be621954..dba508062 100644
--- a/src/mini_c/types.ml
+++ b/src/mini_c/types.ml
@@ -48,6 +48,7 @@ type value =
   | D_some of value
   | D_none
   | D_map of (value * value) list
+  | D_big_map of (value * value) list
   | D_list of value list
   | D_set of value list
   (* | `Macro of anon_macro ... The future. *)
diff --git a/src/operators/operators.ml b/src/operators/operators.ml
index 3db1919f1..5989fed0f 100644
--- a/src/operators/operators.ml
+++ b/src/operators/operators.ml
@@ -235,53 +235,53 @@ module Typer = struct
     ok tl
 
   let map_remove : typer = typer_2 "MAP_REMOVE" @@ fun k m ->
-    let%bind (src , _) = get_t_map m in
+    let%bind (src , _) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind () = assert_type_value_eq (src , k) in
     ok m
 
   let map_add : typer = typer_3 "MAP_ADD" @@ fun k v m ->
-    let%bind (src, dst) = get_t_map m in
+    let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind () = assert_type_value_eq (src, k) in
     let%bind () = assert_type_value_eq (dst, v) in
     ok m
 
   let map_update : typer = typer_3 "MAP_UPDATE" @@ fun k v m ->
-    let%bind (src, dst) = get_t_map m in
+    let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind () = assert_type_value_eq (src, k) in
     let%bind v' = get_t_option v in
     let%bind () = assert_type_value_eq (dst, v') in
     ok m
 
   let map_mem : typer = typer_2 "MAP_MEM" @@ fun k m ->
-    let%bind (src, _dst) = get_t_map m in
+    let%bind (src, _dst) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind () = assert_type_value_eq (src, k) in
     ok @@ t_bool ()
 
   let map_find : typer = typer_2 "MAP_FIND" @@ fun k m ->
-    let%bind (src, dst) = get_t_map m in
+    let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind () = assert_type_value_eq (src, k) in
     ok @@ dst
 
   let map_find_opt : typer = typer_2 "MAP_FIND_OPT" @@ fun k m ->
-    let%bind (src, dst) = get_t_map m in
+    let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind () = assert_type_value_eq (src, k) in
     ok @@ t_option dst ()
 
   let map_iter : typer = typer_2 "MAP_ITER" @@ fun m f ->
-    let%bind (k, v) = get_t_map_not_big_map m in
+    let%bind (k, v) = get_t_map m in
     let%bind (arg , res) = get_t_function f in
     let%bind () = assert_eq_1 arg (t_pair k v ()) in
     let%bind () = assert_eq_1 res (t_unit ()) in
     ok @@ t_unit ()
 
   let map_map : typer = typer_2 "MAP_MAP" @@ fun m f ->
-    let%bind (k, v) = get_t_map_not_big_map m in
+    let%bind (k, v) = get_t_map m in
     let%bind (arg , res) = get_t_function f in
     let%bind () = assert_eq_1 arg (t_pair k v ()) in
     ok @@ t_map k res ()
 
   let map_fold : typer = typer_2 "MAP_FOLD" @@ fun f m ->
-    let%bind (k, v) = get_t_map_not_big_map m in
+    let%bind (k, v) = get_t_map m in
     let%bind (arg_1 , res) = get_t_function f in
     let%bind (arg_2 , res') = get_t_function res in
     let%bind (arg_3 , res'') = get_t_function res' in
@@ -293,7 +293,7 @@ module Typer = struct
   let size = typer_1 "SIZE" @@ fun t ->
     let%bind () =
       Assert.assert_true @@
-      (is_t_map_not_big_map t || is_t_list t || is_t_string t || is_t_bytes t || is_t_set t) in
+      (is_t_map t || is_t_list t || is_t_string t || is_t_bytes t || is_t_set t ) in
     ok @@ t_nat ()
 
   let slice = typer_3 "SLICE" @@ fun i j s ->
@@ -312,7 +312,7 @@ module Typer = struct
     ok @@ t_unit ()
 
   let get_force = typer_2 "MAP_GET_FORCE" @@ fun i m ->
-    let%bind (src, dst) = get_t_map m in
+    let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) m in
     let%bind _ = assert_type_value_eq (src, i) in
     ok dst
 
@@ -641,6 +641,8 @@ module Compiler = struct
     ("MAP_GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
     ("MAP_FIND" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "MAP FIND")]) ;
     ("MAP_GET" , simple_binary @@ prim I_GET) ;
+    ("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE]) ;
+    ("MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ;
     ("SIZE" , simple_unary @@ prim I_SIZE) ;
     ("FAILWITH" , simple_unary @@ prim I_FAILWITH) ;
     ("ASSERT_INFERRED" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
@@ -655,8 +657,6 @@ module Compiler = struct
     ("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ;
     ("SOURCE" , simple_constant @@ prim I_SOURCE) ;
     ("SENDER" , simple_constant @@ prim I_SENDER) ;
-    ("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE]) ;
-    ("MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ;
     ("SET_MEM" , simple_binary @@ prim I_MEM) ;
     ("SET_ADD" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_True)) ; prim I_UPDATE]) ;
     ("SET_REMOVE" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_False)) ; prim I_UPDATE]) ;
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 56da73d5e..ebd71877e 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -434,7 +434,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
       let%bind (init : expression) = return @@ E_make_empty_set t in
       bind_fold_list aux init lst'
     )
-  | (E_map m | E_big_map m) -> (
+  | E_map m -> (
       let%bind (src, dst) =
         trace_strong (corner_case ~loc:__LOC__ "not a map") @@
         Mini_c.Combinators.get_t_map tv in
@@ -448,6 +448,20 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
       let init = return @@ E_make_empty_map (src, dst) in
       List.fold_left aux init m
     )
+  | E_big_map m -> (
+      let%bind (src, dst) =
+        trace_strong (corner_case ~loc:__LOC__ "not a map") @@
+        Mini_c.Combinators.get_t_big_map tv in
+      let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev (k, v) ->
+        let%bind prev' = prev in
+        let%bind (k', v') =
+          let v' = e_a_some v ae.environment in
+          bind_map_pair (translate_annotated_expression) (k , v') in
+        return @@ E_constant ("UPDATE", [k' ; v' ; prev'])
+      in
+      let init = return @@ E_make_empty_map (src, dst) in
+      List.fold_left aux init m
+    )
   | E_look_up dsi -> (
       let%bind (ds', i') = bind_map_pair f dsi in
       return @@ E_constant ("MAP_GET", [i' ; ds'])
@@ -800,8 +814,8 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
     )
   | T_constant ("big_map", [k_ty;v_ty]) -> (
       let%bind lst =
-        trace_strong (wrong_mini_c_value "map" v) @@
-        get_map v in
+        trace_strong (wrong_mini_c_value "big_map" v) @@
+        get_big_map v in
       let%bind lst' =
         let aux = fun (k, v) ->
           let%bind k' = untranspile k k_ty in
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index c95ec44fb..5122e86aa 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -451,7 +451,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
           )
         | Access_map ae' -> (
             let%bind ae'' = type_expression e ae' in
-            let%bind (k , v) = get_t_map prev.type_annotation in
+            let%bind (k , v) = bind_map_or (get_t_map , get_t_big_map) prev.type_annotation in
             let%bind () =
               Ast_typed.assert_type_value_eq (k , get_type_annotation ae'') in
             return (E_look_up (prev , ae'')) v
@@ -570,7 +570,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             bind_fold_list aux None
             @@ List.map get_type_annotation
             @@ List.map fst lst' in
-          let%bind annot = bind_map_option get_t_map_key tv_opt in
+          let%bind annot = bind_map_option get_t_big_map_key tv_opt in
           trace (simple_info "empty map expression without a type annotation") @@
           O.merge_annotation annot sub (needs_annotation ae "this map literal")
         in
@@ -579,7 +579,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
             bind_fold_list aux None
             @@ List.map get_type_annotation
             @@ List.map snd lst' in
-          let%bind annot = bind_map_option get_t_map_value tv_opt in
+          let%bind annot = bind_map_option get_t_big_map_value tv_opt in
           trace (simple_info "empty map expression without a type annotation") @@
           O.merge_annotation annot sub (needs_annotation ae "this map literal")
         in
@@ -644,7 +644,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
       return (E_application (f' , arg)) tv
   | E_look_up dsi ->
       let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
-      let%bind (src, dst) = get_t_map ds.type_annotation in
+      let%bind (src, dst) = bind_map_or (get_t_map , get_t_big_map) ds.type_annotation in
       let%bind _ = O.assert_type_value_eq (ind.type_annotation, src) in
       return (E_look_up (ds , ind)) (t_option dst ())
   (* Advanced *)