diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp
index 22ece7b9950..444624851df 100644
--- a/src/goto-analyzer/taint_analysis.cpp
+++ b/src/goto-analyzer/taint_analysis.cpp
@@ -134,7 +134,8 @@ void taint_analysist::instrument(
           {
             bool match=false;
             for(const auto & i : identifiers)
-              if(has_prefix(id2string(i), "java::"+id2string(rule.function_identifier)+":"))
+              if(has_prefix(id2string(i), "java::"+id2string(rule.function_identifier)+":") ||
+                 id2string(i)==id2string(rule.function_identifier))
               {
                 match=true;
                 break;
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 128c125b649..85d85ecc5d1 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -80,7 +80,8 @@ void goto_convert_functionst::goto_convert()
        it->second.type.id()==ID_code &&
        (it->second.mode==ID_C ||
         it->second.mode==ID_cpp ||
-        it->second.mode==ID_java))
+        it->second.mode==ID_java ||
+        it->second.mode=="jsil"))
       symbol_list.push_back(it->first);
   }
   
diff --git a/src/jsil/Makefile b/src/jsil/Makefile
index 10c915844f2..e3bcb1b92ce 100644
--- a/src/jsil/Makefile
+++ b/src/jsil/Makefile
@@ -1,5 +1,5 @@
 SRC =  jsil_y.tab.cpp jsil_lex.yy.cpp \
-       jsil_convert.cpp jsil_language.cpp jsil_parse_tree.cpp \
+       jsil_convert.cpp jsil_language.cpp jsil_parse_tree.cpp jsil_types.cpp \
        jsil_parser.cpp jsil_typecheck.cpp expr2jsil.cpp \
        jsil_entry_point.cpp jsil_internal_additions.cpp
 
diff --git a/src/jsil/jsil_convert.cpp b/src/jsil/jsil_convert.cpp
index bee5d0299b1..6142c929905 100644
--- a/src/jsil/jsil_convert.cpp
+++ b/src/jsil/jsil_convert.cpp
@@ -56,6 +56,14 @@ bool jsil_convertt::operator()(const jsil_parse_treet &parse_tree)
     if(convert_code(new_symbol, to_code(new_symbol.value)))
       return true;
 
+    if(symbol_table.has_symbol(new_symbol.name))
+    {
+      symbolt &s=symbol_table.lookup(new_symbol.name);
+      if(s.value.id()=="no-body-just-yet")
+      {
+        symbol_table.remove(s.name);
+      }
+    }
     if(symbol_table.add(new_symbol))
     {
       throw "duplicate symbol "+id2string(new_symbol.name);
@@ -104,7 +112,8 @@ bool jsil_convertt::convert_code(const symbolt &symbol, codet &code)
 
       code_try_catcht t_c;
       t_c.try_code().swap(t);
-      code_declt d(symbol.symbol_expr());
+      // Adding empty symbol to catch decl
+      code_declt d(symbol_exprt("decl_symbol"));
       t_c.add_catch(d, g);
       t_c.add_source_location()=code.source_location();
 
diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp
index 00da0cf0102..9f583fbb56b 100644
--- a/src/jsil/jsil_internal_additions.cpp
+++ b/src/jsil/jsil_internal_additions.cpp
@@ -12,6 +12,8 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include <ansi-c/c_types.h>
 
+#include "jsil_types.h"
+
 #include "jsil_internal_additions.h"
 
 /*******************************************************************\
@@ -39,6 +41,8 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
     symbol.is_thread_local=true;
+    // mark as already typechecked
+    symbol.is_extern=true;
     dest.add(symbol);
   }
 
@@ -53,6 +57,8 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbol.is_lvalue=true;
     symbol.is_state_var=true;
     symbol.is_thread_local=true;
+    // mark as already typechecked
+    symbol.is_extern=true;
     dest.add(symbol);
   }
 
@@ -70,4 +76,58 @@ void jsil_internal_additions(symbol_tablet &dest)
     symbol.mode="jsil";
     dest.add(symbol);
   }
+
+  // add nan
+
+  {
+    symbolt symbol;
+    symbol.base_name="nan";
+    symbol.name="nan";
+    symbol.type=floatbv_typet();
+    symbol.mode="jsil";
+    // mark as already typechecked
+    symbol.is_extern=true;
+    dest.add(symbol);
+  }
+
+  // add empty symbol used for decl statemements
+
+  {
+    symbolt symbol;
+    symbol.base_name="decl_symbol";
+    symbol.name="decl_symbol";
+    symbol.type=empty_typet();
+    symbol.mode="jsil";
+    // mark as already typechecked
+    symbol.is_extern=true;
+    dest.add(symbol);
+  }
+
+  // add builtin objects
+  const std::vector<std::string> builtin_objects=
+  {
+    "#lg", "#lg_isNan", "#lg_isFinite", "#lop", "#lop_toString",
+    "#lop_valueOf", "#lop_isPrototypeOf", "#lfunction", "#lfp",
+    "#leval", "#lerror", "#lep", "#lrerror", "#lrep", "#lterror",
+    "#ltep", "#lserror", "#lsep", "#levalerror", "#levalerrorp",
+    "#lrangeerror", "#lrangeerrorp", "#lurierror", "#lurierrorp",
+    "#lobject", "#lobject_get_prototype_of", "#lboolean", "#lbp",
+    "#lbp_toString", "#lbp_valueOf", "#lnumber", "#lnp",
+    "#lnp_toString", "#lnp_valueOf", "#lmath", "#lstring", "#lsp",
+    "#lsp_toString", "#lsp_valueOf", "#larray", "#lap", "#ljson"
+  };
+
+  for(const auto &identifier : builtin_objects)
+  {
+    symbolt new_symbol;
+    new_symbol.name=identifier;
+    new_symbol.type=jsil_builtin_object_type();
+    new_symbol.base_name=identifier;
+    new_symbol.mode="jsil";
+    new_symbol.is_type=false;
+    new_symbol.is_lvalue=false;
+    // mark as already typechecked
+    new_symbol.is_extern=true;
+    dest.add(new_symbol);
+  }
 }
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index 58a9b315ef1..552073e4b77 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -56,6 +56,27 @@ void jsil_languaget::modules_provided(std::set<std::string> &modules)
 
 /*******************************************************************\
 
+Function: jsil_languaget::interfaces
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Adding symbols for all procedure declarations
+
+\*******************************************************************/
+
+bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
+{
+  if(jsil_convert(parse_tree, symbol_table, get_message_handler()))
+    return true;
+
+  jsil_internal_additions(symbol_table);
+  return false;
+}
+
+/*******************************************************************\
+
 Function: jsil_languaget::preprocess
 
   Inputs:
@@ -120,7 +141,7 @@ Function: jsil_languaget::typecheck
 
  Outputs:
 
- Purpose:
+ Purpose: Converting from parse tree and type checking.
 
 \*******************************************************************/
 
@@ -128,10 +149,6 @@ bool jsil_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  if(jsil_convert(parse_tree, symbol_table, get_message_handler()))
-    return true;
-
-  // now typecheck
   if(jsil_typecheck(symbol_table, get_message_handler()))
     return true;
 
@@ -152,7 +169,6 @@ Function: jsil_languaget::final
 
 bool jsil_languaget::final(symbol_tablet &symbol_table)
 {
-  jsil_internal_additions(symbol_table);
 
   if(jsil_entry_point(
       symbol_table,
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 9604777a2c2..3b9f154fb4b 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -62,6 +62,7 @@ class jsil_languaget:public languaget
   virtual std::set<std::string> extensions() const;
 
   virtual void modules_provided(std::set<std::string> &modules);
+  virtual bool interfaces(symbol_tablet &symbol_table);
 
 protected:
   jsil_parse_treet parse_tree;
diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp
index 2f394e31abf..874e36ccef6 100644
--- a/src/jsil/jsil_parse_tree.cpp
+++ b/src/jsil/jsil_parse_tree.cpp
@@ -8,6 +8,8 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include <util/symbol.h>
 
+#include "jsil_types.h"
+
 #include "jsil_parse_tree.h"
 
 /*******************************************************************\
@@ -66,10 +68,19 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
   symbol_exprt s(to_symbol_expr(
       static_cast<const exprt&>(find(ID_declarator))));
 
+  code_typet symbol_type=to_code_type(s.type());
+
+  irep_idt proc_type=s.get("proc_type");
+
+  if(proc_type=="builtin")
+    symbol_type=jsil_builtin_code_typet(symbol_type);
+  else if(proc_type=="spec")
+    symbol_type=jsil_spec_code_typet(symbol_type);
+
   symbol.name=s.get_identifier();
   symbol.base_name=s.get_identifier();
   symbol.mode="jsil";
-  symbol.type=s.type();
+  symbol.type=symbol_type;
   symbol.location=s.source_location();
 
   code_blockt code(to_code_block(
@@ -133,4 +144,3 @@ void jsil_parse_treet::output(std::ostream &out) const
     out << "\n";
   }
 }
-
diff --git a/src/jsil/jsil_parse_tree.h b/src/jsil/jsil_parse_tree.h
index 11ac901ab44..201ffb15542 100644
--- a/src/jsil/jsil_parse_tree.h
+++ b/src/jsil/jsil_parse_tree.h
@@ -29,6 +29,16 @@ class jsil_declarationt:public exprt
     add(ID_declarator, expr);
   }
 
+  const symbol_exprt &declarator() const
+  {
+    return static_cast<const symbol_exprt &>(find(ID_declarator));
+  }
+
+  symbol_exprt &declarator()
+  {
+    return static_cast<symbol_exprt &>(add(ID_declarator));
+  }
+
   void add_returns(
     const irep_idt &value,
     const irep_idt &label)
@@ -37,6 +47,16 @@ class jsil_declarationt:public exprt
     add(ID_return).set(ID_label, label);
   }
 
+  const irep_idt &returns_value() const
+  {
+    return find(ID_return).get(ID_value);
+  }
+
+  const irep_idt &returns_label() const
+  {
+    return find(ID_return).get(ID_label);
+  }
+
   void add_throws(
     const irep_idt &value,
     const irep_idt &label)
@@ -45,11 +65,31 @@ class jsil_declarationt:public exprt
     add(ID_throw).set(ID_label, label);
   }
 
+  const irep_idt &throws_value() const
+  {
+    return find(ID_throw).get(ID_value);
+  }
+
+  const irep_idt &throws_label() const
+  {
+    return find(ID_throw).get(ID_label);
+  }
+
   void add_value(const code_blockt &code)
   {
     add(ID_value, code);
   }
 
+  const code_blockt &value() const
+  {
+    return static_cast<const code_blockt &>(find(ID_value));
+  }
+
+  code_blockt &value()
+  {
+    return static_cast<code_blockt &>(add(ID_value));
+  }
+
   void to_symbol(symbolt &symbol) const;
 
   void output(std::ostream &) const;
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index f0a26a988ec..ee251f93f93 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -7,8 +7,11 @@ Author: Michael Tautschnig, tautschn@amazon.com
 \*******************************************************************/
 
 #include <util/symbol_table.h>
+#include <util/prefix.h>
+#include <util/std_expr.h>
 
 #include "expr2jsil.h"
+#include "jsil_types.h"
 
 #include "jsil_typecheck.h"
 
@@ -48,7 +51,707 @@ std::string jsil_typecheckt::to_string(const typet &type)
 
 /*******************************************************************\
 
-Function: java_bytecode_typecheckt::typecheck_non_type_symbol
+Function: jsil_typecheckt::add_prefix
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Prefix parameters and variables with a procedure name
+
+\*******************************************************************/
+
+irep_idt jsil_typecheckt::add_prefix(const irep_idt &ds)
+{
+  return id2string(proc_name) + "::" + id2string(ds);
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::update_expr_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::update_expr_type(exprt &expr, const typet &type)
+{
+  expr.type()=type;
+
+  if(expr.id()==ID_symbol)
+  {
+    const irep_idt &id=to_symbol_expr(expr).get_identifier();
+
+    if(!symbol_table.has_symbol(id))
+      throw "Unexpected symbol: "+id2string(id);
+
+    symbolt &s=symbol_table.lookup(id);
+    if(s.type.id().empty() || s.type.is_nil())
+      s.type=type;
+    else
+      s.type=jsil_union(s.type, type);
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::make_type_compatible
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::make_type_compatible(
+    exprt &expr,
+    const typet &type,
+    bool must)
+{
+  if(type.id().empty() || type.is_nil())
+  {
+    err_location(expr);
+    str << "make_type_compatible got empty type: " << expr.pretty();
+    throw 0;
+  }
+
+  if(expr.type().id().empty() || expr.type().is_nil())
+  {
+    // Type is not yet set
+    update_expr_type(expr, type);
+    return;
+  }
+
+  if(must)
+  {
+    if(jsil_incompatible_types(expr.type(), type))
+    {
+      err_location(expr);
+      str << "failed to typecheck expr "
+          << expr.pretty() << " with type "
+          << expr.type().pretty()
+          << "; required type " << type.pretty();
+      throw 0;
+    }
+  }
+  else if(!jsil_is_subtype(type, expr.type()))
+  {
+    // Types are not compatible
+    typet upper=jsil_union(expr.type(), type);
+    update_expr_type(expr, upper);
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_type(typet &type)
+{
+  if(type.id()==ID_code)
+  {
+    code_typet &parameters=to_code_type(type);
+
+    for(code_typet::parametert &p : parameters.parameters())
+    {
+      // create new symbol
+      parameter_symbolt new_symbol;
+      new_symbol.base_name=p.get_identifier();
+
+      // append procedure name to parameters
+      p.set_identifier(add_prefix(p.get_identifier()));
+      new_symbol.name=p.get_identifier();
+
+      if(is_jsil_builtin_code_type(type))
+        new_symbol.type=jsil_value_or_empty_type();
+      else if(is_jsil_spec_code_type(type))
+        new_symbol.type=jsil_value_or_reference_type();
+      else
+        new_symbol.type=jsil_value_type(); // User defined function
+
+      new_symbol.mode="jsil";
+
+      // mark as already typechecked
+      new_symbol.is_extern=true;
+
+      if(symbol_table.add(new_symbol))
+      {
+        str << "failed to add parameter symbol `"
+            << new_symbol.name << "' in the symbol table";
+        throw 0;
+      }
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr(exprt &expr)
+{
+  // first do sub-nodes
+  typecheck_expr_operands(expr);
+
+  // now do case-split
+  typecheck_expr_main(expr);
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_expr_operands
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_operands(exprt &expr)
+{
+  Forall_operands(it, expr)
+    typecheck_expr(*it);
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_expr_main
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_main(exprt &expr)
+{
+  if(expr.id()==ID_code)
+  {
+    err_location(expr);
+    str << "typecheck_expr_main got code: " << expr.pretty();
+    throw 0;
+  }
+  else if(expr.id()==ID_symbol)
+    typecheck_symbol_expr(to_symbol_expr (expr));
+  else if(expr.id()==ID_constant)
+  {
+  }
+  else
+  {
+    // expressions are expected not to have type set just yet
+    assert(expr.type().is_nil()||expr.type().id().empty());
+
+    if (expr.id()==ID_null ||
+        expr.id()=="undefined" ||
+        expr.id()==ID_empty)
+      typecheck_expr_constant(expr);
+    else if(expr.id()=="null_type" ||
+            expr.id()=="undefined_type" ||
+            expr.id()==ID_boolean ||
+            expr.id()==ID_string ||
+            expr.id()=="number" ||
+            expr.id()=="builtin_object" ||
+            expr.id()=="user_object" ||
+            expr.id()=="object" ||
+            expr.id()==ID_reference ||
+            expr.id()==ID_member ||
+            expr.id()=="variable")
+      expr.type()=jsil_kind();
+    else if(expr.id()=="proto" ||
+            expr.id()=="fid" ||
+            expr.id()=="scope" ||
+            expr.id()=="constructid" ||
+            expr.id()=="primvalue" ||
+            expr.id()=="targetfunction" ||
+            expr.id()==ID_class)
+    {
+      // TODO: have a special type for builtin fields
+      expr.type()=string_typet();
+    }
+    else if(expr.id()==ID_not)
+      typecheck_expr_unary_boolean(expr);
+    else if(expr.id()=="string_to_num")
+      typecheck_expr_unary_string(expr);
+    else if(expr.id()==ID_unary_minus ||
+            expr.id()=="num_to_int32" ||
+            expr.id()=="num_to_uint32" ||
+            expr.id()==ID_bitnot)
+    {
+      typecheck_expr_unary_num(expr);
+      expr.type()=floatbv_typet();
+    }
+    else if(expr.id()=="num_to_string") {
+      typecheck_expr_unary_num(expr);
+      expr.type()=string_typet();
+    }
+    else if(expr.id()==ID_equal)
+      typecheck_exp_binary_equal(expr);
+    else if(expr.id()==ID_lt ||
+            expr.id()==ID_le)
+      typecheck_expr_binary_compare(expr);
+    else if(expr.id()==ID_plus ||
+            expr.id()==ID_minus ||
+            expr.id()==ID_mult ||
+            expr.id()==ID_div ||
+            expr.id()==ID_mod ||
+            expr.id()==ID_bitand ||
+            expr.id()==ID_bitor ||
+            expr.id()==ID_bitxor ||
+            expr.id()==ID_shl ||
+            expr.id()==ID_shr ||
+            expr.id()==ID_lshr)
+      typecheck_expr_binary_arith(expr);
+    else if(expr.id()==ID_and ||
+            expr.id()==ID_or)
+      typecheck_expr_binary_boolean(expr);
+    else if(expr.id()=="subtype_of")
+      typecheck_expr_subtype(expr);
+    else if(expr.id()==ID_concatenation)
+      typecheck_expr_concatenation(expr);
+    else if(expr.id()=="ref")
+      typecheck_expr_ref(expr);
+    else if(expr.id()=="field")
+      typecheck_expr_field(expr);
+    else if(expr.id()==ID_base)
+      typecheck_expr_base(expr);
+    else if(expr.id()==ID_typeof)
+      expr.type()=jsil_kind();
+    else if(expr.id()=="new")
+      expr.type()=jsil_user_object_type();
+    else if(expr.id()=="hasField")
+      typecheck_expr_has_field(expr);
+    else if(expr.id()==ID_index)
+      typecheck_expr_index(expr);
+    else if(expr.id()=="delete")
+      typecheck_expr_delete(expr);
+    else if(expr.id()=="protoField")
+      typecheck_expr_proto_field(expr);
+    else if(expr.id()=="protoObj")
+      typecheck_expr_proto_obj(expr);
+    else if(expr.id()==ID_side_effect)
+      typecheck_expr_side_effect_throw(to_side_effect_expr_throw(expr));
+    else
+    {
+      err_location(expr);
+      str << "unexpected expression: " << expr.pretty();
+      throw 0;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_expr_side_effect_throw
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_side_effect_throw(
+  side_effect_expr_throwt &expr)
+{
+  irept &excep_list=expr.add(ID_exception_list);
+  assert(excep_list.id()==ID_symbol);
+  symbol_exprt &s=static_cast<symbol_exprt &>(excep_list);
+  typecheck_symbol_expr(s);
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_expr_constant
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_constant(exprt &expr)
+{
+  if(expr.id()==ID_null)
+    expr.type()=jsil_null_type();
+  else if(expr.id()=="undefined")
+    expr.type()=jsil_undefined_type();
+  else if(expr.id()==ID_empty)
+    expr.type()=jsil_empty_type();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_proto_field
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_proto_field(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_object_type(), true);
+  make_type_compatible(expr.op1(), string_typet(), true);
+
+  expr.type()=jsil_value_or_empty_type();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_proto_field
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_proto_obj(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_object_type(), true);
+  make_type_compatible(expr.op1(), jsil_object_type(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_delete
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_delete(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_object_type(), true);
+  make_type_compatible(expr.op1(), string_typet(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_hasfield
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_index(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_object_type(), true);
+  make_type_compatible(expr.op1(), string_typet(), true);
+
+  // special case for function identifiers
+  if (expr.op1().id()=="fid" || expr.op1().id()=="constructid")
+    expr.type()=code_typet();
+  else
+    expr.type()=jsil_value_type();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_hasfield
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_has_field(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_object_type(), true);
+  make_type_compatible(expr.op1(), string_typet(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_field
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_field(exprt &expr)
+{
+  if(expr.operands().size()!=1)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects single operand";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_reference_type(), true);
+
+  expr.type()=string_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_base
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_base(exprt &expr)
+{
+  if(expr.operands().size()!=1)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects single operand";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_reference_type(), true);
+
+  expr.type()=jsil_value_type();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_ref
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_ref(exprt &expr)
+{
+  if(expr.operands().size()!=3)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects three operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_value_type(), true);
+  make_type_compatible(expr.op1(), string_typet(), true);
+
+  exprt &operand3=expr.op2();
+  make_type_compatible(operand3, jsil_kind(), true);
+
+  if(operand3.id()==ID_member)
+    expr.type()=jsil_member_reference_type();
+  else if(operand3.id()=="variable")
+    expr.type()=jsil_variable_reference_type();
+  else
+  {
+    err_location(expr);
+    str << "operator `" << expr.id()
+        << "' expects reference type in the third parameter. Got:"
+        << operand3.pretty();
+    throw 0;
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_concatenation
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_concatenation(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), string_typet(), true);
+  make_type_compatible(expr.op1(), string_typet(), true);
+
+  expr.type()=string_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_subtype
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_subtype(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), jsil_kind(), true);
+  make_type_compatible(expr.op1(), jsil_kind(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_binary_boolean
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_binary_boolean(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), bool_typet(), true);
+  make_type_compatible(expr.op1(), bool_typet(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_binary_arith
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_binary_arith(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+
+  make_type_compatible(expr.op0(), floatbv_typet(), true);
+  make_type_compatible(expr.op1(), floatbv_typet(), true);
+
+  expr.type()=floatbv_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_exp_binary_equal
 
   Inputs:
 
@@ -58,11 +761,514 @@ Function: java_bytecode_typecheckt::typecheck_non_type_symbol
 
 \*******************************************************************/
 
+void jsil_typecheckt::typecheck_exp_binary_equal(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+ // operands can be of any types
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_binary_compare
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_binary_compare(exprt &expr)
+{
+  if(expr.operands().size()!=2)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects two operands";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), floatbv_typet(), true);
+  make_type_compatible(expr.op1(), floatbv_typet(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_unary_boolean
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_unary_boolean(exprt &expr)
+{
+  if(expr.operands().size()!=1)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects one operand";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), bool_typet(), true);
+
+  expr.type()=bool_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_unary_string
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_unary_string(exprt &expr)
+{
+  if(expr.operands().size()!=1)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects one operand";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), string_typet(), true);
+
+  expr.type()=floatbv_typet();
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheck_baset::typecheck_expr_unary_num
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_expr_unary_num(exprt &expr)
+{
+  if(expr.operands().size()!=1)
+  {
+    err_location(expr);
+    str << "operator `" << expr.id() << "' expects one operand";
+    throw 0;
+  }
+
+  make_type_compatible(expr.op0(), floatbv_typet(), true);
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_symbol_expr
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_symbol_expr(symbol_exprt &symbol_expr)
+{
+  irep_idt identifier=symbol_expr.get_identifier();
+
+  // if this is a built-in identifier, check if it exists in the
+  // symbol table and retrieve it's type
+  // TODO: add a flag for not needing to prefix internal symbols
+  // that do not start with hash
+  if(has_prefix(id2string(identifier), "#") ||
+     identifier=="eval" ||
+     identifier=="nan")
+  {
+    symbol_tablet::symbolst::const_iterator s_it=
+      symbol_table.symbols.find(identifier);
+
+    if(s_it==symbol_table.symbols.end())
+      throw "unexpected internal symbol: "+id2string(identifier);
+    else
+    {
+      // symbol already exists
+      const symbolt &symbol=s_it->second;
+
+      // type the expression
+      symbol_expr.type()=symbol.type;
+    }
+  }
+  else
+  {
+    // if this is a variable, we need to check if we already
+    // prefixed it and add to the symbol table if it is not there already
+    irep_idt identifier_base = identifier;
+    if(!has_prefix(id2string(identifier), id2string(proc_name)))
+    {
+      identifier = add_prefix(identifier);
+      symbol_expr.set_identifier(identifier);
+    }
+
+    symbol_tablet::symbolst::const_iterator s_it=
+    symbol_table.symbols.find(identifier);
+
+    if(s_it==symbol_table.symbols.end())
+    {
+      // create new symbol
+      symbolt new_symbol;
+      new_symbol.name=identifier;
+      new_symbol.type=symbol_expr.type();
+      new_symbol.base_name=identifier_base;
+      new_symbol.mode="jsil";
+      new_symbol.is_type=false;
+      new_symbol.is_lvalue=new_symbol.type.id()!=ID_code;
+
+      // mark as already typechecked
+      new_symbol.is_extern=true;
+
+      if(symbol_table.add(new_symbol))
+      {
+        str << "failed to add symbol `"
+            << new_symbol.name << "' in the symbol table";
+        throw 0;
+      }
+    }
+    else
+    {
+      // symbol already exists
+      assert(!s_it->second.is_type);
+
+      const symbolt &symbol=s_it->second;
+
+      // type the expression
+      symbol_expr.type()=symbol.type;
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_code
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_code(codet &code)
+{
+  const irep_idt &statement=code.get_statement();
+
+  if(statement==ID_function_call)
+    typecheck_function_call(to_code_function_call(code));
+  else if(statement==ID_return)
+    typecheck_return(to_code_return(code));
+  else if(statement==ID_expression)
+  {
+    if(code.operands().size()!=1)
+      throw "expression statement expected to have one operand";
+
+    typecheck_expr(code.op0());
+  }
+  else if(statement==ID_label)
+  {
+    typecheck_code(to_code_label(code).code());
+    // TODO: produce defined label set
+  }
+  else if(statement==ID_block)
+    typecheck_block(code);
+  else if(statement==ID_ifthenelse)
+    typecheck_ifthenelse(to_code_ifthenelse(code));
+  else if(statement==ID_goto)
+  {
+    // TODO: produce used label set
+  }
+  else if(statement==ID_assign)
+    typecheck_assign(to_code_assign(code));
+  else if(statement==ID_try_catch)
+    typecheck_try_catch(to_code_try_catch(code));
+  else if(statement==ID_skip)
+  {
+  }
+  else
+  {
+    err_location(code);
+    str << "unexpected statement: " << statement;
+    throw 0;
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_return
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_return(code_returnt &code)
+{
+  if(code.has_return_value())
+    typecheck_expr(code.return_value());
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_block
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_block(codet &code)
+{
+  Forall_operands(it, code)
+    typecheck_code(to_code(*it));
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_try_catch
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_try_catch(code_try_catcht &code)
+{
+  // A special case of try catch with one catch clause
+  if(code.operands().size()!=3)
+    throw "try_catch expected to have three operands";
+
+  // function call
+  typecheck_function_call(to_code_function_call(code.try_code()));
+
+  // catch decl is not used, but is required by goto-programs
+
+  typecheck_code(code.get_catch_code(0));
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_function_call
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_function_call(
+  code_function_callt &call)
+{
+  if(call.operands().size()!=3)
+    throw "function call expected to have three operands";
+
+  exprt &lhs=call.lhs();
+  typecheck_expr(lhs);
+
+  exprt &f=call.function();
+  typecheck_expr(f);
+
+  for(auto &arg : call.arguments())
+    typecheck_expr(arg);
+
+  // Look for a function declaration symbol in the symbol table
+  if(f.id()==ID_symbol)
+  {
+    const irep_idt &id=to_symbol_expr(f).get_identifier();
+
+    if(symbol_table.has_symbol(id))
+    {
+      symbolt &s=symbol_table.lookup(id);
+
+      if(s.type.id()==ID_code)
+      {
+        code_typet &codet=to_code_type(s.type);
+
+        for (int i=0; i<codet.parameters().size(); i++)
+        {
+          if(i>=call.arguments().size()) break;
+
+          const typet &param_type=codet.parameters()[i].type();
+
+          if(!param_type.id().empty() && param_type.is_not_nil())
+          {
+             // check argument's type if parameter's type is given
+             make_type_compatible(call.arguments()[i], param_type, true);
+          }
+        }
+
+        // if there are too few arguments, add undefined
+        if(codet.parameters().size()>call.arguments().size())
+        {
+          for(int i=call.arguments().size();
+                  i<codet.parameters().size();
+                  i++)
+            call.arguments().push_back(
+              exprt("undefined", jsil_undefined_type()));
+        }
+
+        // if there are too many arguments, remove
+        while(codet.parameters().size()<call.arguments().size())
+          call.arguments().pop_back();
+
+        // check return type if exists
+        if(!codet.return_type().id().empty() &&
+            codet.return_type().is_not_nil())
+          make_type_compatible(lhs, codet.return_type(), true);
+        else make_type_compatible(lhs, jsil_any_type(), true);
+      }
+      else
+      {
+        // TODO: a symbol can be a variable evaluating to a string
+        // which corresponds to a function identifier
+        make_type_compatible(lhs, jsil_any_type(), true);
+      }
+    }
+    else
+    {
+      // Should be function, declaration not found yet
+      symbolt new_symbol;
+      new_symbol.name=id;
+      new_symbol.type=code_typet();
+      new_symbol.mode="jsil";
+      new_symbol.is_type=false;
+      new_symbol.value=exprt("no-body-just-yet");
+
+      make_type_compatible(lhs, jsil_any_type(), true);
+
+      if(symbol_table.add(new_symbol))
+        throw "failed to add expression symbol to symbol table";
+    }
+  }
+  else
+  {
+    // TODO: this might be a string literal
+    // which corresponds to a function identifier
+    make_type_compatible(lhs, jsil_any_type(), true);
+  }
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_ifthenelse
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_ifthenelse(code_ifthenelset &code)
+{
+  exprt &cond=code.cond();
+  typecheck_expr(cond);
+  make_type_compatible(cond, bool_typet(), true);
+
+  typecheck_code(to_code(code.then_case()));
+
+  if(!code.else_case().is_nil())
+    typecheck_code(to_code(code.else_case()));
+}
+
+/*******************************************************************\
+
+Function: jsil_typecheckt::typecheck_assign
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void jsil_typecheckt::typecheck_assign(code_assignt &code)
+{
+  typecheck_expr(code.op0());
+  typecheck_expr(code.op1());
+
+  make_type_compatible(code.op0(), code.op1().type(), false);
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_typecheckt::typecheck_non_type_symbol
+
+  Inputs: any symbol
+
+ Outputs:
+
+ Purpose: typecheking procedure declaration; any other symbols
+  should have been typechecked during typecheking of procedure
+  declaration
+
+\*******************************************************************/
+
 void jsil_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
 {
   assert(!symbol.is_type);
+
+  // Using is_extern to check if symbol was already typechecked
+  if(symbol.is_extern)
+    return;
+  if(symbol.value.id()!="no-body-just-yet")
+    symbol.is_extern=true;
+
+  proc_name=symbol.name;
   typecheck_type(symbol.type);
-  typecheck_expr(symbol.value);
+
+  if(symbol.value.id()==ID_code)
+    typecheck_code(to_code(symbol.value));
+  else if(symbol.name=="eval")
+  {
+    // No code for eval. Do nothing
+  }
+  else if(symbol.value.id()=="no-body-just-yet")
+  {
+    // Do nothing
+  }
+  else
+    throw "Non type symbol value expected code, but got "+
+      symbol.value.pretty();
 }
 
 /*******************************************************************\
diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h
index 8768781525e..ca6051418d5 100644
--- a/src/jsil/jsil_typecheck.h
+++ b/src/jsil/jsil_typecheck.h
@@ -11,6 +11,8 @@ Author: Michael Tautschnig, tautschn@amazon.com
 
 #include <util/typecheck.h>
 #include <util/namespace.h>
+#include <util/std_code.h>
+
 
 class codet;
 
@@ -31,29 +33,57 @@ class jsil_typecheckt:public legacy_typecheckt
     message_handlert &_message_handler):
     legacy_typecheckt(_message_handler),
     symbol_table(_symbol_table),
-    ns(symbol_table)
+    ns(symbol_table),
+    proc_name()
   {
   }
 
   virtual ~jsil_typecheckt() { }
 
   virtual void typecheck();
-  virtual void typecheck_expr(exprt &expr) {};
+  virtual void typecheck_expr(exprt &expr);
 
 protected:
   symbol_tablet &symbol_table;
   const namespacet ns;
+  // prefix to variables which is set in typecheck_declaration
+  irep_idt proc_name;
 
+  void update_expr_type (exprt &expr, const typet &type);
+  void make_type_compatible(exprt &expr, const typet &type, bool must);
   void typecheck_type_symbol(symbolt &symbol) {};
   void typecheck_non_type_symbol(symbolt &symbol);
+  void typecheck_symbol_expr(symbol_exprt &symbol_expr);
+  void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr);
+  void typecheck_expr_delete(exprt &expr);
+  void typecheck_expr_index(exprt &expr);
+  void typecheck_expr_proto_field(exprt &expr);
+  void typecheck_expr_proto_obj(exprt &expr);
+  void typecheck_expr_has_field(exprt &expr);
+  void typecheck_expr_ref(exprt &expr);
+  void typecheck_expr_field(exprt &expr);
+  void typecheck_expr_base(exprt &expr);
+  void typecheck_expr_constant(exprt &expr);
+  void typecheck_expr_concatenation(exprt &expr);
+  void typecheck_expr_subtype(exprt &expr);
+  void typecheck_expr_binary_boolean(exprt &expr);
+  void typecheck_expr_binary_arith(exprt &expr);
+  void typecheck_exp_binary_equal(exprt &expr);
+  void typecheck_expr_binary_compare(exprt &expr);
+  void typecheck_expr_unary_boolean(exprt &expr);
+  void typecheck_expr_unary_string(exprt &expr);
+  void typecheck_expr_unary_num(exprt &expr);
+  void typecheck_expr_operands(exprt &expr);
+  void typecheck_expr_main(exprt &expr);
   void typecheck_code(codet &code);
-  void typecheck_type(typet &type) {};
-#if 0
-  void typecheck_expr_symbol(symbol_exprt &expr);
-  void typecheck_expr_member(member_exprt &expr);
-  void typecheck_expr_java_new(side_effect_exprt &expr);
-  void typecheck_expr_java_new_array(side_effect_exprt &expr);
-#endif
+  void typecheck_function_call(code_function_callt &function_call);
+  void typecheck_return(code_returnt &code);
+  void typecheck_block(codet &code);
+  void typecheck_ifthenelse(code_ifthenelset &code);
+  void typecheck_assign(code_assignt &code);
+  void typecheck_try_catch (code_try_catcht &code);
+  void typecheck_type(typet &type);
+  irep_idt add_prefix(const irep_idt &ds);
 
   // overload to use language-specific syntax
   virtual std::string to_string(const exprt &expr);
@@ -63,4 +93,3 @@ class jsil_typecheckt:public legacy_typecheckt
 };
 
 #endif
-
diff --git a/src/jsil/jsil_types.cpp b/src/jsil/jsil_types.cpp
new file mode 100644
index 00000000000..c9d96f4d64b
--- /dev/null
+++ b/src/jsil/jsil_types.cpp
@@ -0,0 +1,526 @@
+/*******************************************************************\
+
+Module: Jsil Language
+
+Author: Daiva Naudziuniene, daivan@amazon.com
+
+\*******************************************************************/
+
+#include <algorithm>
+
+#include "jsil_types.h"
+
+/*******************************************************************\
+
+Function: jsil_any_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_any_type()
+{
+  return jsil_union_typet({
+                          jsil_empty_type(),
+                          jsil_reference_type(),
+                          jsil_value_type()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_value_or_empty_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_value_or_empty_type()
+{
+  return jsil_union_typet({
+                          jsil_value_type(),
+                          jsil_empty_type()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_value_or_reference_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_value_or_reference_type()
+{
+  return jsil_union_typet({
+                          jsil_value_type(),
+                          jsil_reference_type()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_value_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_value_type()
+{
+  return jsil_union_typet({
+                          jsil_undefined_type(),
+                          jsil_null_type(),
+                          jsil_prim_type(),
+                          jsil_object_type()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_prim_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_prim_type()
+{
+  return jsil_union_typet({
+                          floatbv_typet(),
+                          string_typet(),
+                          bool_typet()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_reference_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_reference_type()
+{
+  return jsil_union_typet({
+                          jsil_member_reference_type(),
+                          jsil_variable_reference_type()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_member_reference_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_member_reference_type()
+{
+  return typet("jsil_member_reference_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_variable_reference_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_variable_reference_type()
+{
+  return typet("jsil_variable_reference_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_object_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_object_type()
+{
+  return jsil_union_typet({
+                          jsil_user_object_type(),
+                          jsil_builtin_object_type()
+                          });
+}
+
+/*******************************************************************\
+
+Function: jsil_user_object_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_user_object_type()
+{
+  return typet("jsil_user_object_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_builtin_object_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_builtin_object_type()
+{
+  return typet("jsil_builtin_object_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_null_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_null_type()
+{
+  return typet("jsil_null_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_undefined_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_undefined_type()
+{
+  return typet("jsil_undefined_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_kind
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_kind()
+{
+  return typet("jsil_kind");
+}
+
+/*******************************************************************\
+
+Function: jsil_empty_type
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_empty_type()
+{
+  return typet("jsil_empty_type");
+}
+
+/*******************************************************************\
+
+Function: jsil_is_subtype
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool jsil_is_subtype(const typet &type1, const typet &type2)
+{
+  if(type2.id()==ID_union)
+  {
+    const jsil_union_typet &type2_union=to_jsil_union_type(type2);
+
+    if(type1.id()==ID_union)
+      return to_jsil_union_type(type1).is_subtype(type2_union);
+    else
+      return jsil_union_typet(type1).is_subtype(type2_union);
+  }
+  else
+    return type1.id()==type2.id();
+}
+
+/*******************************************************************\
+
+Function: jsil_incompatible_types
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool jsil_incompatible_types(const typet &type1, const typet &type2)
+{
+  return jsil_union_typet(type1).intersect_with(
+    jsil_union_typet(type2)).components().empty();
+}
+
+/*******************************************************************\
+
+Function: jsil_union
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet jsil_union(const typet &type1, const typet &type2)
+{
+  return jsil_union_typet(type1)
+    .union_with(jsil_union_typet(type2)).to_type();
+}
+
+/*******************************************************************\
+
+Function: compare_components
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool compare_components(
+  const union_typet::componentt &comp1,
+  const union_typet::componentt &comp2)
+{
+  return comp1.type().id()<comp2.type().id();
+}
+
+/*******************************************************************\
+
+Function: jsil_union_typet::jsil_union_typet
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+jsil_union_typet::jsil_union_typet(const std::vector<typet> &types):
+    union_typet()
+{
+  auto &elements=components();
+  for(const auto &type : types)
+  {
+    if(type.id()==ID_union)
+    {
+      for(const auto &component : to_union_type(type).components())
+        elements.push_back(component);
+    }
+    else
+      elements.push_back(componentt(ID_anonymous, type));
+  }
+
+  std::sort(elements.begin(), elements.end(), compare_components);
+}
+
+/*******************************************************************\
+
+Function: jsil_union_typet::union_with
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+jsil_union_typet jsil_union_typet::union_with(
+    const jsil_union_typet &other) const
+{
+  auto &elements1=components();
+  auto &elements2=other.components();
+  jsil_union_typet result;
+  auto &elements=result.components();
+  elements.resize(elements1.size()+elements2.size());
+  std::vector<union_typet::componentt>::iterator it=std::set_union(
+    elements1.begin(), elements1.end(),
+    elements2.begin(), elements2.end(),
+    elements.begin(), compare_components);
+  elements.resize(it-elements.begin());
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: jsil_union_typet::intersect_with
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+jsil_union_typet jsil_union_typet::intersect_with(
+    const jsil_union_typet &other) const
+{
+  auto &elements1=components();
+  auto &elements2=other.components();
+  jsil_union_typet result;
+  auto &elements=result.components();
+  elements.resize(std::min(elements1.size(),elements2.size()));
+  std::vector<union_typet::componentt>::iterator it=std::set_intersection(
+    elements1.begin(), elements1.end(),
+    elements2.begin(), elements2.end(),
+    elements.begin(), compare_components);
+  elements.resize(it-elements.begin());
+
+  return result;
+}
+
+/*******************************************************************\
+
+Function: jsil_union_typet::is_subtype
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bool jsil_union_typet::is_subtype(const jsil_union_typet &other) const
+{
+  auto it=components().begin();
+  auto it2=other.components().begin();
+  while(it<components().end())
+  {
+    if(it2>=other.components().end())
+    {
+      // We haven't found all types, but the second array finishes
+      return false;
+    }
+
+    if(it->type().id()==it2->type().id())
+    {
+      // Found the type
+      it++;
+      it2++;
+    }
+    else if(it->type().id()<it2->type().id())
+    {
+      // Missing type
+      return false;
+    }
+    else // it->type().id()>it2->type().id()
+    {
+      // Skip one element in the second array
+      it2++;
+    }
+  }
+
+  return true;
+}
+
+/*******************************************************************\
+
+Function: jsil_union_typet::to_type()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+const typet& jsil_union_typet::to_type() const
+{
+  auto &elements=components();
+  if(elements.size()==1)
+    return elements[0].type();
+
+  return *this;
+}
diff --git a/src/jsil/jsil_types.h b/src/jsil/jsil_types.h
new file mode 100644
index 00000000000..57950ef340e
--- /dev/null
+++ b/src/jsil/jsil_types.h
@@ -0,0 +1,113 @@
+/*******************************************************************\
+
+Module: Jsil Language
+
+Author: Daiva Naudziuniene, daivan@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_JSIL_TYPES_H
+#define CPROVER_JSIL_TYPES_H
+
+#include <util/type.h>
+#include <util/std_types.h>
+
+typet jsil_kind();
+typet jsil_any_type();
+typet jsil_value_or_empty_type();
+typet jsil_value_or_reference_type();
+typet jsil_value_type();
+typet jsil_prim_type();
+typet jsil_reference_type();
+typet jsil_member_reference_type();
+typet jsil_variable_reference_type();
+typet jsil_object_type();
+typet jsil_user_object_type();
+typet jsil_builtin_object_type();
+typet jsil_null_type();
+typet jsil_undefined_type();
+typet jsil_empty_type();
+
+bool jsil_is_subtype(const typet &type1, const typet &type2);
+bool jsil_incompatible_types(const typet &type1, const typet &type2);
+typet jsil_union(const typet &type1, const typet &type2);
+
+class jsil_builtin_code_typet:public code_typet
+{
+public:
+  explicit inline jsil_builtin_code_typet(code_typet &code):
+    code_typet(code)
+  {
+    set("jsil_builtin_proceduret", true);
+  }
+};
+
+extern inline jsil_builtin_code_typet &to_jsil_builtin_code_type(
+  code_typet &code)
+{
+  assert(code.get_bool("jsil_builtin_proceduret"));
+  return static_cast<jsil_builtin_code_typet &>(code);
+}
+
+extern inline bool is_jsil_builtin_code_type(const typet &type)
+{
+  return type.id()==ID_code &&
+         type.get_bool("jsil_builtin_proceduret");
+}
+
+class jsil_spec_code_typet:public code_typet
+{
+public:
+  explicit inline jsil_spec_code_typet(code_typet &code):
+    code_typet(code)
+  {
+    set("jsil_spec_proceduret", true);
+  }
+};
+
+extern inline jsil_spec_code_typet &to_jsil_spec_code_type(
+  code_typet &code)
+{
+  assert(code.get_bool("jsil_spec_proceduret"));
+  return static_cast<jsil_spec_code_typet &>(code);
+}
+
+extern inline bool is_jsil_spec_code_type(const typet &type)
+{
+  return type.id()==ID_code &&
+         type.get_bool("jsil_spec_proceduret");
+}
+
+class jsil_union_typet:public union_typet
+{
+public:
+  inline jsil_union_typet():union_typet() { }
+
+  explicit inline jsil_union_typet(const typet &type)
+    :jsil_union_typet(std::vector<typet>({type})) { }
+
+  explicit jsil_union_typet(const std::vector<typet> &types);
+
+  jsil_union_typet union_with(const jsil_union_typet &other) const;
+
+  jsil_union_typet intersect_with(const jsil_union_typet &other) const;
+
+  bool is_subtype(const jsil_union_typet &other) const;
+
+  const typet& to_type() const;
+};
+
+extern inline jsil_union_typet &to_jsil_union_type(typet &type)
+{
+  assert(type.id()==ID_union);
+  return static_cast<jsil_union_typet &>(type);
+}
+
+extern inline const jsil_union_typet &to_jsil_union_type(
+  const typet &type)
+{
+  assert(type.id()==ID_union);
+  return static_cast<const jsil_union_typet &>(type);
+}
+
+#endif
diff --git a/src/jsil/parser.y b/src/jsil/parser.y
index dd6c6901be8..9581c944e9d 100644
--- a/src/jsil/parser.y
+++ b/src/jsil/parser.y
@@ -153,7 +153,13 @@ proc_ident: TOK_IDENTIFIER
             newstack($$).swap(e);
           }
           | TOK_BUILTIN_IDENTIFIER
+          {
+            stack($$).set("proc_type", "builtin");
+          }
           | TOK_SPEC_IDENTIFIER
+          {
+            stack($$).set("proc_type", "spec");
+          }
           ;
 
 proc_ident_expr: proc_ident
@@ -417,6 +423,11 @@ literal: TOK_IDENTIFIER
        }
        | TOK_FLOATING
        | TOK_STRING
+       {
+         constant_exprt c(to_string_constant(stack($$))
+           .get_value(), string_typet());
+         stack($$).swap(c);
+       }
        | TOK_BUILTIN_LOC
        | jsil_type
        | builtin_field
@@ -518,11 +529,11 @@ bitwise_op: '&'
           }
           | '|'
           {
-            newstack($$).id(ID_or);
+            newstack($$).id(ID_bitor);
           }
           | '^'
           {
-            newstack($$).id(ID_xor);
+            newstack($$).id(ID_bitxor);
           }
           | TOK_LEFT_SHIFT
           {
@@ -570,11 +581,11 @@ unary_op: TOK_NOT
 
 jsil_type: TOK_T_NULL
          {
-           newstack($$).id(ID_null);
+           newstack($$).id("null_type");
          }
          | TOK_T_UNDEFINED
          {
-           newstack($$).id("undefined");
+           newstack($$).id("undefined_type");
          }
          | TOK_T_BOOLEAN
          {