diff --git a/src/bin/cli.ml b/src/bin/cli.ml
index 4cac0fe45..3ca3d2bf3 100644
--- a/src/bin/cli.ml
+++ b/src/bin/cli.ml
@@ -37,6 +37,14 @@ let syntax =
     info ~docv ~doc ["syntax" ; "s"] in
   value @@ opt string "auto" info
 
+let bigmap =
+  let open Arg in
+  let info =
+    let docv = "BIGMAP" in
+    let doc = "$(docv) is necessary when your storage embeds a big_map." in
+    info ~docv ~doc ["bigmap"] in
+  value @@ flag info
+
 let amount =
   let open Arg in
   let info =
@@ -91,28 +99,28 @@ let compile_parameter =
   (term , Term.info ~docs cmdname)
 
 let compile_storage =
-  let f source entry_point expression syntax display_format =
+  let f source entry_point expression syntax display_format bigmap =
     toplevel ~display_format @@
     let%bind value =
       trace (simple_error "compile-storage") @@
-      Ligo.Compile.Of_source.compile_file_contract_storage source entry_point expression (Syntax_name syntax) in
+      Ligo.Compile.Of_source.compile_file_contract_storage ~value:bigmap source entry_point expression (Syntax_name syntax) in
     ok @@ Format.asprintf "%a\n" Tezos_utils.Michelson.pp value
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ expression "STORAGE" 2 $ syntax $ display_format) in
+    Term.(const f $ source 0 $ entry_point 1 $ expression "STORAGE" 2 $ syntax $ display_format $ bigmap) in
   let cmdname = "compile-storage" in
   let docs = "Subcommand: compile an initial storage in ligo syntax to a michelson expression. The resulting michelson expression can be passed as an argument in a transaction which originates a contract. See `ligo " ^ cmdname ^ " --help' for a list of options specific to this subcommand." in
   (term , Term.info ~docs cmdname)
 
 let dry_run =
-  let f source entry_point storage input amount syntax display_format =
+  let f source entry_point storage input amount syntax display_format bigmap =
     toplevel ~display_format @@
     let%bind output =
-      Ligo.Run.Of_source.run_contract ~amount source entry_point storage input (Syntax_name syntax) in
+      Ligo.Run.Of_source.run_contract ~amount ~storage_value:bigmap source entry_point storage input (Syntax_name syntax) in
     ok @@ Format.asprintf "%a\n" Ast_simplified.PP.expression output
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ expression "PARAMETER" 2 $ expression "STORAGE" 3 $ amount $ syntax $ display_format) in
+    Term.(const f $ source 0 $ entry_point 1 $ expression "PARAMETER" 2 $ expression "STORAGE" 3 $ amount $ syntax $ display_format $ bigmap) in
   let cmdname = "dry-run" in
   let docs = "Subcommand: run a smart-contract with the given storage and input." in
   (term , Term.info ~docs cmdname)
diff --git a/src/main/compile/of_mini_c.ml b/src/main/compile/of_mini_c.ml
index 5a1ff886e..34d8cd753 100644
--- a/src/main/compile/of_mini_c.ml
+++ b/src/main/compile/of_mini_c.ml
@@ -5,8 +5,16 @@ open Tezos_utils
 let compile_value : value -> type_value -> Michelson.t result =
   Compiler.Program.translate_value
 
-let compile_expression : expression -> _ result = fun e ->
-  Compiler.Program.translate_expression e Compiler.Environment.empty
+let compile_expression ?(value = false)  : expression -> _ result = fun e ->
+  if value then (
+    let%bind value = expression_to_value e in
+    Format.printf "Compile to value\n" ;
+    let%bind result = compile_value value e.type_value in
+    Format.printf "Compiled to value\n" ;
+    ok result
+  ) else (
+    Compiler.Program.translate_expression e Compiler.Environment.empty
+  )
 
 let compile_expression_as_function : expression -> _ result = fun e ->
   let (input , output) = t_unit , e.type_value in
diff --git a/src/main/compile/of_simplified.ml b/src/main/compile/of_simplified.ml
index fa27f3d6e..215c908a5 100644
--- a/src/main/compile/of_simplified.ml
+++ b/src/main/compile/of_simplified.ml
@@ -14,9 +14,9 @@ let compile_expression_as_function_entry (program : program) entry_point : _ res
   let%bind typed_program = Typer.type_program program in
   Of_typed.compile_expression_as_function_entry typed_program entry_point
 
-let compile_expression ?(env = Ast_typed.Environment.full_empty) ae : Michelson.t result =
+let compile_expression ?(env = Ast_typed.Environment.full_empty) ?value ae : Michelson.t result =
   let%bind typed = Typer.type_expression env ae in
-  Of_typed.compile_expression typed
+  Of_typed.compile_expression ?value typed
 
 let uncompile_typed_program_entry_expression_result program entry ex_ty_value =
   let%bind output_type =
diff --git a/src/main/compile/of_source.ml b/src/main/compile/of_source.ml
index 169dba0da..42c6adf91 100644
--- a/src/main/compile/of_source.ml
+++ b/src/main/compile/of_source.ml
@@ -30,19 +30,19 @@ let compile_file_expression : string -> string -> string -> s_syntax -> Michelso
   let%bind simplified = parsify_expression syntax expression in
   Of_simplified.compile_expression simplified
 
-let compile_file_contract_storage : string -> string -> string -> s_syntax -> Michelson.t result =
+let compile_file_contract_storage ~value : string -> string -> string -> s_syntax -> Michelson.t result =
   fun source_filename _entry_point expression syntax ->
   let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind simplified = parsify_expression syntax expression in
-  Of_simplified.compile_expression simplified
+  Of_simplified.compile_expression ~value simplified
 
 let compile_file_contract_args =
-  fun source_filename _entry_point storage parameter syntax ->
+  fun ?value source_filename _entry_point storage parameter syntax ->
   let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind storage_simplified = parsify_expression syntax storage in
   let%bind parameter_simplified = parsify_expression syntax parameter in
   let args = Ast_simplified.e_pair storage_simplified parameter_simplified in
-  Of_simplified.compile_expression args
+  Of_simplified.compile_expression ?value args
 
 let type_file ?(debug_simplify = false) ?(debug_typed = false)
     syntax (source_filename:string) : Ast_typed.program result =
diff --git a/src/main/compile/of_typed.ml b/src/main/compile/of_typed.ml
index e6a33abd7..e8ac1e8e7 100644
--- a/src/main/compile/of_typed.ml
+++ b/src/main/compile/of_typed.ml
@@ -3,9 +3,9 @@ open Ast_typed
 open Tezos_utils
 
 
-let compile_expression : annotated_expression -> Michelson.t result = fun e ->
+let compile_expression ?(value = false) : annotated_expression -> Michelson.t result = fun e ->
   let%bind mini_c_expression = Transpiler.transpile_annotated_expression e in
-  let%bind expr = Of_mini_c.compile_expression mini_c_expression in
+  let%bind expr = Of_mini_c.compile_expression ~value mini_c_expression in
   ok expr
 
 let compile_expression_as_function : annotated_expression -> _ result = fun e ->
diff --git a/src/main/run/of_simplified.ml b/src/main/run/of_simplified.ml
index 4332ca9e5..9c5d830cc 100644
--- a/src/main/run/of_simplified.ml
+++ b/src/main/run/of_simplified.ml
@@ -7,15 +7,15 @@ let get_final_environment program =
   post_env
 
 let run_typed_program
-    ?options
+    ?options ?input_to_value
     (program : Ast_typed.program) (entry : string)
     (input : expression) : expression result =
   let%bind code = Compile.Of_typed.compile_function_entry program entry in
   let%bind input =
     let env = get_final_environment program in
-    Compile.Of_simplified.compile_expression ~env input
+    Compile.Of_simplified.compile_expression ~env ?value:input_to_value input
   in
-  let%bind ex_ty_value = Of_michelson.run ?options code input in
+  let%bind ex_ty_value = Of_michelson.run ?is_input_value:input_to_value ?options code input in
   Compile.Of_simplified.uncompile_typed_program_entry_function_result program entry ex_ty_value
 
 let evaluate_typed_program_entry
diff --git a/src/main/run/of_source.ml b/src/main/run/of_source.ml
index 5bc8b421c..3014cbbb7 100644
--- a/src/main/run/of_source.ml
+++ b/src/main/run/of_source.ml
@@ -46,10 +46,10 @@ include struct
     ok ()
 end
 
-let run_contract ?amount source_filename entry_point storage parameter syntax =
+let run_contract ?amount ?storage_value source_filename entry_point storage parameter syntax =
   let%bind program = Compile.Of_source.type_file syntax source_filename in
   let%bind code = Compile.Of_typed.compile_function_entry program entry_point in
-  let%bind args = Compile.Of_source.compile_file_contract_args source_filename entry_point storage parameter syntax in
+  let%bind args = Compile.Of_source.compile_file_contract_args ?value:storage_value source_filename entry_point storage parameter syntax in
   let%bind ex_value_ty =
     let options =
       let open Proto_alpha_utils.Memory_proto_alpha in
diff --git a/src/passes/3-self_ast_simplified/helpers.ml b/src/passes/3-self_ast_simplified/helpers.ml
index 61aa8fcb2..505264b80 100644
--- a/src/passes/3-self_ast_simplified/helpers.ml
+++ b/src/passes/3-self_ast_simplified/helpers.ml
@@ -20,6 +20,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e ->
     let%bind lst' = bind_map_list (bind_map_pair self) lst in
     return @@ E_map lst'
   )
+  | E_big_map lst -> (
+    let%bind lst' = bind_map_list (bind_map_pair self) lst in
+    return @@ E_big_map lst'
+  )
   | E_sequence ab -> (
       let%bind ab' = bind_map_pair self ab in
       return @@ E_sequence ab'
diff --git a/src/passes/4-typer/typer.ml b/src/passes/4-typer/typer.ml
index cd27b1cf4..2cacd1629 100644
--- a/src/passes/4-typer/typer.ml
+++ b/src/passes/4-typer/typer.ml
@@ -447,7 +447,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
@@ -551,6 +551,36 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
         ok (t_map key_type value_type ())
       in
       return (E_map lst') tv
+  | E_big_map lst ->
+      let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
+      let%bind tv =
+        let aux opt c =
+          match opt with
+          | None -> ok (Some c)
+          | Some c' ->
+              let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
+              ok (Some c') in
+        let%bind key_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map fst lst' 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
+        let%bind value_type =
+          let%bind sub =
+            bind_fold_list aux None
+            @@ List.map get_type_annotation
+            @@ List.map snd lst' 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
+        ok (t_big_map key_type value_type ())
+      in
+      return (E_big_map lst') tv
   | E_lambda {
       binder ;
       input_type ;
@@ -609,7 +639,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 *)
@@ -822,6 +852,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
   | E_map m ->
       let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
       return (e_map m')
+  | E_big_map m ->
+      let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
+      return (e_big_map m')
   | E_list lst ->
       let%bind lst' = bind_map_list untype_expression lst in
       return (e_list lst')
diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml
index 76ca3a770..9fbf55374 100644
--- a/src/passes/6-transpiler/transpiler.ml
+++ b/src/passes/6-transpiler/transpiler.ml
@@ -5,7 +5,6 @@ module AST = Ast_typed
 module Append_tree = Tree.Append
 open AST.Combinators
 open Mini_c
-open Combinators
 
 let untranspile = Untranspiler.untranspile
 
@@ -46,6 +45,58 @@ them. please report this to the developers." in
         row_loc location ;
       ] in
     error ~data title content
+
+  let not_functional_main location =
+    let title () = "not functional main" in
+    let content () = "main should be a function" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp location) ;
+    ] in
+    error ~data title content
+
+  let bad_big_map location =
+    let title () = "bad arguments for main" in
+    let content () = "only one big_map per program which must appear 
+      on the left hand side of a pair in the contract's storage" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp location) ;
+    ] in
+    error ~data title content
+
+  let missing_entry_point name =
+    let title () = "missing entry point" in
+    let content () = "no entry point with the given name" in
+    let data = [
+      ("name" , fun () -> name) ;
+    ] in
+    error ~data title content
+
+  let wrong_mini_c_value expected_type actual =
+    let title () = "illed typed intermediary value" in
+    let content () = "type of intermediary value doesn't match what was expected" in
+    let data = [
+      ("expected_type" , fun () -> expected_type) ;
+      ("actual" , fun () -> Format.asprintf "%a" Mini_c.PP.value actual ) ;
+    ] in
+    error ~data title content
+
+  let bad_untranspile bad_type value =
+    let title () = "untranspiling bad value" in
+    let content () = Format.asprintf "can not untranspile %s" bad_type in
+    let data = [
+      ("bad_type" , fun () -> bad_type) ;
+      ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
+    ] in
+    error ~data title content
+
+  let unknown_untranspile unknown_type value =
+    let title () = "untranspiling unknown value" in
+    let content () = Format.asprintf "can not untranspile %s" unknown_type in
+    let data = [
+      ("unknown_type" , fun () -> unknown_type) ;
+      ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
+    ] in
+    error ~data title content
 end
 open Errors
 
@@ -67,6 +118,9 @@ let rec transpile_type (t:AST.type_value) : type_value result =
   | T_constant ("map", [key;value]) ->
       let%bind kv' = bind_map_pair transpile_type (key, value) in
       ok (T_map kv')
+  | T_constant ("big_map", [key;value] ) ->
+      let%bind kv' = bind_map_pair transpile_type (key, value) in
+      ok (T_big_map kv')
   | T_constant ("list", [t]) ->
       let%bind t' = transpile_type t in
       ok (T_list t')
@@ -362,7 +416,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
   | E_list lst -> (
       let%bind t =
         trace_strong (corner_case ~loc:__LOC__ "not a list") @@
-        Mini_c.Combinators.get_t_list tv in
+        get_t_list tv in
       let%bind lst' = bind_map_list (transpile_annotated_expression) lst in
       let aux : expression -> expression -> expression result = fun prev cur ->
         return @@ E_constant ("CONS", [cur ; prev]) in
@@ -372,7 +426,7 @@ and transpile_annotated_expression (ae:AST.annotated_expression) : expression re
   | E_set lst -> (
       let%bind t =
         trace_strong (corner_case ~loc:__LOC__ "not a set") @@
-        Mini_c.Combinators.get_t_set tv in
+        get_t_set tv in
       let%bind lst' = bind_map_list (transpile_annotated_expression) lst in
       let aux : expression -> expression -> expression result = fun prev cur ->
         return @@ E_constant ("SET_ADD", [cur ; prev]) in
@@ -393,6 +447,20 @@ and transpile_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 (transpile_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'])
@@ -566,3 +634,63 @@ let transpile_program (lst : AST.program) : program result =
   in
   let%bind (statements, _) = List.fold_left aux (ok ([], Environment.empty)) (temp_unwrap_loc_list lst) in
   ok statements
+
+(* check whether the storage contains a big_map, if yes, check that
+  it appears on the left hand side of a pair *)
+let check_storage f ty loc : (anon_function * _) result =
+  let rec aux (t:type_value) on_big_map =
+    match t with
+      | T_big_map _ -> on_big_map
+      | T_pair (a , b) -> (aux a true) && (aux b false)
+      | T_or (a,b) -> (aux a false) && (aux b false)
+      | T_function (a,b) -> (aux a false) && (aux b false)
+      | T_deep_closure (_,a,b) -> (aux a false) && (aux b false)
+      | T_map (a,b) -> (aux a false) && (aux b false)
+      | T_list a -> (aux a false)
+      | T_set a -> (aux a false)
+      | T_contract a -> (aux a false)
+      | T_option a -> (aux a false)
+      | _ -> true
+  in
+  match f.body.type_value with
+    | T_pair (_, storage) ->
+      if aux storage false then ok (f, ty) else fail @@ bad_big_map loc
+    | _ -> ok (f, ty)
+
+let extract_constructor (v : value) (tree : _ Append_tree.t') : (string * value * AST.type_value) result =
+  let open Append_tree in
+  let rec aux tv : (string * value * AST.type_value) result=
+    match tv with
+    | Leaf (k, t), v -> ok (k, v, t)
+    | Node {a}, D_left v -> aux (a, v)
+    | Node {b}, D_right v -> aux (b, v)
+    | _ -> fail @@ internal_assertion_failure "bad constructor path"
+  in
+  let%bind (s, v, t) = aux (tree, v) in
+  ok (s, v, t)
+
+let extract_tuple (v : value) (tree : AST.type_value Append_tree.t') : ((value * AST.type_value) list) result =
+  let open Append_tree in
+  let rec aux tv : ((value * AST.type_value) list) result =
+    match tv with
+    | Leaf t, v -> ok @@ [v, t]
+    | Node {a;b}, D_pair (va, vb) ->
+        let%bind a' = aux (a, va) in
+        let%bind b' = aux (b, vb) in
+        ok (a' @ b')
+    | _ -> fail @@ internal_assertion_failure "bad tuple path"
+  in
+  aux (tree, v)
+
+let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result =
+  let open Append_tree in
+  let rec aux tv : ((string * (value * AST.type_value)) list) result =
+    match tv with
+    | Leaf (s, t), v -> ok @@ [s, (v, t)]
+    | Node {a;b}, D_pair (va, vb) ->
+        let%bind a' = aux (a, va) in
+        let%bind b' = aux (b, vb) in
+        ok (a' @ b')
+    | _ -> fail @@ internal_assertion_failure "bad record path"
+  in
+  aux (tree, v)
diff --git a/src/passes/6-transpiler/untranspiler.ml b/src/passes/6-transpiler/untranspiler.ml
index d79e842b4..6c0309bd3 100644
--- a/src/passes/6-transpiler/untranspiler.ml
+++ b/src/passes/6-transpiler/untranspiler.ml
@@ -129,6 +129,18 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         bind_map_list aux lst in
       return (E_map lst')
     )
+  | T_constant ("big_map", [k_ty;v_ty]) -> (
+      let%bind lst =
+        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
+          let%bind v' = untranspile v v_ty in
+          ok (k', v') in
+        bind_map_list aux lst in
+      return (E_big_map lst')
+    )
   | T_constant ("list", [ty]) -> (
       let%bind lst =
         trace_strong (wrong_mini_c_value "list" v) @@
diff --git a/src/passes/8-compiler/compiler_program.ml b/src/passes/8-compiler/compiler_program.ml
index bf0193fe3..8d42c1d3d 100644
--- a/src/passes/8-compiler/compiler_program.ml
+++ b/src/passes/8-compiler/compiler_program.ml
@@ -32,7 +32,7 @@ let get_operator : 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
@@ -104,6 +104,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/passes/8-compiler/compiler_type.ml b/src/passes/8-compiler/compiler_type.ml
index 4596bd74d..b22a0d2ef 100644
--- a/src/passes/8-compiler/compiler_type.ml
+++ b/src/passes/8-compiler/compiler_type.ml
@@ -70,6 +70,7 @@ module Ty = struct
     | T_or _ -> fail (not_comparable "or")
     | T_pair _ -> fail (not_comparable "pair")
     | T_map _ -> fail (not_comparable "map")
+    | T_big_map _ -> fail (not_comparable "big_map")
     | T_list _ -> fail (not_comparable "list")
     | T_set _ -> fail (not_comparable "set")
     | T_option _ -> fail (not_comparable "option")
@@ -116,6 +117,10 @@ module Ty = struct
         let%bind (Ex_comparable_ty k') = comparable_type k in
         let%bind (Ex_ty v') = type_ v in
         ok @@ Ex_ty (map k' v')
+    | T_big_map (k, v) ->
+        let%bind (Ex_comparable_ty k') = comparable_type k in
+        let%bind (Ex_ty v') = type_ v in
+        ok @@ Ex_ty (big_map k' v')
     | T_list t ->
         let%bind (Ex_ty t') = type_ t in
         ok @@ Ex_ty (list t')
@@ -184,6 +189,9 @@ let rec type_ : type_value -> O.michelson result =
   | T_map kv ->
       let%bind (k', v') = bind_map_pair type_ kv in
       ok @@ O.prim ~children:[k';v'] O.T_map
+  | T_big_map kv ->
+      let%bind (k', v') = bind_map_pair type_ kv in
+      ok @@ O.prim ~children:[k';v'] O.T_big_map
   | T_list t ->
       let%bind t' = type_ t in
       ok @@ O.prim ~children:[t'] O.T_list
diff --git a/src/passes/8-compiler/uncompiler.ml b/src/passes/8-compiler/uncompiler.ml
index c0f8aa16b..2838298d3 100644
--- a/src/passes/8-compiler/uncompiler.ml
+++ b/src/passes/8-compiler/uncompiler.ml
@@ -6,19 +6,19 @@ open Protocol
 open Script_typed_ir
 open Script_ir_translator
 
-let rec translate_value (Ex_typed_value (ty, value)) : value result =
+let rec translate_value ?bm_opt (Ex_typed_value (ty, value)) : value result =
   match (ty, value) with
   | Pair_t ((a_ty, _, _), (b_ty, _, _), _), (a, b) -> (
-      let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in
-      let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in
+      let%bind a = translate_value ?bm_opt @@ Ex_typed_value(a_ty, a) in
+      let%bind b = translate_value ?bm_opt @@ Ex_typed_value(b_ty, b) in
       ok @@ D_pair(a, b)
     )
   | Union_t ((a_ty, _), _, _), L a -> (
-      let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in
+      let%bind a = translate_value ?bm_opt @@ Ex_typed_value(a_ty, a) in
       ok @@ D_left a
     )
   | Union_t (_, (b_ty, _), _), R b -> (
-      let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in
+      let%bind b = translate_value ?bm_opt @@ Ex_typed_value(b_ty, b) in
       ok @@ D_right b
     )
   | (Int_t _), n ->
@@ -71,6 +71,30 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
         bind_map_list aux lst
       in
       ok @@ D_map lst'
+  | (Big_map_t (k_cty, v_ty, _)), m ->
+      let k_ty = Script_ir_translator.ty_of_comparable_ty k_cty in
+      let lst =
+        let aux k v acc = (k, v) :: acc in
+        let lst = Script_ir_translator.map_fold aux m.diff [] in
+        List.rev lst in
+      let%bind original_big_map =
+        match bm_opt with
+        | Some (D_big_map l) -> ok @@ l
+        | _ -> ok []
+        (* | _ -> fail @@ simple_error "Do not have access to the original big_map" . When does this matter? *)
+      in
+      let%bind lst' =
+        let aux orig (k, v) =
+          let%bind k' = translate_value (Ex_typed_value (k_ty, k)) in
+          let orig_rem = List.remove_assoc k' orig in
+          match v with
+          | Some vadd ->
+            let%bind v' = translate_value (Ex_typed_value (v_ty, vadd)) in
+            if (List.mem_assoc k' orig) then ok @@ (k', v')::orig_rem
+            else ok @@ (k', v')::orig
+          | None -> ok orig_rem in
+        bind_fold_list aux original_big_map lst in
+      ok @@ D_big_map lst'
   | (List_t (ty, _)), lst ->
       let%bind lst' =
         let aux = fun t -> translate_value (Ex_typed_value (ty, t)) in
diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml
index 22c24151d..71a135f7c 100644
--- a/src/passes/operators/operators.ml
+++ b/src/passes/operators/operators.ml
@@ -235,35 +235,35 @@ 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 ()
 
@@ -290,39 +290,10 @@ module Typer = struct
     let%bind () = assert_eq_1 arg_3 res'' in
     ok @@ res'
 
-  let big_map_remove : typer = typer_2 "BIG_MAP_REMOVE" @@ fun k m ->
-    let%bind (src , _) = get_t_big_map m in
-    let%bind () = assert_type_value_eq (src , k) in
-    ok m
-
-  let big_map_add : typer = typer_3 "BIG_MAP_ADD" @@ fun k v m ->
-    let%bind (src, dst) = 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 big_map_update : typer = typer_3 "BIG_MAP_UPDATE" @@ fun k v m ->
-    let%bind (src, dst) = 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 big_map_mem : typer = typer_2 "BIG_MAP_MEM" @@ fun k m ->
-    let%bind (src, _dst) = get_t_big_map m in
-    let%bind () = assert_type_value_eq (src, k) in
-    ok @@ t_bool ()
-
-  let big_map_find : typer = typer_2 "BIG_MAP_FIND" @@ fun k m ->
-    let%bind (src, dst) = get_t_big_map m in
-    let%bind () = assert_type_value_eq (src, k) in
-    ok @@ dst
-
-
   let size = typer_1 "SIZE" @@ fun t ->
     let%bind () =
       Assert.assert_true @@
-      (is_t_map t || is_t_list t || is_t_string t || is_t_bytes t || is_t_set t || is_t_big_map 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 ->
@@ -341,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
 
@@ -592,7 +563,6 @@ module Typer = struct
       map_map ;
       map_fold ;
       map_iter ;
-      map_map ;
       set_empty ;
       set_mem ;
       set_add ;
@@ -671,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])) ;
@@ -685,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/stages/ast_simplified/PP.ml b/src/stages/ast_simplified/PP.ml
index 01fee164d..6ddef98c6 100644
--- a/src/stages/ast_simplified/PP.ml
+++ b/src/stages/ast_simplified/PP.ml
@@ -41,6 +41,7 @@ let rec expression ppf (e:expression) = match e.expression with
   | E_accessor (ae, p) -> fprintf ppf "%a.%a" expression ae access_path p
   | E_record m -> fprintf ppf "record[%a]" (smap_sep_d expression) m
   | E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_expression) m
+  | E_big_map m -> fprintf ppf "big_map[%a]" (list_sep_d assoc_expression) m
   | E_list lst -> fprintf ppf "list[%a]" (list_sep_d expression) lst
   | E_set lst -> fprintf ppf "set[%a]" (list_sep_d expression) lst
   | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" expression ds expression ind
diff --git a/src/stages/ast_simplified/combinators.ml b/src/stages/ast_simplified/combinators.ml
index a25a08543..6260229ad 100644
--- a/src/stages/ast_simplified/combinators.ml
+++ b/src/stages/ast_simplified/combinators.ml
@@ -43,6 +43,7 @@ let ez_t_sum (lst:(string * type_expression) list) : type_expression =
 
 let t_function param result : type_expression = T_function (param, result)
 let t_map key value = (T_constant ("map", [key ; value]))
+let t_big_map key value = (T_constant ("big_map", [key ; value]))
 let t_set key = (T_constant ("set", [key]))
 
 let make_name (s : string) : name = s
@@ -67,6 +68,7 @@ let e'_bytes b : expression' result =
 let e_bytes ?loc b : expression result =
   let%bind e' = e'_bytes b in
   ok @@ location_wrap ?loc e'
+let e_big_map ?loc lst : expression = location_wrap ?loc @@ E_big_map lst
 let e_record ?loc map : expression = location_wrap ?loc @@ E_record map
 let e_tuple ?loc lst : expression = location_wrap ?loc @@ E_tuple lst
 let e_some ?loc s : expression = location_wrap ?loc @@ E_constant ("SOME", [s])
@@ -113,6 +115,7 @@ let e_typed_list ?loc lst t =
   e_annotation ?loc (e_list lst) (t_list t)
 
 let e_typed_map ?loc lst k v = e_annotation ?loc (e_map lst) (t_map k v)
+let e_typed_big_map ?loc lst k v = e_annotation ?loc (e_big_map lst) (t_big_map k v)
 
 let e_typed_set ?loc lst k = e_annotation ?loc (e_set lst) (t_set k)
 
diff --git a/src/stages/ast_simplified/misc.ml b/src/stages/ast_simplified/misc.ml
index 7e0dc76ab..9484b1f09 100644
--- a/src/stages/ast_simplified/misc.ml
+++ b/src/stages/ast_simplified/misc.ml
@@ -120,7 +120,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
   | E_record _, _ ->
       simple_fail "comparing record with other stuff"
 
-  | E_map lsta, E_map lstb -> (
+  | (E_map lsta, E_map lstb | E_big_map lsta, E_big_map lstb) -> (
       let%bind lst = generic_try (simple_error "maps of different lengths")
           (fun () ->
              let lsta' = List.sort compare lsta in
@@ -133,7 +133,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
       let%bind _all = bind_map_list aux lst in
       ok ()
     )
-  | E_map _, _ ->
+  | (E_map _ | E_big_map _), _ ->
       simple_fail "comparing map with other stuff"
 
   | E_list lsta, E_list lstb -> (
diff --git a/src/stages/ast_simplified/types.ml b/src/stages/ast_simplified/types.ml
index 1e92cfc67..1ca2a19cf 100644
--- a/src/stages/ast_simplified/types.ml
+++ b/src/stages/ast_simplified/types.ml
@@ -59,6 +59,7 @@ and expression' =
   | E_accessor of (expr * access_path)
   (* Data Structures *)
   | E_map of (expr * expr) list
+  | E_big_map of (expr * expr) list
   | E_list of expr list
   | E_set of expr list
   | E_look_up of (expr * expr)
diff --git a/src/stages/ast_typed/PP.ml b/src/stages/ast_typed/PP.ml
index 36298bbf6..9af3eb49a 100644
--- a/src/stages/ast_typed/PP.ml
+++ b/src/stages/ast_typed/PP.ml
@@ -41,6 +41,7 @@ and expression ppf (e:expression) : unit =
   | E_tuple lst -> fprintf ppf "tuple[@;  @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst
   | E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
   | E_map m -> fprintf ppf "map[@;  @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
+  | E_big_map m -> fprintf ppf "big_map[@;  @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
   | E_list m -> fprintf ppf "list[@;  @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) m
   | E_set m -> fprintf ppf "set[@;  @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) m
   | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
diff --git a/src/stages/ast_typed/combinators.ml b/src/stages/ast_typed/combinators.ml
index f0ae6f648..1f4047d5b 100644
--- a/src/stages/ast_typed/combinators.ml
+++ b/src/stages/ast_typed/combinators.ml
@@ -41,6 +41,7 @@ let ez_t_record lst ?s () : type_value =
   t_record m ?s ()
 
 let t_map key value ?s () = make_t (T_constant ("map", [key ; value])) s
+let t_big_map key value ?s () = make_t (T_constant ("big_map", [key ; value])) s
 
 let t_sum m ?s () : type_value = make_t (T_sum m) s
 let make_t_ez_sum (lst:(string * type_value) list) : type_value =
@@ -163,6 +164,14 @@ 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 ()
diff --git a/src/stages/ast_typed/misc.ml b/src/stages/ast_typed/misc.ml
index 3f99790fd..39b437060 100644
--- a/src/stages/ast_typed/misc.ml
+++ b/src/stages/ast_typed/misc.ml
@@ -173,7 +173,7 @@ module Free_variables = struct
     | E_tuple_accessor (a, _) -> self a
     | E_list lst -> unions @@ List.map self lst
     | E_set lst -> unions @@ List.map self lst
-    | E_map m -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
+    | (E_map m | E_big_map m) -> unions @@ List.map self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m
     | E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
     | E_matching (a , cs) -> union (self a) (matching_expression b cs)
     | E_failwith a -> self a
@@ -439,7 +439,7 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
   | E_record _, _ ->
       fail @@ (different_values_because_different_types "record vs. non-record" a b)
 
-  | E_map lsta, E_map lstb -> (
+  | (E_map lsta, E_map lstb | E_big_map lsta, E_big_map lstb) -> (
       let%bind lst = generic_try (different_size_values "maps of different lengths" a b)
           (fun () ->
              let lsta' = List.sort compare lsta in
@@ -452,7 +452,7 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
       let%bind _all = bind_map_list aux lst in
       ok ()
     )
-  | E_map _, _ ->
+  | (E_map _ | E_big_map _), _ ->
       fail @@ different_values_because_different_types "map vs. non-map" a b
 
   | E_list lsta, E_list lstb -> (
diff --git a/src/stages/ast_typed/misc_smart.ml b/src/stages/ast_typed/misc_smart.ml
index dc74d35b2..10e52d2e6 100644
--- a/src/stages/ast_typed/misc_smart.ml
+++ b/src/stages/ast_typed/misc_smart.ml
@@ -78,7 +78,7 @@ module Captured_variables = struct
     | E_set lst ->
       let%bind lst' = bind_map_list self lst in
       ok @@ unions lst'
-    | E_map m ->
+    | (E_map m | E_big_map m) ->
       let%bind lst' = bind_map_list self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m in
       ok @@ unions lst'
     | E_look_up (a , b) ->
diff --git a/src/stages/ast_typed/types.ml b/src/stages/ast_typed/types.ml
index 06a63e975..ce5627086 100644
--- a/src/stages/ast_typed/types.ml
+++ b/src/stages/ast_typed/types.ml
@@ -99,6 +99,7 @@ and expression =
   | E_record_accessor of (ae * string)
   (* Data Structures *)
   | E_map of (ae * ae) list
+  | E_big_map of (ae * ae) list
   | E_list of ae list
   | E_set of ae list
   | E_look_up of (ae * ae)
diff --git a/src/stages/mini_c/PP.ml b/src/stages/mini_c/PP.ml
index 52d87a887..f3863dca6 100644
--- a/src/stages/mini_c/PP.ml
+++ b/src/stages/mini_c/PP.ml
@@ -27,6 +27,7 @@ let rec type_ ppf : type_value -> _ = function
   | T_base b -> type_base ppf b
   | T_function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b
   | T_map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v
+  | T_big_map(k, v) -> fprintf ppf "big_map(%a -> %a)" type_ k type_ v
   | T_list(t) -> fprintf ppf "list(%a)" type_ t
   | T_set(t) -> fprintf ppf "set(%a)" type_ t
   | T_option(o) -> fprintf ppf "option(%a)" type_ o
@@ -61,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/stages/mini_c/combinators.ml b/src/stages/mini_c/combinators.ml
index f19536e8f..074d66618 100644
--- a/src/stages/mini_c/combinators.ml
+++ b/src/stages/mini_c/combinators.ml
@@ -59,6 +59,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"
@@ -105,6 +109,10 @@ let get_t_map (t:type_value) = match t with
   | T_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/stages/mini_c/misc.ml b/src/stages/mini_c/misc.ml
index 21e049e38..60810643c 100644
--- a/src/stages/mini_c/misc.ml
+++ b/src/stages/mini_c/misc.ml
@@ -106,3 +106,61 @@ let aggregate_entry (lst : program) (name : string) (to_functionalize : bool) :
       Format.printf "Not functional: %a\n" PP.expression entry_expression ;
       fail @@ Errors.not_functional_main name
   )
+
+let rec expression_to_value (exp: expression) : value result =
+  match exp.content with
+    | E_literal v -> ok @@ v
+    | E_constant ("map" , lst) ->
+      let aux el =
+        let%bind l = expression_to_value el in
+        match l with
+          | D_pair (a , b) -> ok @@ (a , b)
+          | _ -> fail @@ simple_error "??" in
+      let%bind lstl = bind_map_list aux lst in
+      ok @@ D_map lstl
+    | E_constant ("big_map" , lst) ->
+      let aux el =
+        let%bind l = expression_to_value el in
+        match l with
+          | D_pair (a , b) -> ok @@ (a , b)
+          | _ -> fail @@ simple_error "??" in
+      let%bind lstl = bind_map_list aux lst in
+      ok @@ D_big_map lstl
+    | E_constant ("PAIR" , fst::snd::[]) ->
+      let%bind fstl = expression_to_value fst in
+      let%bind sndl = expression_to_value snd in
+      ok @@ D_pair (fstl , sndl)
+    | E_constant ("UNIT", _) -> ok @@ D_unit
+    | E_constant ("UPDATE", _) ->
+      let rec handle_prev upd =
+        match upd.content with
+        | E_constant ("UPDATE" , [k;v;prev]) ->
+          begin
+            match v.content with
+              | E_constant ("SOME" , [i]) ->
+                let%bind kl = expression_to_value k in
+                let%bind il  = expression_to_value i in
+                let%bind prevl = handle_prev prev in
+                ok @@ (kl,il)::prevl
+              | E_constant ("NONE" , []) ->
+                let%bind prevl = handle_prev prev in
+                ok @@ prevl
+              | _ -> failwith "UPDATE second parameter is not an option"
+          end
+        | E_make_empty_map _ ->
+          ok @@ []
+        | _ -> failwith "Ill-constructed map"
+      in
+      begin
+      match exp.type_value with
+        | T_big_map _ ->
+          let%bind kvl = handle_prev exp in
+          ok @@ D_big_map kvl
+        | T_map _ ->
+          let%bind kvl = handle_prev exp in
+          ok @@ D_map kvl
+        | _ -> failwith "UPDATE with a non-map type_value"
+      end
+    | _ as nl ->
+      let expp = Format.asprintf "'%a'" PP.expression' nl in
+      fail @@ simple_error ("Can not convert expression "^expp^" to literal")
diff --git a/src/stages/mini_c/types.ml b/src/stages/mini_c/types.ml
index bbffddbc6..f7fdb0d05 100644
--- a/src/stages/mini_c/types.ml
+++ b/src/stages/mini_c/types.ml
@@ -15,6 +15,7 @@ type type_value =
   | T_deep_closure of (environment * type_value * type_value)
   | T_base of type_base
   | T_map of (type_value * type_value)
+  | T_big_map of (type_value * type_value)
   | T_list of type_value
   | T_set of type_value
   | T_contract of type_value
@@ -47,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/test/contracts/big_map.ligo b/src/test/contracts/big_map.ligo
new file mode 100644
index 000000000..461c2c206
--- /dev/null
+++ b/src/test/contracts/big_map.ligo
@@ -0,0 +1,60 @@
+type storage_ is big_map(int, int) * unit
+
+function main(const p : unit; const s : storage_) : list(operation) * storage_ is
+  var r : big_map(int, int) := s.0 ;
+  var toto : option (int) := Some(0);
+  block {
+    toto := r[23];
+    r[2] := 444;
+    s.0 := r;
+  }
+  with ((nil: list(operation)), s)
+
+function set_ (var n : int ; var m : storage_) : storage_ is block {
+  var tmp : big_map(int,int) := m.0 ;
+  tmp[23] := n ;
+  m.0 := tmp ;
+} with m
+
+function rm (var m : storage_) : storage_ is block {
+  var tmp : big_map(int,int) := m.0 ;
+  remove 42 from map tmp;
+  m.0 := tmp;
+} with m
+
+function gf (const m : storage_) : int is begin skip end with get_force(23, m.0)
+
+function get (const m : storage_) : option(int) is
+  begin
+    skip
+  end with m.0[42]
+
+// the following is not supported (negative test cases):
+
+// const bm : storage_ = big_map
+//   144 -> 23 ;
+//   51 -> 23 ;
+//   42 -> 23 ;
+//   120 -> 23 ;
+//   421 -> 23 ;
+// end
+
+// type foobar is big_map(int, int)
+// const fb : foobar = big_map
+//   23 -> 0 ;
+//   42 -> 0 ;
+// end
+
+// function size_ (const m : storage_) : nat is
+//   block {skip} with (size(m.0))
+
+// function iter_op (const m : storage_) : int is
+//   var r : int := 0 ;
+//   function aggregate (const i : int ; const j : int) : unit is block { r := r + i + j } with unit ;
+//   block {
+//     map_iter(m.0 , aggregate) ;
+//   } with r ;
+
+// function map_op (const m : storage_) : storage_ is
+//   function increment (const i : int ; const j : int) : int is block { skip } with j + 1 ;
+//   block { skip } with map_map(m.0 , increment) ;
diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml
index 9215b5a5c..639310afc 100644
--- a/src/test/integration_tests.ml
+++ b/src/test/integration_tests.ml
@@ -407,6 +407,38 @@ let map () : unit result =
   in
   ok ()
 
+let big_map () : unit result =
+  let%bind program = type_file "./contracts/big_map.ligo" in
+  let ez lst =
+    let open Ast_simplified.Combinators in
+    let lst' = List.map (fun (x, y) -> e_int x, e_int y) lst in
+    e_pair (e_typed_big_map lst' t_int t_int) (e_unit ())
+  in
+  let%bind () =
+    let make_input = fun n -> ez [(23, n) ; (42, 4)] in
+    let make_expected = e_int in
+    expect_eq_n ~input_to_value:true program "gf" make_input make_expected
+  in
+  let%bind () =
+    let make_input = fun n ->
+      let m = ez [(23 , 0) ; (42 , 0)] in
+      e_tuple [(e_int n) ; m]
+    in
+    let make_expected = fun n -> ez [(23 , n) ; (42 , 0)] in
+    expect_eq_n_pos_small ?input_to_value:(Some true) program "set_" make_input make_expected
+  in
+  let%bind () =
+    let make_input = fun n -> ez [(23, n) ; (42, 4)] in
+    let make_expected = fun _ -> e_some @@ e_int 4 in
+    expect_eq_n ?input_to_value:(Some true) program "get" make_input make_expected
+  in
+  let%bind () =
+    let input = ez [(23, 23) ; (42, 42)] in
+    let expected = ez [23, 23] in
+    expect_eq ?input_to_value:(Some true) program "rm" input expected
+  in
+  ok ()
+
 let list () : unit result =
   let%bind program = type_file "./contracts/list.ligo" in
   let ez lst =
@@ -720,6 +752,7 @@ let main = test_suite "Integration (End to End)" [
     test "option" option ;
     test "option (mligo)" moption ;
     test "map" map ;
+    test "big_map" big_map ;
     test "list" list ;
     test "loop" loop ;
     test "matching" matching ;
diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml
index 96b5522cb..9eee8adc0 100644
--- a/src/test/test_helpers.ml
+++ b/src/test/test_helpers.ml
@@ -31,14 +31,14 @@ let test_suite name lst = Test_suite (name , lst)
 
 open Ast_simplified.Combinators
 
-let expect ?options program entry_point input expecter =
+let expect ?input_to_value ?options program entry_point input expecter =
   let%bind result =
     let run_error =
       let title () = "expect run" in
       let content () = Format.asprintf "Entry_point: %s" entry_point in
       error title content in
     trace run_error @@
-    Ligo.Run.Of_simplified.run_typed_program ?options program entry_point input in
+    Ligo.Run.Of_simplified.run_typed_program ?input_to_value ?options program entry_point input in
   expecter result
 
 let expect_fail ?options program entry_point input =
@@ -52,7 +52,7 @@ let expect_fail ?options program entry_point input =
   @@ Ligo.Run.Of_simplified.run_typed_program ?options program entry_point input
 
 
-let expect_eq ?options program entry_point input expected =
+let expect_eq ?input_to_value ?options program entry_point input expected =
   let expecter = fun result ->
     let expect_error =
       let title () = "expect result" in
@@ -62,7 +62,7 @@ let expect_eq ?options program entry_point input expected =
       error title content in
     trace expect_error @@
     Ast_simplified.Misc.assert_value_eq (expected , result) in
-  expect ?options program entry_point input expecter
+  expect ?input_to_value ?options program entry_point input expecter
 
 let expect_evaluate program entry_point expecter =
   let error =
@@ -89,23 +89,23 @@ let expect_n_aux ?options lst program entry_point make_input make_expecter =
   let%bind _ = bind_map_list aux lst in
   ok ()
 
-let expect_eq_n_aux ?options lst program entry_point make_input make_expected =
+let expect_eq_n_aux ?input_to_value ?options lst program entry_point make_input make_expected =
   let aux n =
     let input = make_input n in
     let expected = make_expected n in
     trace (simple_error ("expect_eq_n " ^ (string_of_int n))) @@
-    let result = expect_eq ?options program entry_point input expected in
+    let result = expect_eq ?input_to_value ?options program entry_point input expected in
     result
   in
   let%bind _ = bind_map_list_seq aux lst in
   ok ()
 
-let expect_eq_n ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163 ; -1]
-let expect_eq_n_pos ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163]
-let expect_eq_n_strict_pos ?options = expect_eq_n_aux ?options [2 ; 42 ; 163]
-let expect_eq_n_pos_small ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 10]
-let expect_eq_n_strict_pos_small ?options = expect_eq_n_aux ?options [1 ; 2 ; 10]
-let expect_eq_n_pos_mid = expect_eq_n_aux [0 ; 1 ; 2 ; 10 ; 33]
+let expect_eq_n ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [0 ; 1 ; 2 ; 42 ; 163 ; -1]
+let expect_eq_n_pos ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [0 ; 1 ; 2 ; 42 ; 163]
+let expect_eq_n_strict_pos ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [2 ; 42 ; 163]
+let expect_eq_n_pos_small ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [0 ; 1 ; 2 ; 10]
+let expect_eq_n_strict_pos_small ?input_to_value ?options = expect_eq_n_aux ?input_to_value ?options [1 ; 2 ; 10]
+let expect_eq_n_pos_mid ?input_to_value = expect_eq_n_aux ?input_to_value [0 ; 1 ; 2 ; 10 ; 33]
 
 let expect_n_pos_small ?options = expect_n_aux ?options [0 ; 2 ; 10]
 let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]
diff --git a/vendors/ligo-utils/simple-utils/trace.ml b/vendors/ligo-utils/simple-utils/trace.ml
index 52637021e..329203a46 100644
--- a/vendors/ligo-utils/simple-utils/trace.ml
+++ b/vendors/ligo-utils/simple-utils/trace.ml
@@ -639,6 +639,8 @@ let bind_or (a, b) =
   match a with
   | Ok _ as o -> o
   | _ -> b
+let bind_map_or (fa , fb) c =
+  bind_or (fa c , fb c)
 
 let bind_lr (type a b) ((a : a result), (b:b result)) : [`Left of a | `Right of b] result =
   match (a, b) with