diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp
index 9937d4d3905..248b350f71b 100644
--- a/jbmc/src/java_bytecode/java_types.cpp
+++ b/jbmc/src/java_bytecode/java_types.cpp
@@ -91,7 +91,12 @@ reference_typet java_reference_type(const typet &subtype)
   return reference_type(subtype);
 }
 
-reference_typet java_lang_object_type()
+java_reference_typet java_reference_type(const struct_tag_typet &subtype)
+{
+  return to_java_reference_type(reference_type(subtype));
+}
+
+java_reference_typet java_lang_object_type()
 {
   static const auto result =
     java_reference_type(struct_tag_typet("java::java.lang.Object"));
@@ -102,7 +107,7 @@ reference_typet java_lang_object_type()
 /// java::array[]. Its ID_element_type is set to the corresponding primitive
 /// type, or void* for arrays of references.
 /// \param subtype: Character indicating the type of array
-reference_typet java_array_type(const char subtype)
+java_reference_typet java_array_type(const char subtype)
 {
   std::string subtype_str;
 
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 7b39f917c3b..fd63ea64e74 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -360,6 +360,48 @@ inline java_method_typet &to_java_method_type(typet &type)
   return static_cast<java_method_typet &>(type);
 }
 
+/// This is a specialization of reference_typet.
+/// The subtype is guaranteed to be a struct_tag_typet.
+class java_reference_typet : public reference_typet
+{
+public:
+  explicit java_reference_typet(
+    const struct_tag_typet &_subtype,
+    std::size_t _width)
+    : reference_typet(_subtype, _width)
+  {
+  }
+
+  struct_tag_typet &subtype()
+  {
+    return static_cast<struct_tag_typet &>(reference_typet::subtype());
+  }
+
+  const struct_tag_typet &subtype() const
+  {
+    return static_cast<const struct_tag_typet &>(reference_typet::subtype());
+  }
+};
+
+template <>
+inline bool can_cast_type<java_reference_typet>(const typet &type)
+{
+  return type.id() == ID_pointer &&
+         to_type_with_subtype(type).subtype().id() == ID_struct_tag;
+}
+
+inline const java_reference_typet &to_java_reference_type(const typet &type)
+{
+  PRECONDITION(can_cast_type<java_reference_typet>(type));
+  return static_cast<const java_reference_typet &>(type);
+}
+
+inline java_reference_typet &to_java_reference_type(typet &type)
+{
+  PRECONDITION(can_cast_type<java_reference_typet>(type));
+  return static_cast<java_reference_typet &>(type);
+}
+
 signedbv_typet java_int_type();
 signedbv_typet java_long_type();
 signedbv_typet java_short_type();
@@ -369,11 +411,12 @@ floatbv_typet java_float_type();
 floatbv_typet java_double_type();
 c_bool_typet java_boolean_type();
 empty_typet java_void_type();
+java_reference_typet java_reference_type(const struct_tag_typet &subtype);
 reference_typet java_reference_type(const typet &subtype);
-reference_typet java_lang_object_type();
+java_reference_typet java_lang_object_type();
 struct_tag_typet java_classname(const std::string &);
 
-reference_typet java_array_type(const char subtype);
+java_reference_typet java_array_type(const char subtype);
 const typet &java_array_element_type(const struct_tag_typet &array_symbol);
 typet &java_array_element_type(struct_tag_typet &array_symbol);
 bool is_java_array_type(const typet &type);