diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml
index 65d954428..46091ce4a 100644
--- a/src/ligo/ast_simplified.ml
+++ b/src/ligo/ast_simplified.ml
@@ -63,6 +63,8 @@ and expression =
   (* Record *)
   | Record of ae_map
   | Accessor of ae * access_path
+  (* Data Structures *)
+  | Map of (ae * ae) list
 
 and access =
   | Tuple_access of int
@@ -137,11 +139,15 @@ module PP = struct
     | Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
     | Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
     | Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
+    | Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
     | Lambda {binder;input_type;output_type;result;body} ->
         fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
           binder type_expression input_type type_expression output_type
           block body annotated_expression result
 
+  and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
+    fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
+
   and access ppf (a:access) =
     match a with
     | Tuple_access n -> fprintf ppf "%d" n
@@ -300,6 +306,10 @@ module Rename = struct
           let%bind sm' = bind_smap
             @@ SMap.map (rename_annotated_expression r) sm in
           ok (Record sm')
+      | Map m ->
+          let%bind m' = bind_map_list
+            (fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
+          ok (Map m')
   end
 end
 
diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml
index b0031c72f..3d1fb0f04 100644
--- a/src/ligo/ast_typed.ml
+++ b/src/ligo/ast_typed.ml
@@ -64,8 +64,10 @@ and expression =
   (* Record *)
   | Record of ae_map
   | Record_accessor of ae * string
+  (* Data Structures *)
+  | Map of (ae * ae) list
 
-and value = annotated_expression (* BAD *)
+and value = annotated_expression (* todo (for refactoring) *)
 
 and literal =
   | Unit
@@ -105,6 +107,7 @@ open! Ligo_helpers.Trace
 
 let type_value type_value simplified = { type_value ; simplified }
 let annotated_expression expression type_annotation = { expression ; type_annotation }
+let get_type_annotation x = x.type_annotation
 
 let get_entry (p:program) (entry : string) : annotated_expression result =
   let aux (d:declaration) =
@@ -159,6 +162,10 @@ module PP = struct
     | Tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
     | Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
     | Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
+    | Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
+
+  and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
+    fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
 
   and literal ppf (l:literal) : unit =
     match l with
@@ -415,6 +422,9 @@ module Combinators = struct
     let m = SMap.of_list lst in
     make_t_record m
 
+  let t_map key value s = type_value (Type_constant ("map", [key ; value])) s
+  let make_t_map key value = t_map key value None
+
   let t_sum m s : type_value = type_value (Type_sum m) s
   let make_t_sum m = t_sum m None
   let make_t_ez_sum (lst:(string * type_value) list) : type_value =
@@ -452,12 +462,13 @@ module Combinators = struct
     | _ -> simple_fail "not a record"
 
   let record map : expression = Record map
-
   let record_ez (lst : (string * ae) list) : expression =
     let aux prev (k, v) = SMap.add k v prev in
     let map = List.fold_left aux SMap.empty lst in
     record map
 
+  let map lst : expression = Map lst
+
   let unit : expression = Literal (Unit)
   let int n : expression = Literal (Int n)
   let bool b : expression = Literal (Bool b)
@@ -469,6 +480,7 @@ module Combinators = struct
   let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
   let a_record r = annotated_expression (record r) (make_t_record (SMap.map (fun x -> x.type_annotation) r))
   let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
+  let a_map lst k v = annotated_expression (map lst) (make_t_map k v)
 
   let get_a_int (t:annotated_expression) =
     match t.expression with
diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo
index c9a879b3d..dd9a583af 100644
--- a/src/ligo/contracts/heap.ligo
+++ b/src/ligo/contracts/heap.ligo
@@ -1,4 +1,8 @@
+
 type heap is record
   heap_content : map(int, heap_element) ;
   heap_size : nat ;
 end
+
+function is_empty (const h : heap) : bool is
+  block {skip} with h.heap_size = 0
diff --git a/src/ligo/ligo-helpers/trace.ml b/src/ligo/ligo-helpers/trace.ml
index c6478808c..6d2ffb7a9 100644
--- a/src/ligo/ligo-helpers/trace.ml
+++ b/src/ligo/ligo-helpers/trace.ml
@@ -114,6 +114,10 @@ let bind_and (a, b) =
   b >>? fun b ->
   ok (a, b)
 
+let bind_pair = bind_and
+let bind_map_pair f (a, b) =
+  bind_pair (f a, f b)
+
 module AE = Tezos_utils.Memory_proto_alpha.Alpha_environment
 module TP = Tezos_base__TzPervasives
 
diff --git a/src/ligo/meta-michelson/contract.ml b/src/ligo/meta-michelson/contract.ml
index d5ce41d4c..7f6a6791c 100644
--- a/src/ligo/meta-michelson/contract.ml
+++ b/src/ligo/meta-michelson/contract.ml
@@ -247,6 +247,7 @@ module Types = struct
   let nat = Nat_t None
   let int = Int_t None
   let nat_k = Nat_key None
+  let int_k = Int_key None
 
   let big_map k v = Big_map_t (k, v, None)
 
diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml
index 9b874cb32..813fd106a 100644
--- a/src/ligo/mini_c.ml
+++ b/src/ligo/mini_c.ml
@@ -15,7 +15,7 @@ type type_name = string
 type type_base =
   | Unit
   | Bool
-  | Int | Nat | Float
+  | Int | Nat
   | String | Bytes
 
 type type_value = [
@@ -25,6 +25,7 @@ type type_value = [
   | `Deep_closure of environment_small * type_value * type_value
   | `Shallow_closure of environment * type_value * type_value
   | `Base of type_base
+  | `Map of type_value * type_value
 ]
 
 and environment_element = string * type_value
@@ -114,7 +115,6 @@ module PP = struct
     | Unit -> fprintf ppf "unit"
     | Bool -> fprintf ppf "bool"
     | Int -> fprintf ppf "int"
-    | Float -> fprintf ppf "float"
     | Nat -> fprintf ppf "nat"
     | String -> fprintf ppf "string"
     | Bytes -> fprintf ppf "bytes"
@@ -124,6 +124,7 @@ module PP = struct
     | `Pair(a, b) -> fprintf ppf "(%a) & (%a)" type_ a type_ b
     | `Base b -> type_base ppf b
     | `Function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b
+    | `Map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v
     | `Shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b
     | `Deep_closure(c, arg, ret) ->
       fprintf ppf "[%a](%a)->(%a)"
@@ -232,12 +233,40 @@ module Translate_type = struct
 
   module Ty = struct
 
-    let base_type : type_base -> ex_ty result =
-      function
-      | Unit -> ok @@ Ex_ty Types.unit
-      | Bool -> ok @@ Ex_ty Types.bool
-      | Int -> ok @@ Ex_ty Types.int
-      | _ -> simple_fail "all based types not supported yet"
+    let not_comparable name = error "not a comparable type" name
+
+    let comparable_type_base : type_base -> ex_comparable_ty result = fun tb ->
+      let open Types in
+      let return x = ok @@ Ex_comparable_ty x in
+      match tb with
+      | Unit -> fail (not_comparable "unit")
+      | Bool -> fail (not_comparable "bool")
+      | Nat -> return nat_k
+      | Int -> return int_k
+      | String -> return string_k
+      | Bytes -> return bytes_k
+
+    let comparable_type : type_value -> ex_comparable_ty result = fun tv ->
+      match tv with
+      | `Base b -> comparable_type_base b
+      | `Deep_closure _ -> fail (not_comparable "deep closure")
+      | `Shallow_closure _ -> fail (not_comparable "shallow closure")
+      | `Function _ -> fail (not_comparable "function closure")
+      | `Or _ -> fail (not_comparable "or closure")
+      | `Pair _ -> fail (not_comparable "pair closure")
+      | `Map _ -> fail (not_comparable "map closure")
+
+    let base_type : type_base -> ex_ty result = fun b ->
+      let open Types in
+      let return x = ok @@ Ex_ty x in
+      match b with
+      | Unit -> return unit
+      | Bool -> return bool
+      | Int -> return int
+      | Nat -> return nat
+      | String -> return string
+      | Bytes -> return bytes
+
 
     let rec type_ : type_value -> ex_ty result =
       function
@@ -266,6 +295,10 @@ module Translate_type = struct
           let%bind (Ex_ty arg) = type_ arg in
           let%bind (Ex_ty ret) = type_ ret in
           ok @@ Ex_ty Types.(pair capture @@ lambda (pair capture arg) ret)
+      | `Map (k, v) ->
+          let%bind (Ex_comparable_ty k') = comparable_type k in
+          let%bind (Ex_ty v') = type_ v in
+          ok @@ Ex_ty Types.(map k' v')
 
 
     and environment_small' = let open Append_tree in function
@@ -294,7 +327,9 @@ module Translate_type = struct
     | Unit -> ok @@ prim T_unit
     | Bool -> ok @@ prim T_bool
     | Int -> ok @@ prim T_int
-    | _ -> simple_fail "all based types not supported yet"
+    | Nat -> ok @@ prim T_nat
+    | String -> ok @@ prim T_string
+    | Bytes -> ok @@ prim T_bytes
 
   let rec type_ : type_value -> michelson result =
     function
@@ -309,6 +344,9 @@ module Translate_type = struct
         type_ t' >>? fun t' ->
         ok @@ prim ~children:[t;t'] T_or
       )
+    | `Map kv ->
+        let%bind (k', v') = bind_map_pair type_ kv in
+        ok @@ prim ~children:[k';v'] T_map
     | `Function (arg, ret) ->
       let%bind arg = type_ arg in
       let%bind ret = type_ ret in
@@ -1037,6 +1075,10 @@ module Combinators = struct
     | `Pair (a, b) -> ok (a, b)
     | _ -> simple_fail "not a type pair"
 
+  let get_t_map (t:type_value) = match t with
+    | `Map kv -> ok kv
+    | _ -> simple_fail "not a type map"
+
   let get_left (v:value) = match v with
     | `Left b -> ok b
     | _ -> simple_fail "not a left"
diff --git a/src/ligo/test/heap_tests.ml b/src/ligo/test/heap_tests.ml
new file mode 100644
index 000000000..6bab7235c
--- /dev/null
+++ b/src/ligo/test/heap_tests.ml
@@ -0,0 +1,199 @@
+open Ligo_helpers.Trace
+open Ligo
+open Test_helpers
+
+let get_program =
+  let s = ref None in
+  fun () -> match !s with
+    | Some s -> ok s
+    | None -> (
+        let%bind program = type_file "./contracts/heap.ligo" in
+        s := Some program ;
+        ok program
+      )
+
+let a_heap content size =
+  let open AST_Typed.Combinators in
+  a_record_ez [
+    ("content", content) ;
+    ("size", size) ;
+  ]
+
+let a_heap_ez ?value_type (content:(int * AST_Typed.ae) list) =
+  let open AST_Typed.Combinators in
+  let content =
+    let aux = fun (x, y) -> a_int x, y in
+    List.map aux content in
+  let value_type = match value_type, content with
+    | None, hd :: _ -> (snd hd).type_annotation
+    | Some s, _ -> s
+    | _ -> raise (Failure "no value type and heap empty when building heap") in
+  a_map content make_t_int value_type
+
+let is_empty () : unit result =
+  let%bind program = get_program () in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = a_int n in
+    let%bind result = easy_run_main_typed program input in
+    let%bind result' =
+      trace (simple_error "bad result") @@
+      get_a_int result in
+    Assert.assert_equal_int (3 * n + 2) result'
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 42 ; 163 ; -1] in
+  ok ()
+
+let bool_expression () : unit result =
+  let%bind program = type_file "./contracts/boolean_operators.ligo" in
+  let aux (name, f) =
+    let aux b =
+      let open AST_Typed.Combinators in
+      let input = a_bool b in
+      let%bind result = easy_run_typed name program input in
+      let%bind result' =
+        trace (simple_error "bad result") @@
+        get_a_bool result in
+      Assert.assert_equal_bool (f b) result'
+    in
+    let%bind _ = bind_list
+      @@ List.map aux [true;false] in
+    ok ()
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [
+      ("or_true", fun b -> b || true) ;
+      ("or_false", fun b -> b || false) ;
+      ("and_true", fun b -> b && true) ;
+      ("and_false", fun b -> b && false) ;
+    ] in
+  ok ()
+
+let unit_expression () : unit result =
+  let%bind program = type_file "./contracts/unit.ligo" in
+  let open AST_Typed.Combinators in
+  let%bind result = easy_evaluate_typed "u" program in
+  let%bind () =
+    trace (simple_error "result isn't unit") @@
+    get_a_unit result in
+  ok ()
+
+let record_ez_int names n =
+  let open AST_Typed.Combinators in
+  a_record_ez @@ List.map (fun x -> x, a_int n) names
+
+let multiple_parameters () : unit result  =
+  let%bind program = type_file "./contracts/multiple-parameters.ligo" in
+  let inputs = [0 ; 2 ; 42 ; 163 ; -1] in
+  let aux (name, input_f, output_f) =
+    let aux n =
+      let input = input_f n in
+      let%bind result = easy_run_typed name program input in
+      let%bind result' = AST_Typed.Combinators.get_a_int result in
+      let expected = output_f n in
+      let%bind _ = Assert.assert_equal_int expected result' in
+      ok ()
+    in
+    let%bind _ = bind_list @@ List.map aux inputs in
+    ok ()
+  in
+  let%bind _ = bind_list @@ List.map aux [
+      ("ab", record_ez_int ["a";"b"], fun n -> 2 * n) ;
+      ("abcd", record_ez_int ["a";"b";"c";"d"], fun n -> 4 * n + 2) ;
+      ("abcde", record_ez_int ["a";"b";"c";"d";"e"], fun n -> 2 * n + 3) ;
+    ] in
+  ok ()
+
+let record () : unit result  =
+  let%bind program = type_file "./contracts/record.ligo" in
+  let%bind _foobar =
+    let%bind result = easy_evaluate_typed "fb" program in
+    let expect = record_ez_int ["foo";"bar"] 0 in
+    AST_Typed.assert_value_eq (expect, result)
+  in
+  let%bind _projection =
+    let aux n =
+      let input = record_ez_int ["foo";"bar"] n in
+      let%bind result = easy_run_typed "projection" program input in
+      let expect = AST_Typed.Combinators.a_int (2 * n) in
+      AST_Typed.assert_value_eq (expect, result)
+    in
+    bind_list @@ List.map aux [0 ; -42 ; 144]
+  in
+  let%bind _big =
+    let%bind result = easy_evaluate_typed "br" program in
+    let expect = record_ez_int ["a";"b";"c";"d";"e"] 23 in
+    AST_Typed.assert_value_eq (expect, result)
+  in
+  ok ()
+
+let condition () : unit result =
+  let%bind program = type_file "./contracts/condition.ligo" in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = a_int n in
+    let%bind result = easy_run_main_typed program input in
+    let%bind result' =
+      trace (simple_error "bad result") @@
+      get_a_int result in
+    Assert.assert_equal_int (if n = 2 then 42 else 0) result'
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 42 ; 163 ; -1] in
+  ok ()
+
+let declarations () : unit result =
+  let%bind program = type_file "./contracts/declarations.ligo" in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = a_int n in
+    let%bind result = easy_run_main_typed program input in
+    let%bind result' =
+      trace (simple_error "bad result") @@
+      get_a_int result in
+    Assert.assert_equal_int (42 + n) result'
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 42 ; 163 ; -1] in
+  ok ()
+
+let quote_declaration () : unit result =
+  let%bind program = type_file "./contracts/quote-declaration.ligo" in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = a_int n in
+    let%bind result = easy_run_main_typed program input in
+    let%bind result' =
+      trace (simple_error "bad result") @@
+      get_a_int result in
+    Assert.assert_equal_int result' (42 + 2 * n)
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 42 ; 163 ; -1] in
+  ok ()
+
+let quote_declarations () : unit result =
+  let%bind program = type_file "./contracts/quote-declarations.ligo" in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = a_int n in
+    let%bind result = easy_run_main_typed program input in
+    let%bind result' =
+      trace (simple_error "bad result") @@
+      get_a_int result in
+    Assert.assert_equal_int result' (74 + 2 * n)
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 42 ; 163 ; -1] in
+  ok ()
+
+let main = "Heap (End to End)", [
+    test "is_empty" is_empty ;
+  ]
diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml
index 67a965d81..17de7848b 100644
--- a/src/ligo/test/integration_tests.ml
+++ b/src/ligo/test/integration_tests.ml
@@ -189,7 +189,6 @@ let quote_declarations () : unit result =
     @@ [0 ; 2 ; 42 ; 163 ; -1] in
   ok ()
 
-
 let main = "Integration (End to End)", [
     test "basic" basic ;
     test "function" function_ ;
diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml
index 5fc47ddac..3d5ab340f 100644
--- a/src/ligo/test/test.ml
+++ b/src/ligo/test/test.ml
@@ -7,5 +7,6 @@ let () =
     Compiler_tests.main ;
     Transpiler_tests.main ;
     Typer_tests.main ;
+    Heap_tests.main ;
   ] ;
   ()
diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml
index 77e799f81..30ad7e2f8 100644
--- a/src/ligo/transpiler.ml
+++ b/src/ligo/transpiler.ml
@@ -84,6 +84,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
 
 and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
   let%bind tv = translate_type ae.type_annotation in
+  let return (expr, tv) = ok (expr, tv, env) in
   match ae.expression with
   | Literal (Bool b) -> ok (Literal (`Bool b), tv, env)
   | Literal (Int n) -> ok (Literal (`Int n), tv, env)
@@ -198,6 +199,15 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
       let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in
       ok (Predicate (name, lst'), tv, env)
   | Lambda l -> translate_lambda env l tv
+  | Map m ->
+      let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev kv ->
+        let%bind prev' = prev in
+        let%bind (k', v') = bind_map_pair (translate_annotated_expression env) kv in
+        return (Predicate ("UPDATE", [k' ; v' ; prev']), tv)
+      in
+      let init = return (Predicate ("EMPTY", []), tv) in
+      List.fold_left aux init m
+
 
 and translate_lambda_shallow env l tv =
   let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml
index aa7457e85..4833aaf07 100644
--- a/src/ligo/typer.ml
+++ b/src/ligo/typer.ml
@@ -317,6 +317,33 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
       let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
       let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in
       ok O.{expression = O.Record m' ; type_annotation }
+  (* Data-structure *)
+  | Map lst ->
+      let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in
+      let%bind type_annotation =
+        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 opt =
+            bind_fold_list aux None
+            @@ List.map Ast_typed.get_type_annotation
+            @@ List.map fst lst' in
+          trace_option (simple_error "empty map expression") opt
+        in
+        let%bind value_type =
+          let%bind opt =
+            bind_fold_list aux None
+            @@ List.map Ast_typed.get_type_annotation
+            @@ List.map snd lst' in
+          trace_option (simple_error "empty map expression") opt
+        in
+        check (make_t_map key_type value_type)
+      in
+      ok O.{expression = O.Map lst' ; type_annotation}
   | Lambda {
       binder ;
       input_type ;
@@ -420,6 +447,9 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
   | Record_accessor (r, s) ->
       let%bind r' = untype_annotated_expression r in
       return (Accessor (r', [Record_access s]))
+  | Map m ->
+      let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
+      return (Map m')
 
 and untype_block (b:O.block) : (I.block) result =
   bind_list @@ List.map untype_instruction b