diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index 0430d8209..b53e7897b 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -38,6 +38,7 @@ struct choice_value : public value {
     choice_value(unsigned num_fs, expr const * fs):m_choices(fs, fs + num_fs) {}
     virtual ~choice_value() {}
     virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE
+    virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
     virtual name get_name() const { return name("Choice"); }
     virtual void display(std::ostream & out) const {
         out << "(Choice";
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index b161ac198..133b32f24 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -58,13 +58,17 @@ expr const TypeU = Type(u_lvl);
 static char const * g_Bool_str = "Bool";
 static name g_Bool_name(g_Bool_str);
 static format g_Bool_fmt(g_Bool_str);
+
 class bool_type_value : public value {
 public:
     virtual ~bool_type_value() {}
     virtual expr get_type() const { return Type(); }
     virtual name get_name() const { return g_Bool_name; }
+    virtual void write(serializer & s) const { s << g_Bool_str; }
 };
 expr const Bool = mk_value(*(new bool_type_value()));
+expr read_bool_type(deserializer & ) { return Bool; }
+static register_deserializer_fn bool_ds(g_Bool_str, read_bool_type);
 expr mk_bool_type() { return Bool; }
 MK_IS_BUILTIN(is_bool, Bool)
 // =======================================
@@ -94,10 +98,15 @@ public:
         return _other && _other->m_val == m_val;
     }
     // LCOV_EXCL_STOP
+    virtual void write(serializer & s) const { s << (m_val ? "true" : "false"); }
     bool get_val() const { return m_val; }
 };
 expr const True  = mk_value(*(new bool_value_value(true)));
 expr const False = mk_value(*(new bool_value_value(false)));
+expr read_true(deserializer & ) { return True; }
+expr read_false(deserializer & ) { return False; }
+static register_deserializer_fn true_ds("true", read_true);
+static register_deserializer_fn false_ds("false", read_false);
 expr mk_bool_value(bool v) {
     return v ? True : False;
 }
@@ -146,8 +155,11 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << "if"; }
 };
 MK_BUILTIN(if_fn, if_fn_value);
+expr read_if(deserializer & ) { return mk_if_fn(); }
+static register_deserializer_fn if_ds("if", read_if);
 MK_IS_BUILTIN(is_if_fn, mk_if_fn());
 bool is_if(expr const & n, expr & c, expr & t, expr & e) {
     if (is_if(n)) {
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 5bbcfea96..6590668f6 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -7,8 +7,10 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <sstream>
+#include <string>
 #include "util/hash.h"
 #include "util/buffer.h"
+#include "util/object_serializer.h"
 #include "kernel/expr.h"
 #include "kernel/free_vars.h"
 #include "kernel/expr_eq.h"
@@ -204,11 +206,31 @@ expr_value::expr_value(value & v):
 expr_value::~expr_value() {
     m_val.dec_ref();
 }
+typedef std::unordered_map<std::string, value::reader> value_readers;
+static std::unique_ptr<value_readers> g_value_readers;
+std::unordered_map<std::string, value::reader> & get_value_readers() {
+    if (!g_value_readers)
+        g_value_readers.reset(new value_readers());
+    return *(g_value_readers.get());
+}
+
+void value::register_deserializer(std::string const & k, value::reader rd) {
+    value_readers & readers = get_value_readers();
+    lean_assert(readers.find(k) == readers.end());
+    readers[k] = rd;
+}
+static expr read_value(deserializer & d) {
+    auto k  = d.read_string();
+    value_readers & readers = get_value_readers();
+    auto it = readers.find(k);
+    lean_assert(it != readers.end());
+    return it->second(d);
+}
+
 expr_metavar::expr_metavar(name const & n, local_context const & lctx):
     expr_cell(expr_kind::MetaVar, n.hash(), true),
     m_name(n), m_lctx(lctx) {}
 expr_metavar::~expr_metavar() {}
-
 void expr_cell::dealloc() {
     try {
         buffer<expr_cell*> todo;
@@ -281,4 +303,154 @@ expr copy(expr const & a) {
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
+
+serializer & operator<<(serializer & s, local_context const & lctx) {
+    s << length(lctx);
+    for (auto const & e : lctx) {
+        if (e.is_lift()) {
+            s << true << e.s() << e.n();
+        } else {
+            s << false << e.s() << e.v();
+        }
+    }
+    return s;
+}
+
+local_context read_local_context(deserializer & d) {
+    unsigned num = d.read_unsigned();
+    buffer<local_entry> entries;
+    for (unsigned i = 0; i < num; i++) {
+        if (d.read_bool()) {
+            unsigned s, n;
+            d >> s >> n;
+            entries.push_back(mk_lift(s, n));
+        } else {
+            unsigned s; expr v;
+            d >> s >> v;
+            entries.push_back(mk_inst(s, v));
+        }
+    }
+    return to_list(entries.begin(), entries.end());
+}
+
+class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
+    typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
+public:
+    void write(optional<expr> const & a) {
+        serializer & s = get_owner();
+        if (a) {
+            s << true;
+            write(*a);
+        } else {
+            s << false;
+        }
+    }
+
+    void write(expr const & a) {
+        super::write(a, [&]() {
+                serializer & s = get_owner();
+                auto k = a.kind();
+                s << static_cast<char>(k);
+                switch (k) {
+                case expr_kind::Var:       s << var_idx(a); break;
+                case expr_kind::Constant:  s << const_name(a); write(const_type(a)); break;
+                case expr_kind::Type:      s << ty_level(a); break;
+                case expr_kind::Value:     to_value(a).write(s); break;
+                case expr_kind::App:
+                    s << num_args(a);
+                    for (unsigned i = 0; i < num_args(a); i++)
+                        write(arg(a, i));
+                    break;
+                case expr_kind::Eq:        write(eq_lhs(a)); write(eq_rhs(a)); break;
+                case expr_kind::Lambda:
+                case expr_kind::Pi:        s << abst_name(a); write(abst_domain(a)); write(abst_body(a)); break;
+                case expr_kind::Let:       s << let_name(a); write(let_type(a)); write(let_value(a)); write(let_body(a)); break;
+                case expr_kind::MetaVar:   s << metavar_name(a) << metavar_lctx(a); break;
+                }
+            });
+    }
+};
+
+class expr_deserializer : public object_deserializer<expr> {
+    typedef object_deserializer<expr> super;
+public:
+    optional<expr> read_opt() {
+        deserializer & d = get_owner();
+        if (d.read_bool()) {
+            return some_expr(read());
+        } else {
+            return none_expr();
+        }
+    }
+
+    expr read() {
+        return super::read([&]() {
+                deserializer & d = get_owner();
+                auto k = static_cast<expr_kind>(d.read_char());
+                switch (k) {
+                case expr_kind::Var:
+                    return mk_var(d.read_unsigned());
+                case expr_kind::Constant: {
+                    auto n = read_name(d);
+                    return mk_constant(n, read_opt());
+                }
+                case expr_kind::Type:
+                    return mk_type(read_level(d));
+                    break;
+                case expr_kind::Value:
+                    return read_value(d);
+                case expr_kind::App: {
+                    buffer<expr> args;
+                    unsigned num = d.read_unsigned();
+                    for (unsigned i = 0; i < num; i++)
+                        args.push_back(read());
+                    return mk_app(args);
+                }
+                case expr_kind::Eq: {
+                    expr lhs = read();
+                    return mk_eq(lhs, read());
+                }
+                case expr_kind::Lambda: {
+                    name n = read_name(d);
+                    expr d = read();
+                    return mk_lambda(n, d, read());
+                }
+                case expr_kind::Pi: {
+                    name n = read_name(d);
+                    expr d = read();
+                    return mk_pi(n, d, read());
+                }
+                case expr_kind::Let: {
+                    name n = read_name(d);
+                    optional<expr> t = read_opt();
+                    expr v = read();
+                    return mk_let(n, t, v, read());
+                }
+                case expr_kind::MetaVar: {
+                    name n = read_name(d);
+                    return mk_metavar(n, read_local_context(d));
+                }}
+                lean_unreachable(); // LCOV_EXCL_LINE
+            });
+    }
+};
+
+struct expr_sd {
+    unsigned m_s_extid;
+    unsigned m_d_extid;
+    expr_sd() {
+        m_s_extid = serializer::register_extension([](){ return std::unique_ptr<serializer::extension>(new expr_serializer()); });
+        m_d_extid = deserializer::register_extension([](){ return std::unique_ptr<deserializer::extension>(new expr_deserializer()); });
+    }
+};
+static expr_sd g_expr_sd;
+
+serializer & operator<<(serializer & s, expr const & n) {
+    s.get_extension<expr_serializer>(g_expr_sd.m_s_extid).write(n);
+    return s;
+}
+
+expr read_expr(deserializer & d) {
+    return d.get_extension<expr_deserializer>(g_expr_sd.m_d_extid).read();
+}
 }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index f55a60346..7482ff925 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include <limits>
 #include <utility>
 #include <tuple>
+#include <string>
 #include "util/thread.h"
 #include "util/lua.h"
 #include "util/rc.h"
@@ -18,6 +19,7 @@ Author: Leonardo de Moura
 #include "util/buffer.h"
 #include "util/list_fn.h"
 #include "util/optional.h"
+#include "util/serializer.h"
 #include "util/sexpr/format.h"
 #include "kernel/level.h"
 
@@ -296,7 +298,14 @@ public:
     virtual format pp(bool unicode, bool coercion) const;
     virtual int push_lua(lua_State * L) const;
     virtual unsigned hash() const;
+    virtual void write(serializer & s) const = 0;
+    typedef expr (*reader)(deserializer & d);
+    static void register_deserializer(std::string const & k, reader rd);
 };
+struct register_deserializer_fn {
+    register_deserializer_fn(std::string const & k, value::reader rd) { value::register_deserializer(k, rd); }
+};
+
 /** \brief Semantic attachments */
 class expr_value : public expr_cell {
     value & m_val;
@@ -694,5 +703,13 @@ inline expr update_const(expr const & e, optional<expr> const & t) {
 }
 // =======================================
 
+
+// =======================================
+// Serializer/Deserializer
+serializer & operator<<(serializer & s, expr const & e);
+expr read_expr(deserializer & d);
+inline deserializer & operator>>(deserializer & d, expr & e) { e = read_expr(d); return d; }
+// =======================================
+
 std::ostream & operator<<(std::ostream & out, expr const & e);
 }
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 1ea154337..0a95af03e 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -52,6 +52,7 @@ public:
     closure(expr const & e, context const & ctx, value_stack const & s):m_expr(e), m_ctx(ctx), m_stack(s) {}
     virtual ~closure() {}
     virtual expr get_type() const { lean_unreachable(); } // LCOV_EXCL_LINE
+    virtual void write(serializer & ) const { lean_unreachable(); } // LCOV_EXCL_LINE
     virtual name get_name() const { return name("Closure"); }
     virtual void display(std::ostream & out) const {
         out << "(Closure " << m_expr << " [";
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index ac935276f..22aef59fd 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
 #include "library/kernel_bindings.h"
@@ -18,9 +19,12 @@ namespace lean {
 class int_type_value : public num_type_value {
 public:
     int_type_value():num_type_value("Int", "\u2124") /* ℤ */ {}
+    virtual void write(serializer & s) const { s << "Int"; }
 };
 expr const Int = mk_value(*(new int_type_value()));
 expr mk_int_type() { return Int; }
+expr read_int(deserializer & ) { return Int; }
+static register_deserializer_fn if_ds("Int", read_int);
 
 class int_value_value : public value {
     mpz m_val;
@@ -48,11 +52,14 @@ public:
     virtual unsigned hash() const { return m_val.hash(); }
     virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); }
     mpz const & get_num() const { return m_val; }
+    virtual void write(serializer & s) const { s << "int" << m_val; }
 };
 
 expr mk_int_value(mpz const & v) {
     return mk_value(*(new int_value_value(v)));
 }
+expr read_int_value(deserializer & d) { return mk_int_value(read_mpz(d)); }
+static register_deserializer_fn int_value_ds("int", read_int_value);
 
 bool is_int_value(expr const & e) {
     return is_value(e) && dynamic_cast<int_value_value const *>(&to_value(e)) != nullptr;
@@ -78,17 +85,22 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << (std::string("int_") + Name); }
 };
 
 constexpr char int_add_name[] = "add";
 struct int_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
 typedef int_bin_op<int_add_name, int_add_eval> int_add_value;
 MK_BUILTIN(int_add_fn, int_add_value);
+expr read_int_add(deserializer & ) { return mk_int_add_fn(); }
+static register_deserializer_fn int_add_ds("int_add", read_int_add);
 
 constexpr char int_mul_name[] = "mul";
 struct int_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
 typedef int_bin_op<int_mul_name, int_mul_eval> int_mul_value;
 MK_BUILTIN(int_mul_fn, int_mul_value);
+expr read_int_mul(deserializer & ) { return mk_int_mul_fn(); }
+static register_deserializer_fn int_mul_ds("int_mul", read_int_mul);
 
 constexpr char int_div_name[] = "div";
 struct int_div_eval {
@@ -101,6 +113,8 @@ struct int_div_eval {
 };
 typedef int_bin_op<int_div_name, int_div_eval> int_div_value;
 MK_BUILTIN(int_div_fn, int_div_value);
+expr read_int_div(deserializer & ) { return mk_int_div_fn(); }
+static register_deserializer_fn int_div_ds("int_div", read_int_div);
 
 class int_le_value : public const_value {
 public:
@@ -112,8 +126,11 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << "int_le"; }
 };
 MK_BUILTIN(int_le_fn, int_le_value);
+expr read_int_le(deserializer & ) { return mk_int_le_fn(); }
+static register_deserializer_fn int_le_ds("int_le", read_int_le);
 
 MK_CONSTANT(int_sub_fn, name({"Int", "sub"}));
 MK_CONSTANT(int_neg_fn, name({"Int", "neg"}));
@@ -137,8 +154,11 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << "nat_to_int"; }
 };
 MK_BUILTIN(nat_to_int_fn, nat_to_int_value);
+expr read_nat_to_int(deserializer & ) { return mk_nat_to_int_fn(); }
+static register_deserializer_fn nat_to_int_ds("nat_to_int", read_nat_to_int);
 
 MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"}));
 MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"}));
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
index 0d0928c83..5a43b1d2c 100644
--- a/src/library/arith/nat.cpp
+++ b/src/library/arith/nat.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
 #include "library/kernel_bindings.h"
@@ -17,9 +18,12 @@ namespace lean {
 class nat_type_value : public num_type_value {
 public:
     nat_type_value():num_type_value("Nat", "\u2115") /* ℕ */ {}
+    virtual void write(serializer & s) const { s << "Nat"; }
 };
 expr const Nat = mk_value(*(new nat_type_value()));
 expr mk_nat_type() { return Nat; }
+expr read_nat(deserializer & ) { return Nat; }
+static register_deserializer_fn if_ds("Nat", read_nat);
 
 class nat_value_value : public value {
     mpz m_val;
@@ -42,11 +46,13 @@ public:
     virtual unsigned hash() const { return m_val.hash(); }
     virtual int push_lua(lua_State * L) const { return push_mpz(L, m_val); }
     mpz const & get_num() const { return m_val; }
+    virtual void write(serializer & s) const { s << "nat" << m_val; }
 };
-
 expr mk_nat_value(mpz const & v) {
     return mk_value(*(new nat_value_value(v)));
 }
+expr read_nat_value(deserializer & d) { return mk_nat_value(read_mpz(d)); }
+static register_deserializer_fn nat_value_ds("nat", read_nat_value);
 
 bool is_nat_value(expr const & e) {
     return is_value(e) && dynamic_cast<nat_value_value const *>(&to_value(e)) != nullptr;
@@ -72,6 +78,7 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << (std::string("nat_") + Name); }
 };
 
 constexpr char nat_add_name[] = "add";
@@ -79,12 +86,16 @@ constexpr char nat_add_name[] = "add";
 struct nat_add_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 + v2; }; };
 typedef nat_bin_op<nat_add_name, nat_add_eval> nat_add_value;
 MK_BUILTIN(nat_add_fn, nat_add_value);
+expr read_nat_add(deserializer & ) { return mk_nat_add_fn(); }
+static register_deserializer_fn nat_add_ds("nat_add", read_nat_add);
 
 constexpr char nat_mul_name[] = "mul";
 /** \brief Evaluator for * : Nat -> Nat -> Nat */
 struct nat_mul_eval { mpz operator()(mpz const & v1, mpz const & v2) { return v1 * v2; }; };
 typedef nat_bin_op<nat_mul_name, nat_mul_eval> nat_mul_value;
 MK_BUILTIN(nat_mul_fn, nat_mul_value);
+expr read_nat_mul(deserializer & ) { return mk_nat_mul_fn(); }
+static register_deserializer_fn nat_mul_ds("nat_mul", read_nat_mul);
 
 /**
    \brief Semantic attachment for less than or equal to operator with type
@@ -100,8 +111,11 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << "nat_le"; }
 };
 MK_BUILTIN(nat_le_fn, nat_le_value);
+expr read_nat_le(deserializer & ) { return mk_nat_le_fn(); }
+static register_deserializer_fn nat_le_ds("nat_le", read_nat_le);
 
 MK_CONSTANT(nat_ge_fn,  name({"Nat", "ge"}));
 MK_CONSTANT(nat_lt_fn,  name({"Nat", "lt"}));
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index 2e136608f..78680f240 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
 #include "library/kernel_bindings.h"
@@ -16,9 +17,12 @@ namespace lean {
 class real_type_value : public num_type_value {
 public:
     real_type_value():num_type_value("Real", "\u211D") /* ℝ */ {}
+    virtual void write(serializer & s) const { s << "Real"; }
 };
 expr const Real = mk_value(*(new real_type_value()));
 expr mk_real_type() { return Real; }
+expr read_real(deserializer & ) { return Real; }
+static register_deserializer_fn if_ds("Real", read_real);
 
 /**
    \brief Semantic attachment for "Real" values.
@@ -51,11 +55,14 @@ public:
     virtual unsigned hash() const { return m_val.hash(); }
     virtual int push_lua(lua_State * L) const { return push_mpq(L, m_val); }
     mpq const & get_num() const { return m_val; }
+    virtual void write(serializer & s) const { s << "real" << m_val; }
 };
 
 expr mk_real_value(mpq const & v) {
     return mk_value(*(new real_value_value(v)));
 }
+expr read_real_value(deserializer & d) { return mk_real_value(read_mpq(d)); }
+static register_deserializer_fn real_value_ds("real", read_real_value);
 
 bool is_real_value(expr const & e) {
     return is_value(e) && dynamic_cast<real_value_value const *>(&to_value(e)) != nullptr;
@@ -81,6 +88,7 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << (std::string("real_") + Name); }
 };
 
 constexpr char real_add_name[] = "add";
@@ -88,12 +96,16 @@ constexpr char real_add_name[] = "add";
 struct real_add_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 + v2; }; };
 typedef real_bin_op<real_add_name, real_add_eval> real_add_value;
 MK_BUILTIN(real_add_fn, real_add_value);
+expr read_real_add(deserializer & ) { return mk_real_add_fn(); }
+static register_deserializer_fn real_add_ds("real_add", read_real_add);
 
 constexpr char real_mul_name[] = "mul";
 /** \brief Evaluator for * : Real -> Real -> Real */
 struct real_mul_eval { mpq operator()(mpq const & v1, mpq const & v2) { return v1 * v2; }; };
 typedef real_bin_op<real_mul_name, real_mul_eval> real_mul_value;
 MK_BUILTIN(real_mul_fn, real_mul_value);
+expr read_real_mul(deserializer & ) { return mk_real_mul_fn(); }
+static register_deserializer_fn real_mul_ds("real_mul", read_real_mul);
 
 constexpr char real_div_name[] = "div";
 /** \brief Evaluator for / : Real -> Real -> Real */
@@ -107,6 +119,8 @@ struct real_div_eval {
 };
 typedef real_bin_op<real_div_name, real_div_eval> real_div_value;
 MK_BUILTIN(real_div_fn, real_div_value);
+expr read_real_div(deserializer & ) { return mk_real_div_fn(); }
+static register_deserializer_fn real_div_ds("real_div", read_real_div);
 
 /**
    \brief Semantic attachment for less than or equal to operator with type
@@ -122,8 +136,11 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << "real_le"; }
 };
 MK_BUILTIN(real_le_fn, real_le_value);
+expr read_real_le(deserializer & ) { return mk_real_le_fn(); }
+static register_deserializer_fn real_le_ds("real_le", read_real_le);
 
 MK_CONSTANT(real_sub_fn, name({"Real", "sub"}));
 MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
@@ -166,8 +183,11 @@ public:
             return none_expr();
         }
     }
+    virtual void write(serializer & s) const { s << "int_to_real"; }
 };
 MK_BUILTIN(int_to_real_fn,  int_to_real_value);
+expr read_int_to_real(deserializer & ) { return mk_int_to_real_fn(); }
+static register_deserializer_fn int_to_real_ds("int_to_real", read_int_to_real);
 MK_CONSTANT(nat_to_real_fn, name("nat_to_real"));
 
 void import_int_to_real_coercions(environment const & env) {
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 88efd1d70..e12e493a8 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -19,6 +19,20 @@ Author: Leonardo de Moura
 #include "library/arith/arith.h"
 using namespace lean;
 
+static void check_serializer(expr const & e) {
+    std::ostringstream out;
+    serializer s(out);
+    s << e << e;
+    std::cout << "OUT size: " << out.str().size() << "\n";
+    std::istringstream in(out.str());
+    deserializer d(in);
+    expr n1, n2;
+    d >> n1 >> n2;
+    lean_assert(e == n1);
+    lean_assert(e == n2);
+    lean_assert(is_eqp(n1, n2));
+}
+
 static void tst1() {
     expr a;
     a = Const("a");
@@ -88,9 +102,10 @@ static expr mk_big(expr f, unsigned depth, unsigned val) {
 
 static void tst3() {
     expr f = Const("f");
-    expr r1 = mk_big(f, 20, 0);
-    expr r2 = mk_big(f, 20, 0);
+    expr r1 = mk_big(f, 16, 0);
+    expr r2 = mk_big(f, 16, 0);
     lean_assert(r1 == r2);
+    check_serializer(r1);
 }
 
 static void tst4() {
@@ -229,6 +244,7 @@ static void tst10() {
    \pre s and t must be closed expressions (i.e., no free variables)
 */
 static expr substitute(expr const & e, expr const & s, expr const & t) {
+    check_serializer(e);
     return instantiate(abstract(e, s), t);
 }
 
@@ -270,6 +286,8 @@ static void tst12() {
 static void tst13() {
     expr t0 = Type();
     expr t1 = Type(level()+1);
+    check_serializer(t0);
+    check_serializer(t1);
     lean_assert(ty_level(t1) == level()+1);
     lean_assert(t0 != t1);
     std::cout << t0 << " " << t1 << "\n";
@@ -277,8 +295,10 @@ static void tst13() {
 
 static void tst14() {
     expr t = Eq(Const("a"), Const("b"));
+    check_serializer(t);
     std::cout << t << "\n";
     expr l = mk_let("a", none_expr(), Const("b"), Var(0));
+    check_serializer(l);
     std::cout << l << "\n";
     lean_assert(closed(l));
 }
@@ -288,6 +308,7 @@ static void tst15() {
     expr x = Var(0);
     expr a = Const("a");
     expr m = mk_metavar("m");
+    check_serializer(m);
     lean_assert(has_metavar(m));
     lean_assert(has_metavar(f(m)));
     lean_assert(!has_metavar(f(a)));
@@ -316,6 +337,7 @@ static void check_copy(expr const & e) {
     expr c = copy(e);
     lean_assert(!is_eqp(e, c));
     lean_assert(e == c);
+    check_serializer(e);
 }
 
 static void tst16() {
@@ -335,6 +357,8 @@ static void tst17() {
     lean_assert(is_false(False));
     lean_assert(!is_true(Const("a")));
     lean_assert(!is_false(Const("a")));
+    check_serializer(True);
+    check_serializer(False);
 }
 
 static void tst18() {