diff --git a/gitlab-pages/website/static/.well-known/acme-challenge/pY4yiss3_bmzORHLtOPUEYaFxWxD_GkD8XZajWh0DUU b/gitlab-pages/website/static/.well-known/acme-challenge/pY4yiss3_bmzORHLtOPUEYaFxWxD_GkD8XZajWh0DUU
new file mode 100644
index 000000000..d17cdcfbe
--- /dev/null
+++ b/gitlab-pages/website/static/.well-known/acme-challenge/pY4yiss3_bmzORHLtOPUEYaFxWxD_GkD8XZajWh0DUU
@@ -0,0 +1 @@
+pY4yiss3_bmzORHLtOPUEYaFxWxD_GkD8XZajWh0DUU.4Dc00ftieGaWDmacztwSS7euFOKPULDHjUNzikwPvao
diff --git a/src/ast_simplified/PP.ml b/src/ast_simplified/PP.ml
index e136988d2..07277c664 100644
--- a/src/ast_simplified/PP.ml
+++ b/src/ast_simplified/PP.ml
@@ -24,6 +24,7 @@ let literal ppf (l:literal) = match l with
   | Literal_bool b -> fprintf ppf "%b" b
   | Literal_int n -> fprintf ppf "%d" n
   | Literal_nat n -> fprintf ppf "+%d" n
+  | Literal_timestamp n -> fprintf ppf "+%d" n
   | Literal_tez n -> fprintf ppf "%dtz" n
   | Literal_string s -> fprintf ppf "%S" s
   | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
@@ -41,6 +42,7 @@ let rec expression ppf (e:expression) = match Location.unwrap e with
   | 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_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
   | E_lambda {binder;input_type;output_type;result} ->
       fprintf ppf "lambda (%a:%a) : %a return %a"
diff --git a/src/ast_simplified/ast_simplified.ml b/src/ast_simplified/ast_simplified.ml
index 566e95155..f2eca5152 100644
--- a/src/ast_simplified/ast_simplified.ml
+++ b/src/ast_simplified/ast_simplified.ml
@@ -1,5 +1,5 @@
 include Types
-include Misc
+(* include Misc *)
 include Combinators
 
 module Types = Types
diff --git a/src/ast_simplified/combinators.ml b/src/ast_simplified/combinators.ml
index 690c9dfcb..edc8ef449 100644
--- a/src/ast_simplified/combinators.ml
+++ b/src/ast_simplified/combinators.ml
@@ -4,6 +4,17 @@ module Option = Simple_utils.Option
 
 module SMap = Map.String
 
+module Errors = struct
+  let bad_kind expected location =
+    let title () = Format.asprintf "a %s was expected" expected in
+    let message () = "" in
+    let data = [
+      ("location" , fun () -> Format.asprintf "%a" Location.pp location) ;
+    ] in
+    error ~data title message
+end
+open Errors
+
 let t_bool      : type_expression = T_constant ("bool", [])
 let t_string    : type_expression = T_constant ("string", [])
 let t_bytes     : type_expression = T_constant ("bytes", [])
@@ -32,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_set key = (T_constant ("set", [key]))
 
 let make_name (s : string) : name = s
 
@@ -40,6 +52,7 @@ let e_literal ?loc l : expression = Location.wrap ?loc @@ E_literal l
 let e_unit ?loc () : expression = Location.wrap ?loc @@ E_literal (Literal_unit)
 let e_int ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_int n)
 let e_nat ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_nat n)
+let e_timestamp ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_timestamp n)
 let e_bool ?loc   b : expression = Location.wrap ?loc @@ E_literal (Literal_bool b)
 let e_string ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_string s)
 let e_address ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_address s)
@@ -51,6 +64,7 @@ let e_some ?loc s : expression = Location.wrap ?loc @@ E_constant ("SOME", [s])
 let e_none ?loc () : expression = Location.wrap ?loc @@ E_constant ("NONE", [])
 let e_map_add ?loc k v old : expression = Location.wrap ?loc @@ E_constant ("MAP_ADD" , [k ; v ; old])
 let e_map ?loc lst : expression = Location.wrap ?loc @@ E_map lst
+let e_set ?loc lst : expression = Location.wrap ?loc @@ E_set lst
 let e_list ?loc lst : expression = Location.wrap ?loc @@ E_list lst
 let e_pair ?loc a b : expression = Location.wrap ?loc @@ E_tuple [a; b]
 let e_constructor ?loc s a : expression = Location.wrap ?loc @@ E_constructor (s , a)
@@ -90,6 +104,8 @@ 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_set ?loc lst k = e_annotation ?loc (e_set lst) (t_set k)
 
 let e_lambda ?loc (binder : string)
     (input_type : type_expression option)
@@ -140,3 +156,23 @@ let get_e_failwith = fun e ->
   | _ -> simple_fail "not a failwith"
 
 let is_e_failwith e = to_bool @@ get_e_failwith e
+
+let extract_pair : expression -> (expression * expression) result = fun e ->
+  match Location.unwrap e with
+  | E_tuple [ a ; b ] -> ok (a , b)
+  | _ -> fail @@ bad_kind "pair" e.location
+
+let extract_list : expression -> (expression list) result = fun e ->
+  match Location.unwrap e with
+  | E_list lst -> ok lst
+  | _ -> fail @@ bad_kind "list" e.location
+
+let extract_record : expression -> (string * expression) list result = fun e ->
+  match Location.unwrap e with
+  | E_record lst -> ok @@ SMap.to_kv_list lst
+  | _ -> fail @@ bad_kind "record" e.location
+
+let extract_map : expression -> (expression * expression) list result = fun e ->
+  match Location.unwrap e with
+  | E_map lst -> ok lst
+  | _ -> fail @@ bad_kind "map" e.location
diff --git a/src/ast_simplified/misc.ml b/src/ast_simplified/misc.ml
index c857b8072..e1582b073 100644
--- a/src/ast_simplified/misc.ml
+++ b/src/ast_simplified/misc.ml
@@ -42,6 +42,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
   | Literal_nat a, Literal_nat b when a = b -> ok ()
   | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
   | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
+  | Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
+  | Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
+  | Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
   | Literal_tez a, Literal_tez b when a = b -> ok ()
   | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
   | Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
@@ -59,7 +62,6 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
   | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
   | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b
 
-
 let rec assert_value_eq (a, b: (expression * expression )) : unit result =
   let error_content () =
     Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
@@ -143,6 +145,19 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
     )
   | E_list _, _ ->
       simple_fail "comparing list with other stuff"
+
+  | E_set lsta, E_set lstb -> (
+      let lsta' = List.sort (compare) lsta in
+      let lstb' = List.sort (compare) lstb in
+      let%bind lst =
+        generic_try (simple_error "set of different lengths")
+          (fun () -> List.combine lsta' lstb') in
+      let%bind _all = bind_map_list assert_value_eq lst in
+      ok ()
+    )
+  | E_set _, _ ->
+      simple_fail "comparing set with other stuff"
+
   | (E_annotation (a , _) ,  _b') -> assert_value_eq (a , b)
   | (_a' , E_annotation (b , _)) -> assert_value_eq (a , b)
   | (E_variable _, _) | (E_lambda _, _)
@@ -151,6 +166,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
   | (E_look_up _, _) | (E_matching _, _) | (E_failwith _, _) | (E_sequence _, _)
   | (E_loop _, _) | (E_assign _, _) | (E_skip, _) -> simple_fail "comparing not a value"
 
+let is_value_eq (a , b) = to_bool @@ assert_value_eq (a , b)
 
 (* module Rename = struct
  *   open Trace
diff --git a/src/ast_simplified/types.ml b/src/ast_simplified/types.ml
index 4693546b8..3eb0990cb 100644
--- a/src/ast_simplified/types.ml
+++ b/src/ast_simplified/types.ml
@@ -60,6 +60,7 @@ and expression' =
   (* Data Structures *)
   | E_map of (expr * expr) list
   | E_list of expr list
+  | E_set of expr list
   | E_look_up of (expr * expr)
   (* Matching *)
   | E_matching of (expr * matching_expr)
@@ -90,6 +91,7 @@ and literal =
   | Literal_string of string
   | Literal_bytes of bytes
   | Literal_address of string
+  | Literal_timestamp of int
   | Literal_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation
 
 and 'a matching =
diff --git a/src/ast_typed/PP.ml b/src/ast_typed/PP.ml
index 4c2122fa8..3e8edf30c 100644
--- a/src/ast_typed/PP.ml
+++ b/src/ast_typed/PP.ml
@@ -43,6 +43,7 @@ and expression ppf (e:expression) : unit =
   | 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_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
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
@@ -68,6 +69,7 @@ and literal ppf (l:literal) : unit =
   | Literal_bool b -> fprintf ppf "%b" b
   | Literal_int n -> fprintf ppf "%d" n
   | Literal_nat n -> fprintf ppf "+%d" n
+  | Literal_timestamp n -> fprintf ppf "+%d" n
   | Literal_tez n -> fprintf ppf "%dtz" n
   | Literal_string s -> fprintf ppf "%s" s
   | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
diff --git a/src/ast_typed/combinators.ml b/src/ast_typed/combinators.ml
index a6d34c72a..1b4a1926c 100644
--- a/src/ast_typed/combinators.ml
+++ b/src/ast_typed/combinators.ml
@@ -15,6 +15,8 @@ let make_n_t type_name type_value = { type_name ; type_value }
 let t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s
 let t_string ?s () : type_value = make_t (T_constant ("string", [])) s
 let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s
+let t_key ?s () : type_value = make_t (T_constant ("key", [])) s
+let t_key_hash ?s () : type_value = make_t (T_constant ("key_hash", [])) s
 let t_int ?s () : type_value = make_t (T_constant ("int", [])) s
 let t_address ?s () : type_value = make_t (T_constant ("address", [])) s
 let t_operation ?s () : type_value = make_t (T_constant ("operation", [])) s
@@ -25,6 +27,7 @@ let t_unit ?s () : type_value = make_t (T_constant ("unit", [])) s
 let t_option o ?s () : type_value = make_t (T_constant ("option", [o])) s
 let t_tuple lst ?s () : type_value = make_t (T_tuple lst) s
 let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s
+let t_set t ?s () : type_value = make_t (T_constant ("set", [t])) s
 let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s
 let t_pair a b ?s () = t_tuple [a ; b] ?s ()
 
@@ -93,6 +96,22 @@ let get_t_list (t:type_value) : type_value result = match t.type_value' with
   | T_constant ("list", [o]) -> ok o
   | _ -> simple_fail "not a list"
 
+let get_t_set (t:type_value) : type_value result = match t.type_value' with
+  | T_constant ("set", [o]) -> ok o
+  | _ -> simple_fail "not a set"
+
+let get_t_key (t:type_value) : unit result = match t.type_value' with
+  | T_constant ("key", []) -> ok ()
+  | _ -> simple_fail "not a key"
+
+let get_t_signature (t:type_value) : unit result = match t.type_value' with
+  | T_constant ("signature", []) -> ok ()
+  | _ -> simple_fail "not a signature"
+
+let get_t_key_hash (t:type_value) : unit result = match t.type_value' with
+  | T_constant ("key_hash", []) -> ok ()
+  | _ -> simple_fail "not a key_hash"
+
 let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
   | T_tuple lst -> ok lst
   | _ -> simple_fail "not a tuple"
@@ -136,7 +155,10 @@ let assert_t_map = fun t ->
 
 let is_t_map = Function.compose to_bool get_t_map
 
-let assert_t_tez :type_value -> unit result = get_t_tez
+let assert_t_tez : type_value -> unit result = get_t_tez
+let assert_t_key = get_t_key
+let assert_t_signature = get_t_signature
+let assert_t_key_hash = get_t_key_hash
 
 let assert_t_list t =
   let%bind _ = get_t_list t in
diff --git a/src/ast_typed/misc.ml b/src/ast_typed/misc.ml
index 077f00c0a..091531789 100644
--- a/src/ast_typed/misc.ml
+++ b/src/ast_typed/misc.ml
@@ -155,6 +155,7 @@ module Free_variables = struct
     | E_record_accessor (a, _) -> self a
     | 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_look_up (a , b) -> unions @@ List.map self [ a ; b ]
     | E_matching (a , cs) -> union (self a) (matching_expression b cs)
@@ -344,6 +345,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
   | Literal_nat a, Literal_nat b when a = b -> ok ()
   | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
   | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b
+  | Literal_timestamp a, Literal_timestamp b when a = b -> ok ()
+  | Literal_timestamp _, Literal_timestamp _ -> fail @@ different_literals "different timestamps" a b
+  | Literal_timestamp _, _ -> fail @@ different_literals_because_different_types "timestamp vs non-timestamp" a b
   | Literal_tez a, Literal_tez b when a = b -> ok ()
   | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
   | Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b
@@ -443,6 +447,15 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
     )
   | E_list _, _ ->
       fail @@ different_values_because_different_types "list vs. non-list" a b
+  | E_set lsta, E_set lstb -> (
+      let%bind lst =
+        generic_try (different_size_values "sets of different lengths" a b)
+          (fun () -> List.combine lsta lstb) in
+      let%bind _all = bind_map_list assert_value_eq lst in
+      ok ()
+    )
+  | E_set _, _ ->
+      fail @@ different_values_because_different_types "set vs. non-set" a b
   | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
   | (E_lambda _, _) | (E_let_in _, _) | (E_tuple_accessor _, _)
   | (E_record_accessor _, _)
diff --git a/src/ast_typed/misc_smart.ml b/src/ast_typed/misc_smart.ml
index 2c56ad89c..0d0e8cd02 100644
--- a/src/ast_typed/misc_smart.ml
+++ b/src/ast_typed/misc_smart.ml
@@ -77,6 +77,9 @@ module Captured_variables = struct
     | E_list lst ->
       let%bind lst' = bind_map_list self lst in
       ok @@ unions lst'
+    | E_set lst ->
+      let%bind lst' = bind_map_list self lst in
+      ok @@ unions lst'
     | E_map m ->
       let%bind lst' = bind_map_list self @@ List.concat @@ List.map (fun (a, b) -> [ a ; b ]) m in
       ok @@ unions lst'
diff --git a/src/ast_typed/types.ml b/src/ast_typed/types.ml
index a1bfd46d3..65524fde8 100644
--- a/src/ast_typed/types.ml
+++ b/src/ast_typed/types.ml
@@ -100,6 +100,7 @@ and expression =
   (* Data Structures *)
   | E_map of (ae * ae) list
   | E_list of ae list
+  | E_set of ae list
   | E_look_up of (ae * ae)
   (* Advanced *)
   | E_matching of (ae * matching_expr)
@@ -116,6 +117,7 @@ and literal =
   | Literal_bool of bool
   | Literal_int of int
   | Literal_nat of int
+  | Literal_timestamp of int
   | Literal_tez of int
   | Literal_string of string
   | Literal_bytes of bytes
diff --git a/src/bin/cli.ml b/src/bin/cli.ml
index 1118ac02c..86c5c9ea6 100644
--- a/src/bin/cli.ml
+++ b/src/bin/cli.ml
@@ -45,7 +45,7 @@ let source n =
   let open Arg in
   let info =
     let docv = "SOURCE_FILE" in
-    let doc = "$(docv) is the path to the .ligo file of the contract." in
+    let doc = "$(docv) is the path to the .ligo or .mligo file of the contract." in
     info ~docv ~doc [] in
   required @@ pos n (some string) None info
 
@@ -57,9 +57,9 @@ let entry_point n =
     info ~docv ~doc [] in
   required @@ pos n (some string) (Some "main") info
 
-let expression n =
+let expression purpose n =
   let open Arg in
-  let docv = "EXPRESSION" in
+  let docv = purpose ^ "_EXPRESSION" in
   let doc = "$(docv) is the expression that will be compiled." in
   let info = info ~docv ~doc [] in
   required @@ pos n (some string) None info
@@ -68,16 +68,24 @@ let syntax =
   let open Arg in
   let info =
     let docv = "SYNTAX" in
-    let doc = "$(docv) is the syntax that will be used. Currently supported syntaxes are \"pascaligo\" and \"cameligo\". \"pascaligo\" is the default." in
+    let doc = "$(docv) is the syntax that will be used. Currently supported syntaxes are \"pascaligo\" and \"cameligo\". By default, the syntax is guessed from the extension (.ligo and .mligo, respectively)." in
     info ~docv ~doc ["syntax" ; "s"] in
-  value @@ opt string "pascaligo" info
+  value @@ opt string "auto" info
+
+let amount =
+  let open Arg in
+  let info =
+    let docv = "AMOUNT" in
+    let doc = "$(docv) is the amount the dry-run transaction will use." in
+    info ~docv ~doc ["amount"] in
+  value @@ opt string "0" info
 
 let compile_file =
   let f source entry_point syntax =
     toplevel @@
     let%bind contract =
       trace (simple_info "compiling contract to michelson") @@
-      Ligo.Run.compile_contract_file source entry_point syntax in
+      Ligo.Run.compile_contract_file source entry_point (Syntax_name syntax) in
     Format.printf "%s\n" contract ;
     ok ()
   in
@@ -92,12 +100,12 @@ let compile_parameter =
     toplevel @@
     let%bind value =
       trace (simple_error "compile-input") @@
-      Ligo.Run.compile_contract_parameter source entry_point expression syntax in
+      Ligo.Run.compile_contract_parameter source entry_point expression (Syntax_name syntax) in
     Format.printf "%s\n" value;
     ok ()
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ expression 2 $ syntax) in
+    Term.(const f $ source 0 $ entry_point 1 $ expression "PARAMETER" 2 $ syntax) in
   let cmdname = "compile-parameter" in
   let docs = "Subcommand: compile parameters to a michelson expression. The resulting michelson expression can be passed as an argument in a transaction which calls a contract. See `ligo " ^ cmdname ^ " --help' for a list of options specific to this subcommand." in
   (term , Term.info ~docs cmdname)
@@ -107,54 +115,54 @@ let compile_storage =
     toplevel @@
     let%bind value =
       trace (simple_error "compile-storage") @@
-      Ligo.Run.compile_contract_storage source entry_point expression syntax in
+      Ligo.Run.compile_contract_storage source entry_point expression (Syntax_name syntax) in
     Format.printf "%s\n" value;
     ok ()
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ expression 2 $ syntax) in
+    Term.(const f $ source 0 $ entry_point 1 $ expression "STORAGE" 2 $ syntax) 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 syntax =
+  let f source entry_point storage input amount syntax =
     toplevel @@
     let%bind output =
-      Ligo.Run.run_contract source entry_point storage input syntax in
+      Ligo.Run.run_contract ~amount source entry_point storage input (Syntax_name syntax) in
     Format.printf "%a\n" Ast_simplified.PP.expression output ;
     ok ()
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ expression 2 $ expression 3 $ syntax) in
+    Term.(const f $ source 0 $ entry_point 1 $ expression "PARAMETER" 2 $ expression "STORAGE" 3 $ amount $ syntax) 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)
 
 let run_function =
-  let f source entry_point parameter syntax =
+  let f source entry_point parameter amount syntax =
     toplevel @@
     let%bind output =
-      Ligo.Run.run_function source entry_point parameter syntax in
+      Ligo.Run.run_function ~amount source entry_point parameter (Syntax_name syntax) in
     Format.printf "%a\n" Ast_simplified.PP.expression output ;
     ok ()
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ expression 2 $ syntax) in
+    Term.(const f $ source 0 $ entry_point 1 $ expression "PARAMETER" 2 $ amount $ syntax) in
   let cmdname = "run-function" in
   let docs = "Subcommand: run a function with the given parameter." in
   (term , Term.info ~docs cmdname)
 
 let evaluate_value =
-  let f source entry_point syntax =
+  let f source entry_point amount syntax =
     toplevel @@
     let%bind output =
-      Ligo.Run.evaluate_value source entry_point syntax in
+      Ligo.Run.evaluate_value ~amount source entry_point (Syntax_name syntax) in
     Format.printf "%a\n" Ast_simplified.PP.expression output ;
     ok ()
   in
   let term =
-    Term.(const f $ source 0 $ entry_point 1 $ syntax) in
+    Term.(const f $ source 0 $ entry_point 1 $ amount $ syntax) in
   let cmdname = "evaluate-value" in
   let docs = "Subcommand: evaluate a given definition." in
   (term , Term.info ~docs cmdname)
diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml
index db8e7936e..ebd20a00a 100644
--- a/src/compiler/compiler_program.ml
+++ b/src/compiler/compiler_program.ml
@@ -16,6 +16,16 @@ let get_predicate : string -> type_value -> expression list -> predicate result
   | Some x -> ok x
   | None -> (
       match s with
+      | "NONE" -> (
+          let%bind ty' = Mini_c.get_t_option ty in
+          let%bind m_ty = Compiler_type.type_ ty' in
+          ok @@ simple_unary @@ prim ~children:[m_ty] I_NONE
+        )
+      | "UNPACK" -> (
+          let%bind ty' = Mini_c.get_t_option ty in
+          let%bind m_ty = Compiler_type.type_ ty' in
+          ok @@ simple_unary @@ prim ~children:[m_ty] I_UNPACK
+        )
       | "MAP_REMOVE" ->
           let%bind v = match lst with
             | [ _ ; expr ] ->
@@ -52,6 +62,7 @@ let rec translate_value (v:value) : michelson result = match v with
   | D_bool b -> ok @@ prim (if b then D_True else D_False)
   | D_int n -> ok @@ int (Z.of_int n)
   | D_nat n -> ok @@ int (Z.of_int n)
+  | D_timestamp n -> ok @@ int (Z.of_int n)
   | D_tez n -> ok @@ int (Z.of_int n)
   | D_string s -> ok @@ string s
   | D_bytes s -> ok @@ bytes (Tezos_stdlib.MBytes.of_bytes s)
@@ -75,6 +86,9 @@ let rec translate_value (v:value) : michelson result = match v with
   | D_list lst ->
       let%bind lst' = bind_map_list translate_value lst in
       ok @@ seq lst'
+  | D_set lst ->
+      let%bind lst' = bind_map_list translate_value lst in
+      ok @@ seq lst'
   | D_operation _ ->
       simple_fail "can't compile an operation"
 
@@ -216,14 +230,6 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
       i_drop ;
       b' ;
     ]
-  (* | E_sequence_drop (a , b) ->
-   *   let%bind (a' , env_a) = translate_expression a env in
-   *   let%bind (b' , env_b) = translate_expression b env_a in
-   *   return ~end_env:env_b @@ seq [
-   *     a' ;
-   *     i_drop ;
-   *     b' ;
-   *   ] *)
   | E_constant(str, lst) ->
       let module L = Logger.Stateful() in
       let%bind lst' =
@@ -269,6 +275,9 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
   | E_make_empty_list t ->
       let%bind t' = Compiler_type.type_ t in
       return @@ i_nil t'
+  | E_make_empty_set t ->
+      let%bind t' = Compiler_type.type_ t in
+      return @@ i_empty_set t'
   | E_make_none o ->
       let%bind o' = Compiler_type.type_ o in
       return @@ i_none o'
diff --git a/src/compiler/compiler_type.ml b/src/compiler/compiler_type.ml
index 18ea463cf..2632f2bd8 100644
--- a/src/compiler/compiler_type.ml
+++ b/src/compiler/compiler_type.ml
@@ -35,6 +35,7 @@ module Ty = struct
     | T_pair _ -> fail (not_comparable "pair")
     | T_map _ -> fail (not_comparable "map")
     | T_list _ -> fail (not_comparable "list")
+    | T_set _ -> fail (not_comparable "set")
     | T_option _ -> fail (not_comparable "option")
     | T_contract _ -> fail (not_comparable "contract")
 
@@ -82,6 +83,10 @@ module Ty = struct
     | T_list t ->
         let%bind (Ex_ty t') = type_ t in
         ok @@ Ex_ty Contract_types.(list t')
+    | T_set t -> (
+        let%bind (Ex_comparable_ty t') = comparable_type t in
+        ok @@ Ex_ty Contract_types.(set t')
+      )
     | T_option t ->
         let%bind (Ex_ty t') = type_ t in
         ok @@ Ex_ty Contract_types.(option t')
@@ -142,6 +147,9 @@ let rec type_ : type_value -> O.michelson result =
   | T_list t ->
       let%bind t' = type_ t in
       ok @@ O.prim ~children:[t'] O.T_list
+  | T_set t ->
+      let%bind t' = type_ t in
+      ok @@ O.prim ~children:[t'] O.T_set
   | T_option o ->
       let%bind o' = type_ o in
       ok @@ O.prim ~children:[o'] O.T_option
diff --git a/src/compiler/uncompiler.ml b/src/compiler/uncompiler.ml
index ebf9f4028..d8855471e 100644
--- a/src/compiler/uncompiler.ml
+++ b/src/compiler/uncompiler.ml
@@ -29,6 +29,11 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
         trace_option (simple_error "too big to fit an int") @@
         Alpha_context.Script_int.to_int n in
       ok @@ D_nat n
+  | (Timestamp_t _), n ->
+      let n =
+        Z.to_int @@
+        Alpha_context.Script_timestamp.to_zint n in
+      ok @@ D_timestamp n
   | (Mutez_t _), n ->
       let%bind n =
         generic_try (simple_error "too big to fit an int") @@
@@ -72,6 +77,18 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
         bind_map_list aux lst'
       in
       ok @@ D_list lst''
+  | (Set_t (ty, _)), (module S) -> (
+      let lst = S.OPS.elements S.boxed in
+      let lst' =
+        let aux acc cur = cur :: acc in
+        let lst = List.fold_left aux lst [] in
+        List.rev lst in
+      let%bind lst'' =
+        let aux = fun t -> translate_value (Ex_typed_value (ty_of_comparable_ty ty, t)) in
+        bind_map_list aux lst'
+      in
+      ok @@ D_set lst''
+    )
   | (Operation_t _) , op ->
       ok @@ D_operation op
   | ty, v ->
diff --git a/src/contracts/amount.mligo b/src/contracts/amount.mligo
new file mode 100644
index 000000000..995f165fe
--- /dev/null
+++ b/src/contracts/amount.mligo
@@ -0,0 +1 @@
+let check = if Current.amount > 100tz then 42 else 0
\ No newline at end of file
diff --git a/src/contracts/super-counter.mligo b/src/contracts/super-counter.mligo
new file mode 100644
index 000000000..ff3a1f5fb
--- /dev/null
+++ b/src/contracts/super-counter.mligo
@@ -0,0 +1,10 @@
+type action =
+| Increment of int
+| Decrement of int
+
+let main (p : action) (s : int) : (operation list * int) =
+  let storage =
+    match p with
+    | Increment n -> s + n
+    | Decrement n -> s - n in
+  (([] : operation list) , storage)
diff --git a/src/contracts/vote.mligo b/src/contracts/vote.mligo
new file mode 100644
index 000000000..136933526
--- /dev/null
+++ b/src/contracts/vote.mligo
@@ -0,0 +1,55 @@
+type storage = {
+  title : string ;
+  candidates : (string , int) map ;
+  voters : address set ;
+  beginning_time : timestamp ;
+  finish_time : timestamp ;
+}
+
+type init_action = {
+  title : string ;
+  beginning_time : timestamp ;
+  finish_time : timestamp ;
+}
+
+type action =
+  | Vote of string
+  | Init of init_action
+
+let init (init_params : init_action) (_ : storage) =
+  let candidates = Map [
+      ("Yes" , 0) ;
+      ("No" , 0)
+    ] in
+  (
+    ([] : operation list),
+    {
+      title = init_params.title ;
+      candidates = candidates ;
+      voters = (Set [] : address set) ;
+      beginning_time = init_params.beginning_time ;
+      finish_time = init_params.finish_time ;
+    }
+  )
+
+let vote (parameter : string) (storage : storage) =
+  let now = Current.time in
+  (* let _ = assert (now >= storage.beginning_time && storage.finish_time > now) in *)
+  let addr = Current.source in
+  (* let _ = assert (not Set.mem addr storage.voters) in *)
+  let x = Map.find parameter storage.candidates in
+  (
+    ([] : operation list),
+    {
+      title = storage.title ;
+      candidates = Map.update parameter (Some (x + 1)) storage.candidates ;
+      voters = Set.add addr storage.voters ;
+      beginning_time = storage.beginning_time ;
+      finish_time = storage.finish_time ;
+    }
+  )
+
+let main (action : action) (storage : storage) =
+  match action with
+  | Vote p -> vote p storage
+  | Init ps -> init ps storage
diff --git a/src/main/run_simplified.ml b/src/main/run_simplified.ml
index 898ba6954..17833d6b3 100644
--- a/src/main/run_simplified.ml
+++ b/src/main/run_simplified.ml
@@ -17,8 +17,8 @@ let run_simplityped
   let%bind annotated_result = Typer.untype_expression typed_result in
   ok annotated_result
 
-let evaluate_simplityped (program : Ast_typed.program) (entry : string)
+let evaluate_simplityped ?options (program : Ast_typed.program) (entry : string)
   : Ast_simplified.expression result =
-  let%bind typed_result = Run_typed.evaluate_typed entry program in
+  let%bind typed_result = Run_typed.evaluate_typed ?options entry program in
   let%bind annotated_result = Typer.untype_expression typed_result in
   ok annotated_result
diff --git a/src/main/run_source.ml b/src/main/run_source.ml
index 79f71ce97..a0a18be96 100644
--- a/src/main/run_source.ml
+++ b/src/main/run_source.ml
@@ -95,24 +95,54 @@ let parsify_expression_ligodity = fun source ->
     Simplify.Ligodity.simpl_expression raw in
   ok simplified
 
-let parsify = fun syntax source ->
-  let%bind parsify = match syntax with
-    | "pascaligo" -> ok parsify_pascaligo
-    | "cameligo" -> ok parsify_ligodity
-    | _ -> simple_fail "unrecognized parser"
+type s_syntax = Syntax_name of string
+type v_syntax =  [`pascaligo | `cameligo ]
+
+let syntax_to_variant : s_syntax -> string option -> v_syntax result =
+  fun syntax source_filename ->
+  let subr s n =
+    String.sub s (String.length s - n) n in
+  let endswith s suffix =
+    let suffixlen = String.length suffix in
+    (  String.length s >= suffixlen
+       && String.equal (subr s suffixlen) suffix)
   in
-  parsify source
+  match syntax with
+    Syntax_name syntax ->
+    begin
+      if String.equal syntax "auto" then
+        begin
+          match source_filename with
+          | Some source_filename
+            when endswith source_filename ".ligo"
+            -> ok `pascaligo
+          | Some source_filename
+            when endswith source_filename ".mligo"
+            -> ok `cameligo
+          | _ -> simple_fail "cannot auto-detect syntax, pleas use -s name_of_syntax"
+        end
+      else if String.equal syntax "pascaligo" then ok `pascaligo
+      else if String.equal syntax "cameligo" then ok `cameligo
+      else simple_fail "unrecognized parser"
+    end
+
+let parsify = fun (syntax : v_syntax) source_filename ->
+  let%bind parsify = match syntax with
+    | `pascaligo -> ok parsify_pascaligo
+    | `cameligo -> ok parsify_ligodity
+  in
+  parsify source_filename
 
 let parsify_expression = fun syntax source ->
   let%bind parsify = match syntax with
-    | "pascaligo" -> ok parsify_expression_pascaligo
-    | "cameligo" -> ok parsify_expression_ligodity
-    | _ -> simple_fail "unrecognized parser"
+    | `pascaligo -> ok parsify_expression_pascaligo
+    | `cameligo -> ok parsify_expression_ligodity
   in
   parsify source
 
-let compile_contract_file : string -> string -> string -> string result = fun source entry_point syntax ->
-  let%bind simplified = parsify syntax source in
+let compile_contract_file : string -> string -> s_syntax -> string result = fun source_filename entry_point syntax ->
+  let%bind syntax = syntax_to_variant syntax (Some source_filename) in
+  let%bind simplified = parsify syntax source_filename in
   let%bind () =
     assert_entry_point_defined simplified entry_point in
   let%bind typed =
@@ -128,9 +158,10 @@ let compile_contract_file : string -> string -> string -> string result = fun so
     Format.asprintf "%a" Michelson.pp_stripped michelson in
   ok str
 
-let compile_contract_parameter : string -> string -> string -> string -> string result = fun source entry_point expression syntax ->
+let compile_contract_parameter : string -> string -> string -> s_syntax -> string result = fun source_filename entry_point expression syntax ->
+  let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind (program , parameter_tv) =
-    let%bind simplified = parsify syntax source in
+    let%bind simplified = parsify syntax source_filename in
     let%bind () =
       assert_entry_point_defined simplified entry_point in
     let%bind typed =
@@ -166,9 +197,10 @@ let compile_contract_parameter : string -> string -> string -> string -> string
   ok expr
 
 
-let compile_contract_storage : string -> string -> string -> string -> string result = fun source entry_point expression syntax ->
+let compile_contract_storage : string -> string -> string -> s_syntax -> string result = fun source_filename entry_point expression syntax ->
+  let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind (program , storage_tv) =
-    let%bind simplified = parsify syntax source in
+    let%bind simplified = parsify syntax source_filename in
     let%bind () =
       assert_entry_point_defined simplified entry_point in
     let%bind typed =
@@ -204,8 +236,8 @@ let compile_contract_storage : string -> string -> string -> string -> string re
   ok expr
 
 let type_file ?(debug_simplify = false) ?(debug_typed = false)
-    syntax (path:string) : Ast_typed.program result =
-  let%bind simpl = parsify syntax path in
+    syntax (source_filename:string) : Ast_typed.program result =
+  let%bind simpl = parsify syntax source_filename in
   (if debug_simplify then
      Format.(printf "Simplified : %a\n%!" Ast_simplified.PP.program simpl)
   ) ;
@@ -217,23 +249,38 @@ let type_file ?(debug_simplify = false) ?(debug_typed = false)
     )) ;
   ok typed
 
-let run_contract source entry_point storage input syntax =
+let run_contract ?amount source_filename entry_point storage input syntax =
+  let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind typed =
-    type_file syntax source in
+    type_file syntax source_filename in
   let%bind storage_simpl =
     parsify_expression syntax storage in
   let%bind input_simpl =
     parsify_expression syntax input in
-  Run_simplified.run_simplityped typed entry_point (Ast_simplified.e_pair storage_simpl input_simpl)
+  let options =
+    let open Proto_alpha_utils.Memory_proto_alpha in
+    let amount = Option.bind (fun amount -> Alpha_context.Tez.of_string amount) amount in
+    (make_options ?amount ()) in
+  Run_simplified.run_simplityped ~options typed entry_point (Ast_simplified.e_pair storage_simpl input_simpl)
 
-let run_function source entry_point parameter syntax =
+let run_function ?amount source_filename entry_point parameter syntax =
+  let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind typed =
-    type_file syntax source in
+    type_file syntax source_filename in
   let%bind parameter' =
     parsify_expression syntax parameter in
-  Run_simplified.run_simplityped typed entry_point parameter'
+  let options =
+    let open Proto_alpha_utils.Memory_proto_alpha in
+    let amount = Option.bind (fun amount -> Alpha_context.Tez.of_string amount) amount in
+    (make_options ?amount ()) in
+  Run_simplified.run_simplityped ~options typed entry_point parameter'
 
-let evaluate_value source entry_point syntax =
+let evaluate_value ?amount source_filename entry_point syntax =
+  let%bind syntax = syntax_to_variant syntax (Some source_filename) in
   let%bind typed =
-    type_file syntax source in
-  Run_simplified.evaluate_simplityped typed entry_point
+    type_file syntax source_filename in
+  let options =
+    let open Proto_alpha_utils.Memory_proto_alpha in
+    let amount = Option.bind (fun amount -> Alpha_context.Tez.of_string amount) amount in
+    (make_options ?amount ()) in
+  Run_simplified.evaluate_simplityped ~options typed entry_point
diff --git a/src/main/run_typed.ml b/src/main/run_typed.ml
index 47a67469d..4f0ff0f77 100644
--- a/src/main/run_typed.ml
+++ b/src/main/run_typed.ml
@@ -13,12 +13,12 @@ let transpile_value
   let%bind r = Run_mini_c.run_entry f input in
   ok r
 
-let evaluate_typed (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result =
+let evaluate_typed ?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result =
   trace (simple_error "easy evaluate typed") @@
   let%bind result =
     let%bind mini_c_main =
       Transpiler.translate_entry program entry in
-    Run_mini_c.run_entry mini_c_main (Mini_c.Combinators.d_unit) in
+    Run_mini_c.run_entry ?options mini_c_main (Mini_c.Combinators.d_unit) in
   let%bind typed_result =
     let%bind typed_main = Ast_typed.get_entry program entry in
     Transpiler.untranspile result typed_main.type_annotation in
diff --git a/src/meta_michelson/contract.ml b/src/meta_michelson/contract.ml
index 7e38869c9..a9174a098 100644
--- a/src/meta_michelson/contract.ml
+++ b/src/meta_michelson/contract.ml
@@ -267,6 +267,7 @@ module Types = struct
   let key = Key_t None
 
   let list a = List_t (a, None)
+  let set a = Set_t (a, None)
   let assert_list = function
     | List_t (a, _) -> a
     | _ -> assert false
diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml
index 51867e490..af5543689 100644
--- a/src/mini_c/PP.ml
+++ b/src/mini_c/PP.ml
@@ -27,6 +27,7 @@ let rec type_ ppf : type_value -> _ = function
   | 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_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
   | T_contract(t) -> fprintf ppf "contract(%a)" type_ t
   | T_deep_closure(c, arg, ret) ->
@@ -45,6 +46,7 @@ let rec value ppf : value -> unit = function
   | D_operation _ -> fprintf ppf "operation[...bytes]"
   | D_int n -> fprintf ppf "%d" n
   | D_nat n -> fprintf ppf "+%d" n
+  | D_timestamp n -> fprintf ppf "+%d" n
   | D_tez n -> fprintf ppf "%dtz" n
   | D_unit -> fprintf ppf " "
   | D_string s -> fprintf ppf "\"%s\"" s
@@ -57,6 +59,7 @@ let rec value ppf : value -> unit = function
   | D_some s -> fprintf ppf "Some (%a)" value s
   | D_map m -> fprintf ppf "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
 
 and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
   fprintf ppf "%a -> %a" value a value b
@@ -73,6 +76,7 @@ and expression' ppf (e:expression') = match e with
   | E_literal v -> fprintf ppf "%a" value v
   | E_make_empty_map _ -> fprintf ppf "map[]"
   | E_make_empty_list _ -> fprintf ppf "list[]"
+  | E_make_empty_set _ -> fprintf ppf "set[]"
   | E_make_none _ -> fprintf ppf "none"
   | E_if_bool (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
   | E_if_none (c, n, ((name, _) , s)) -> fprintf ppf "%a ?? %a : %s -> %a" expression c expression n name expression s
diff --git a/src/mini_c/combinators.ml b/src/mini_c/combinators.ml
index 670d63e5f..3aa4d5726 100644
--- a/src/mini_c/combinators.ml
+++ b/src/mini_c/combinators.ml
@@ -37,6 +37,10 @@ let get_nat (v:value) = match v with
   | D_nat n -> ok n
   | _ -> simple_fail "not a nat"
 
+let get_timestamp (v:value) = match v with
+  | D_timestamp n -> ok n
+  | _ -> simple_fail "not a timestamp"
+
 let get_string (v:value) = match v with
   | D_string s -> ok s
   | _ -> simple_fail "not a string"
@@ -62,6 +66,10 @@ let get_list (v:value) = match v with
   | D_list lst -> ok lst
   | _ -> simple_fail "not a list"
 
+let get_set (v:value) = match v with
+  | D_set lst -> ok lst
+  | _ -> simple_fail "not a set"
+
 let get_t_option (v:type_value) = match v with
   | T_option t -> ok t
   | _ -> simple_fail "not an option"
@@ -82,6 +90,10 @@ let get_t_list (t:type_value) = match t with
   | T_list t -> ok t
   | _ -> simple_fail "not a type list"
 
+let get_t_set (t:type_value) = match t with
+  | T_set t -> ok t
+  | _ -> simple_fail "not a type set"
+
 let get_left (v:value) = match v with
   | D_left b -> ok b
   | _ -> simple_fail "not a left"
diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml
index 6e5bb4906..57f117165 100644
--- a/src/mini_c/types.ml
+++ b/src/mini_c/types.ml
@@ -16,6 +16,7 @@ type type_value =
   | T_base of type_base
   | T_map of (type_value * type_value)
   | T_list of type_value
+  | T_set of type_value
   | T_contract of type_value
   | T_option of type_value
 
@@ -35,6 +36,7 @@ type value =
   | D_unit
   | D_bool of bool
   | D_nat of int
+  | D_timestamp of int
   | D_tez of int
   | D_int of int
   | D_string of string
@@ -46,6 +48,7 @@ type value =
   | D_none
   | D_map of (value * value) list
   | D_list of value list
+  | D_set of value list
   (* | `Macro of anon_macro ... The future. *)
   | D_function of anon_function
   | D_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation
@@ -64,6 +67,7 @@ and expression' =
   | E_variable of var_name
   | E_make_empty_map of (type_value * type_value)
   | E_make_empty_list of type_value
+  | E_make_empty_set of type_value
   | E_make_none of type_value
   | E_if_bool of expression * expression * expression
   | E_if_none of expression * expression * ((var_name * type_value) * expression)
diff --git a/src/operators/helpers.ml b/src/operators/helpers.ml
index 7cdc617f4..7982ddde0 100644
--- a/src/operators/helpers.ml
+++ b/src/operators/helpers.ml
@@ -88,6 +88,7 @@ module Typer = struct
         t_string () ;
         t_bytes () ;
         t_address () ;
+        t_timestamp () ;
       ] in
     ok @@ t_bool ()
 
diff --git a/src/operators/operators.ml b/src/operators/operators.ml
index d8c3d134f..70fc01986 100644
--- a/src/operators/operators.ml
+++ b/src/operators/operators.ml
@@ -42,6 +42,9 @@ module Simplify = struct
     ("bool" , "bool") ;
     ("operation" , "operation") ;
     ("address" , "address") ;
+    ("key" , "key") ;
+    ("key_hash" , "key_hash") ;
+    ("signature" , "signature") ;
     ("timestamp" , "timestamp") ;
     ("contract" , "contract") ;
     ("list" , "list") ;
@@ -76,7 +79,7 @@ module Simplify = struct
       ("Bytes.pack" , "PACK") ;
       ("Crypto.hash" , "HASH") ;
       ("Operation.transaction" , "CALL") ;
-      ("Operation.get_contract" , "GET_CONTRACT") ;
+      ("Operation.get_contract" , "CONTRACT") ;
       ("sender" , "SENDER") ;
       ("unit" , "UNIT") ;
       ("source" , "SOURCE") ;
@@ -87,6 +90,8 @@ module Simplify = struct
 
   module Ligodity = struct
     let constants = [
+      ("assert" , "ASSERT") ;
+      
       ("Current.balance", "BALANCE") ;
       ("balance", "BALANCE") ;
       ("Current.time", "NOW") ;
@@ -97,6 +102,8 @@ module Simplify = struct
       ("gas", "STEPS_TO_QUOTA") ;
       ("Current.sender" , "SENDER") ;
       ("sender", "SENDER") ;
+      ("Current.source" , "SOURCE") ;
+      ("source", "SOURCE") ;
       ("Current.failwith", "FAILWITH") ;
       ("failwith" , "FAILWITH") ;
 
@@ -115,6 +122,17 @@ module Simplify = struct
       ("Bytes.slice", "SLICE") ;
       ("Bytes.sub", "SLICE") ;
 
+      ("Set.mem" , "SET_MEM") ;
+      ("Set.empty" , "SET_EMPTY") ;
+      ("Set.add" , "SET_ADD") ;
+      ("Set.remove" , "SET_REMOVE") ;
+
+      ("Map.find_opt" , "MAP_FIND_OPT") ;
+      ("Map.find" , "MAP_FIND") ;
+      ("Map.update" , "MAP_UPDATE") ;
+      ("Map.add" , "MAP_ADD") ;
+      ("Map.remove" , "MAP_REMOVE") ;
+      
       ("String.length", "SIZE") ;
       ("String.size", "SIZE") ;
       ("String.slice", "SLICE") ;
@@ -126,7 +144,7 @@ module Simplify = struct
       ("List.iter", "ITER") ;
 
       ("Operation.transaction" , "CALL") ;
-      ("Operation.get_contract" , "GET_CONTRACT") ;
+      ("Operation.get_contract" , "CONTRACT") ;
       ("int" , "INT") ;
       ("abs" , "ABS") ;
       ("unit" , "UNIT") ;
@@ -195,7 +213,7 @@ module Typer = struct
     let%bind () = assert_type_value_eq (dst, v) in
     ok m
 
-  let map_update : typer = typer_3 "MAP_UPDATE_TODO" @@ fun k v m ->
+  let map_update : typer = typer_3 "MAP_UPDATE" @@ fun k v m ->
     let%bind (src, dst) = get_t_map m in
     let%bind () = assert_type_value_eq (src, k) in
     let%bind v' = get_t_option v in
@@ -207,7 +225,12 @@ module Typer = struct
     let%bind () = assert_type_value_eq (src, k) in
     ok @@ t_bool ()
 
-  let map_find : typer = typer_2 "MAP_FIND_TODO" @@ fun k m ->
+  let map_find : typer = typer_2 "MAP_FIND" @@ fun k m ->
+    let%bind (src, dst) = get_t_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 () = assert_type_value_eq (src, k) in
     ok @@ t_option dst ()
@@ -243,9 +266,15 @@ module Typer = struct
   let size = typer_1 "SIZE" @@ fun t ->
     let%bind () =
       Assert.assert_true @@
-      (is_t_map t || is_t_list t) in
+      (is_t_map t || is_t_list t || is_t_string t) in
     ok @@ t_nat ()
 
+  let slice = typer_3 "SLICE" @@ fun i j s ->
+    let%bind () =
+      Assert.assert_true @@
+      (is_t_nat i && is_t_nat j && is_t_string s) in
+    ok @@ t_string ()
+  
   let failwith_ = typer_1 "FAILWITH" @@ fun t ->
     let%bind () =
       Assert.assert_true @@
@@ -269,10 +298,28 @@ module Typer = struct
     trace_option (simple_error "untyped UNPACK") @@
     output_opt
 
-  let crypto_hash = typer_1 "HASH" @@ fun t ->
+  let hash256 = typer_1 "SHA256" @@ fun t ->
     let%bind () = assert_t_bytes t in
     ok @@ t_bytes ()
 
+  let hash512 = typer_1 "SHA512" @@ fun t ->
+    let%bind () = assert_t_bytes t in
+    ok @@ t_bytes ()
+
+  let blake2b = typer_1 "BLAKE2b" @@ fun t ->
+    let%bind () = assert_t_bytes t in
+    ok @@ t_bytes ()
+
+  let hash_key = typer_1 "HASH_KEY" @@ fun t ->
+    let%bind () = assert_t_key t in
+    ok @@ t_key_hash ()
+
+  let check_signature = typer_3 "CHECK_SIGNATURE" @@ fun k s b ->
+    let%bind () = assert_t_key k in
+    let%bind () = assert_t_signature s in
+    let%bind () = assert_t_bytes b in
+    ok @@ t_bool ()
+  
   let sender = constant "SENDER" @@ t_address ()
 
   let source = constant "SOURCE" @@ t_address ()
@@ -281,6 +328,8 @@ module Typer = struct
 
   let amount = constant "AMOUNT" @@ t_tez ()
 
+  let address = constant "ADDRESS" @@ t_address ()
+
   let now = constant "NOW" @@ t_timestamp ()
 
   let transaction = typer_3 "CALL" @@ fun param amount contract ->
@@ -301,6 +350,11 @@ module Typer = struct
     let%bind () = assert_t_int t in
     ok @@ t_nat ()
 
+  let assertion = typer_1 "ASSERT" @@ fun a ->
+    if eq_1 a (t_bool ())
+    then ok @@ t_unit ()
+    else simple_fail "Asserting a non-bool"
+  
   let times = typer_2 "TIMES" @@ fun a b ->
     if eq_2 (a , b) (t_nat ())
     then ok @@ t_nat () else
@@ -335,6 +389,29 @@ module Typer = struct
     then ok @@ t_int () else
       simple_fail "Adding with wrong types. Expected nat, int or tez."
 
+  let set_mem = typer_2 "SET_MEM" @@ fun elt set ->
+    let%bind key = get_t_set set in
+    if eq_1 elt key
+    then ok @@ t_bool ()
+    else simple_fail "Set_mem: elt and set don't match"
+
+  let set_add = typer_2 "SET_ADD" @@ fun elt set ->
+    let%bind key = get_t_set set in
+    if eq_1 elt key
+    then ok set
+    else simple_fail "Set_add: elt and set don't match"
+
+  let set_remove = typer_2 "SET_REMOVE" @@ fun elt set ->
+    let%bind key = get_t_set set in
+    if eq_1 elt key
+    then ok set
+    else simple_fail "Set_remove: elt and set don't match"
+
+  let not_ = typer_1 "NOT" @@ fun elt ->
+    if eq_1 elt (t_bool ())
+    then ok @@ t_bool ()
+    else simple_fail "bad parameter to not"
+  
   let constant_typers = Map.String.of_list [
       add ;
       times ;
@@ -351,6 +428,7 @@ module Typer = struct
       comparator "GE" ;
       boolean_operator_2 "OR" ;
       boolean_operator_2 "AND" ;
+      not_ ;
       map_remove ;
       map_add ;
       map_update ;
@@ -360,6 +438,9 @@ module Typer = struct
       map_map ;
       map_fold ;
       map_iter ;
+      set_mem ;
+      set_add ;
+      set_remove ;
       (* map_size ; (* use size *) *)
       int ;
       size ;
@@ -367,7 +448,11 @@ module Typer = struct
       get_force ;
       bytes_pack ;
       bytes_unpack ;
-      crypto_hash ;
+      hash256 ;
+      hash512 ;
+      blake2b ;
+      hash_key ;
+      check_signature ;
       sender ;
       source ;
       unit ;
@@ -376,6 +461,9 @@ module Typer = struct
       get_contract ;
       abs ;
       now ;
+      slice ;
+      address ;
+      assertion ;
     ]
 
 end
@@ -407,6 +495,8 @@ module Compiler = struct
     ("NEG" , simple_unary @@ prim I_NEG) ;
     ("OR" , simple_binary @@ prim I_OR) ;
     ("AND" , simple_binary @@ prim I_AND) ;
+    ("XOR" , simple_binary @@ prim I_XOR) ;
+    ("NOT" , simple_unary @@ prim I_NOT) ;
     ("PAIR" , simple_binary @@ prim I_PAIR) ;
     ("CAR" , simple_unary @@ prim I_CAR) ;
     ("CDR" , simple_unary @@ prim I_CDR) ;
@@ -419,21 +509,35 @@ module Compiler = struct
     ("UPDATE" , simple_ternary @@ prim I_UPDATE) ;
     ("SOME" , simple_unary @@ prim I_SOME) ;
     ("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) ;
     ("SIZE" , simple_unary @@ prim I_SIZE) ;
     ("FAILWITH" , simple_unary @@ prim I_FAILWITH) ;
-    ("ASSERT" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
+    ("ASSERT_INFERRED" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
+    ("ASSERT" , simple_unary @@ i_if (seq [i_push_unit ; i_failwith]) (seq [i_push_unit])) ;
     ("INT" , simple_unary @@ prim I_INT) ;
     ("ABS" , simple_unary @@ prim I_ABS) ;
     ("CONS" , simple_binary @@ prim I_CONS) ;
     ("UNIT" , simple_constant @@ prim I_UNIT) ;
     ("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
+    ("ADDRESS" , simple_constant @@ prim I_ADDRESS) ;
     ("NOW" , simple_constant @@ prim I_NOW) ;
     ("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) ;
+    ("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]) ;
+    ("SLICE" , simple_ternary @@ prim I_SLICE) ;
+    ("SHA256" , simple_unary @@ prim I_SHA256) ;
+    ("SHA512" , simple_unary @@ prim I_SHA512) ;
+    ("BLAKE2B" , simple_unary @@ prim I_BLAKE2B) ;
+    ("CHECK_SIGNATURE" , simple_ternary @@ prim I_CHECK_SIGNATURE) ;
+    ("HASH_KEY" , simple_unary @@ prim I_HASH_KEY) ;
+    ("PACK" , simple_unary @@ prim I_PACK) ;
   ]
 
+  (* Some complex predicates will need to be added in compiler/compiler_program *)
+  
 end
diff --git a/src/parser/ligodity.ml b/src/parser/ligodity.ml
index fba239b59..b56d63ea2 100644
--- a/src/parser/ligodity.ml
+++ b/src/parser/ligodity.ml
@@ -34,6 +34,19 @@ let parse_file (source: string) : AST.t result =
           in
           simple_error str
         )
+      | Lexer.Error err -> (
+          let start = Lexing.lexeme_start_p lexbuf in
+          let end_ = Lexing.lexeme_end_p lexbuf in
+          let str = Format.sprintf
+              "Lexer error (%s) at \"%s\" from (%d, %d) to (%d, %d). In file \"%s|%s\"\n"
+              (err.value)
+              (Lexing.lexeme lexbuf)
+              start.pos_lnum (start.pos_cnum - start.pos_bol)
+              end_.pos_lnum (end_.pos_cnum - end_.pos_bol)
+              start.pos_fname source
+          in
+          simple_error str
+        )
       | exn ->
           let start = Lexing.lexeme_start_p lexbuf in
           let end_ = Lexing.lexeme_end_p lexbuf in
diff --git a/src/simplify/ligodity.ml b/src/simplify/ligodity.ml
index cd3a4472d..34866fd91 100644
--- a/src/simplify/ligodity.ml
+++ b/src/simplify/ligodity.ml
@@ -147,6 +147,22 @@ module Errors = struct
     ] in
     error ~data title message
 
+  let bad_set_definition =
+    let title () = "bad set definition" in
+    let message () = "a set definition is a list" in
+    info title message
+
+  let bad_list_definition =
+    let title () = "bad list definition" in
+    let message () = "a list definition is a list" in
+    info title message
+
+  let bad_map_definition =
+    let title () = "bad map definition" in
+    let message () = "a map definition is a list of pairs" in
+    info title message
+
+  
   let corner_case ~loc message =
     let title () = "corner case" in
     let content () = "We don't have a good error message for this case. \
@@ -158,6 +174,7 @@ module Errors = struct
       ("message" , fun () -> message) ;
     ] in
     error ~data title content
+
 end
 
 open Errors
@@ -170,6 +187,7 @@ let rec pattern_to_var : Raw.pattern -> _ = fun p ->
   match p with
   | Raw.PPar p -> pattern_to_var p.value.inside
   | Raw.PVar v -> ok v
+  | Raw.PWild r -> ok @@ ({ region = r ; value = "_" } : Raw.variable)
   | _ -> fail @@ wrong_pattern "var" p
 
 let rec pattern_to_typed_var : Raw.pattern -> _ = fun p ->
@@ -181,6 +199,7 @@ let rec pattern_to_typed_var : Raw.pattern -> _ = fun p ->
       ok (v , Some tp.type_expr)
     )
   | Raw.PVar v -> ok (v , None)
+  | Raw.PWild r -> ok (({ region = r ; value = "_" } : Raw.variable) , None)
   | _ -> fail @@ wrong_pattern "typed variable" p
 
 let rec expr_to_typed_expr : Raw.expr -> _ = fun e ->
@@ -358,10 +377,37 @@ let rec simpl_expression :
       let (c_name , _c_loc) = r_split c_name in
       let args =
         match args with
-          None -> []
+        | None -> []
         | Some arg -> [arg] in
       let%bind arg = simpl_tuple_expression @@ args in
-      return @@ e_constructor ~loc c_name arg
+      match c_name with
+      | "Set" -> (
+          let%bind args' =
+            trace bad_set_definition @@
+            extract_list arg in
+          return @@ e_set ~loc args'
+        )
+      | "List" -> (
+          let%bind args' =
+            trace bad_list_definition @@
+            extract_list arg in
+          return @@ e_list ~loc args'
+        )
+      | "Map" -> (
+          let%bind args' =
+            trace bad_map_definition @@
+            extract_list arg in
+          let%bind pairs =
+            trace bad_map_definition @@
+            bind_map_list extract_pair args' in
+          return @@ e_map ~loc pairs
+        )
+      | "Some" -> (
+          return @@ e_some ~loc arg
+        )
+      | _ -> (
+          return @@ e_constructor ~loc c_name arg
+        )
     )
   | EArith (Add c) ->
       simpl_binop "ADD" c
diff --git a/src/test/bin_tests.ml b/src/test/bin_tests.ml
index d54239a64..2ee1485bc 100644
--- a/src/test/bin_tests.ml
+++ b/src/test/bin_tests.ml
@@ -4,7 +4,7 @@ open Test_helpers
 
 let compile_contract_basic () : unit result =
   let%bind _ =
-    compile_contract_file "./contracts/dispatch-counter.ligo" "main" "pascaligo"
+    compile_contract_file "./contracts/dispatch-counter.ligo" "main" (Syntax_name "pascaligo")
   in
   ok ()
 
diff --git a/src/test/coase_tests.ml b/src/test/coase_tests.ml
index 2f16212d4..0db0e53f8 100644
--- a/src/test/coase_tests.ml
+++ b/src/test/coase_tests.ml
@@ -4,7 +4,7 @@ open Trace
 open Ligo.Run
 open Test_helpers
 
-let type_file = type_file "pascaligo"
+let type_file = type_file `pascaligo
 
 let get_program =
   let s = ref None in
@@ -217,7 +217,7 @@ let sell () =
       let expected_storage =
         let cards = List.hds @@ cards_ez first_owner n in
         basic 99 1000 cards (2 * n) in
-      Ast_simplified.assert_value_eq (expected_storage , storage)
+      Ast_simplified.Misc.assert_value_eq (expected_storage , storage)
     in
     let%bind () =
       let amount = Memory_proto_alpha.Alpha_context.Tez.zero in
diff --git a/src/test/heap_tests.ml b/src/test/heap_tests.ml
index a7be1fbb4..5a6f440df 100644
--- a/src/test/heap_tests.ml
+++ b/src/test/heap_tests.ml
@@ -2,7 +2,7 @@ open Trace
 open Ligo.Run
 open Test_helpers
 
-let type_file = type_file "pascaligo"
+let type_file = type_file `pascaligo
 
 let get_program =
   let s = ref None in
diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml
index 92e88ed1e..55445db99 100644
--- a/src/test/integration_tests.ml
+++ b/src/test/integration_tests.ml
@@ -4,8 +4,8 @@ open Test_helpers
 
 open Ast_simplified.Combinators
 
-let mtype_file ?debug_simplify ?debug_typed = type_file ?debug_simplify ?debug_typed "cameligo"
-let type_file = type_file "pascaligo"
+let mtype_file ?debug_simplify ?debug_typed = type_file ?debug_simplify ?debug_typed `cameligo
+let type_file = type_file `pascaligo
 
 let type_alias () : unit result =
   let%bind program = type_file "./contracts/type-alias.ligo" in
@@ -429,6 +429,16 @@ let super_counter_contract () : unit result =
     e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
   expect_eq_n program "main" make_input make_expected
 
+let super_counter_contract_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/super-counter.mligo" in
+  let make_input = fun n ->
+    let action = if n mod 2 = 0 then "Increment" else "Decrement" in
+    e_pair (e_constructor action (e_int n)) (e_int 42) in
+  let make_expected = fun n ->
+    let op = if n mod 2 = 0 then (+) else (-) in
+    e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in
+  expect_eq_n program "main" make_input make_expected
+
 let dispatch_counter_contract () : unit result =
   let%bind program = type_file "./contracts/dispatch-counter.ligo" in
   let make_input = fun n ->
@@ -566,6 +576,7 @@ let main = test_suite "Integration (End to End)" [
     test "#include directives" include_ ;
     test "counter contract" counter_contract ;
     test "super counter contract" super_counter_contract ;
+    test "super counter contract" super_counter_contract_mligo ;
     test "dispatch counter contract" dispatch_counter_contract ;
     test "closure" closure ;
     test "shared function" shared_function ;
diff --git a/src/test/test.ml b/src/test/test.ml
index e07209be2..05db3980f 100644
--- a/src/test/test.ml
+++ b/src/test/test.ml
@@ -51,6 +51,7 @@ let () =
     Typer_tests.main ;
     Heap_tests.main ;
     Coase_tests.main ;
+    Vote_tests.main ;
     Bin_tests.main ;
   ] ;
   ()
diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml
index 5817845aa..f178adcd2 100644
--- a/src/test/test_helpers.ml
+++ b/src/test/test_helpers.ml
@@ -5,7 +5,7 @@ type test =
   | Test_suite of (string * test list)
   | Test of test_case
 
-let error_pp out (e : error) =
+let rec error_pp out (e : error) =
     let open JSON_string_utils in
   let message =
     let opt = e |> member "message" |> string in
@@ -30,6 +30,7 @@ let error_pp out (e : error) =
     let infos = e |> member "infos" in
     match infos with
     | `Null -> ""
+    | `List lst -> Format.asprintf "@[<v2>%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst
     | _ -> " " ^ (J.to_string infos) ^ "\n" in
   Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos
 
@@ -70,7 +71,7 @@ let expect_eq ?options program entry_point input expected =
           Ast_simplified.PP.expression result in
       error title content in
     trace expect_error @@
-    Ast_simplified.assert_value_eq (expected , result) in
+    Ast_simplified.Misc.assert_value_eq (expected , result) in
   expect ?options program entry_point input expecter
 
 let expect_evaluate program entry_point expecter =
@@ -84,7 +85,7 @@ let expect_evaluate program entry_point expecter =
 
 let expect_eq_evaluate program entry_point expected =
   let expecter = fun result ->
-    Ast_simplified.assert_value_eq (expected , result) in
+    Ast_simplified.Misc.assert_value_eq (expected , result) in
   expect_evaluate program entry_point expecter
 
 let expect_n_aux ?options lst program entry_point make_input make_expecter =
diff --git a/src/test/vote_tests.ml b/src/test/vote_tests.ml
new file mode 100644
index 000000000..d4d1f9336
--- /dev/null
+++ b/src/test/vote_tests.ml
@@ -0,0 +1,55 @@
+open Trace
+open Ligo.Run
+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 `cameligo "./contracts/vote.mligo" in
+        s := Some program ;
+        ok program
+      )
+
+open Ast_simplified
+
+let init_storage name = ez_e_record [
+    ("title" , e_string name) ;
+    ("candidates" , e_map [
+        (e_string "Yes" , e_int 0) ;
+        (e_string "No" , e_int 0) ;
+      ]) ;
+    ("voters" , e_typed_set [] t_address) ;
+    ("beginning_time" , e_timestamp 0) ;
+    ("finish_time" , e_timestamp 1000000000) ;
+  ]
+
+let init title beginning_time finish_time =
+  let init_action = ez_e_record [
+      ("title" , e_string title) ;
+      ("beginning_time" , e_timestamp beginning_time) ;
+      ("finish_time" , e_timestamp finish_time) ;
+    ] in
+  e_constructor "Init" init_action
+
+let vote str =
+  let vote = e_string str in
+  e_constructor "Vote" vote
+
+let init_vote () =
+  let%bind program = get_program () in
+  let%bind result = Ligo.Run.run_simplityped program "main" (e_pair (vote "Yes") (init_storage "basic")) in
+  let%bind (_ , storage) = extract_pair result in
+  let%bind storage' = extract_record storage in
+  let votes = List.assoc "candidates" storage' in
+  let%bind votes' = extract_map votes in
+  let%bind (_ , yess) =
+    trace_option (simple_error "") @@
+    List.find_opt (fun (k , _) -> Ast_simplified.Misc.is_value_eq (k , e_string "Yes")) votes' in
+  let%bind () = Ast_simplified.Misc.assert_value_eq (yess , e_int 1) in
+  ok ()
+
+let main = test_suite "Vote" [
+    test "type" init_vote ;
+  ]
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 724a32b32..8dbaf60a8 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -105,6 +105,9 @@ let rec translate_type (t:AST.type_value) : type_value result =
   | T_constant ("list", [t]) ->
       let%bind t' = translate_type t in
       ok (T_list t')
+  | T_constant ("set", [t]) ->
+      let%bind t' = translate_type t in
+      ok (T_set t')
   | T_constant ("option", [o]) ->
       let%bind o' = translate_type o in
       ok (T_option o')
@@ -181,6 +184,7 @@ let rec translate_literal : AST.literal -> value = fun l -> match l with
   | Literal_bool b -> D_bool b
   | Literal_int n -> D_int n
   | Literal_nat n -> D_nat n
+  | Literal_timestamp n -> D_timestamp n
   | Literal_tez n -> D_tez n
   | Literal_bytes s -> D_bytes s
   | Literal_string s -> D_string s
@@ -362,6 +366,16 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
       let%bind (init : expression) = return @@ E_make_empty_list t in
       bind_fold_list aux init lst'
     )
+  | E_set lst -> (
+      let%bind t =
+        trace_strong (corner_case ~loc:__LOC__ "not a set") @@
+        Mini_c.Combinators.get_t_set tv in
+      let%bind lst' = bind_map_list (translate_annotated_expression) lst in
+      let aux : expression -> expression -> expression result = fun prev cur ->
+        return @@ E_constant ("CONS", [cur ; prev]) in
+      let%bind (init : expression) = return @@ E_make_empty_set t in
+      bind_fold_list aux init lst'
+    )
   | E_map m -> (
       let%bind (src, dst) =
         trace_strong (corner_case ~loc:__LOC__ "not a map") @@
@@ -663,6 +677,12 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         get_nat v in      
       return (E_literal (Literal_nat n))
     )
+  | T_constant ("timestamp", []) -> (
+      let%bind n =
+        trace_strong (wrong_mini_c_value "timestamp" v) @@
+        get_timestamp v in      
+      return (E_literal (Literal_timestamp n))
+    )
   | T_constant ("tez", []) -> (
       let%bind n =
         trace_strong (wrong_mini_c_value "tez" v) @@
@@ -712,6 +732,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
         bind_map_list aux lst in
       return (E_list lst')
     )
+  | T_constant ("set", [ty]) -> (
+      let%bind lst =
+        trace_strong (wrong_mini_c_value "set" v) @@
+        get_set v in
+      let%bind lst' =
+        let aux = fun e -> untranspile e ty in
+        bind_map_list aux lst in
+      return (E_set lst')
+    )
   | T_constant ("contract" , [_ty]) ->
     fail @@ bad_untranspile "contract" v
   | T_constant ("operation" , []) -> (
diff --git a/src/typer/typer.ml b/src/typer/typer.ml
index a3f0f0140..5c962cc10 100644
--- a/src/typer/typer.ml
+++ b/src/typer/typer.ml
@@ -206,11 +206,13 @@ module Errors = struct
     ] in
     error ~data title message ()
 
-  let constant_error loc =
+  let constant_error loc lst tv_opt =
     let title () = "typing constant" in
     let message () = "" in
     let data = [
       ("location" , fun () -> Format.asprintf "%a" Location.pp loc ) ;
+      ("argument_types" , fun () -> Format.asprintf "%a" PP_helpers.(list_sep Ast_typed.PP.type_value (const " , ")) lst) ;
+      ("type_opt" , fun () -> Format.asprintf "%a" PP_helpers.(option Ast_typed.PP.type_value) tv_opt) ;
     ] in
     error ~data title message
 end
@@ -416,6 +418,8 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
       return (E_literal (Literal_int n)) (t_int ())
   | E_literal (Literal_nat n) ->
       return (E_literal (Literal_nat n)) (t_nat ())
+  | E_literal (Literal_timestamp n) ->
+      return (E_literal (Literal_timestamp n)) (t_timestamp ())
   | E_literal (Literal_tez n) ->
       return (E_literal (Literal_tez n)) (t_tez ())
   | E_literal (Literal_address s) ->
@@ -501,6 +505,27 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
         ok (t_list ty ())
       in
       return (E_list lst') tv
+  | E_set lst ->
+      let%bind lst' = bind_map_list (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 init = match tv_opt with
+          | None -> ok None
+          | Some ty ->
+              let%bind ty' = get_t_set ty in
+              ok (Some ty') in
+        let%bind ty =
+          let%bind opt = bind_fold_list aux init
+          @@ List.map get_type_annotation lst' in
+          trace_option (needs_annotation ae "empty set") opt in
+        ok (t_set ty ())
+      in
+      return (E_set lst') tv
   | E_map lst ->
       let%bind lst' = bind_map_list (bind_map_pair (type_expression e)) lst in
       let%bind tv =
@@ -613,7 +638,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
                             ae.location)
             @@ assert_t_unit (get_type_annotation mf') in
           let mt' = make_a_e
-              (E_constant ("ASSERT" , [ex' ; fw']))
+              (E_constant ("ASSERT_INFERRED" , [ex' ; fw']))
               (t_unit ())
               e
           in
@@ -738,7 +763,7 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
   let%bind typer =
     trace_option (unrecognized_constant name loc) @@
     Map.String.find_opt name ct in
-  trace (constant_error loc) @@
+  trace (constant_error loc lst tv_opt) @@
   typer lst tv_opt
 
 let untype_type_value (t:O.type_value) : (I.type_expression) result =
@@ -752,6 +777,7 @@ let untype_literal (l:O.literal) : I.literal result =
   | Literal_unit -> ok Literal_unit
   | Literal_bool b -> ok (Literal_bool b)
   | Literal_nat n -> ok (Literal_nat n)
+  | Literal_timestamp n -> ok (Literal_timestamp n)
   | Literal_tez n -> ok (Literal_tez n)
   | Literal_int n -> ok (Literal_int n)
   | Literal_string s -> ok (Literal_string s)
@@ -803,6 +829,9 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
   | E_list lst ->
       let%bind lst' = bind_map_list untype_expression lst in
       return (e_list lst')
+  | E_set lst ->
+      let%bind lst' = bind_map_list untype_expression lst in
+      return (e_set lst')
   | E_look_up dsi ->
       let%bind (a , b) = bind_map_pair untype_expression dsi in
       return (e_look_up a b)
diff --git a/vendors/ligo-utils/tezos-utils/x_michelson.ml b/vendors/ligo-utils/tezos-utils/x_michelson.ml
index 5222abd63..462a40b63 100644
--- a/vendors/ligo-utils/tezos-utils/x_michelson.ml
+++ b/vendors/ligo-utils/tezos-utils/x_michelson.ml
@@ -47,6 +47,7 @@ let i_push_unit = i_push t_unit d_unit
 let i_push_string str = i_push t_string (string str)
 let i_none ty = prim ~children:[ty] I_NONE
 let i_nil ty = prim ~children:[ty] I_NIL
+let i_empty_set ty = prim ~children:[ty] I_EMPTY_SET
 let i_some = prim I_SOME
 let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA
 let i_empty_map src dst = prim ~children:[src;dst] I_EMPTY_MAP