diff --git a/src/kernel/definition.cpp b/src/kernel/definition.cpp
index 1d321b1f1..c8edfc292 100644
--- a/src/kernel/definition.cpp
+++ b/src/kernel/definition.cpp
@@ -9,9 +9,6 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 
 namespace lean {
-static serializer & operator<<(serializer & s, param_names const & ps) { return write_list<name>(s, ps); }
-static param_names read_params(deserializer & d) { return read_list<name>(d); }
-
 struct definition::cell {
     MK_LEAN_RC();
     name           m_name;
@@ -39,25 +36,6 @@ struct definition::cell {
          bool opaque, unsigned w, module_idx mod_idx, bool use_conv_opt):
         m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
         m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
-
-    void write(serializer & s) const {
-        char k = 0;
-        if (m_value) {
-            k |= 1;
-            if (m_opaque)
-                k |= 2;
-            if (m_use_conv_opt)
-                k |= 4;
-        }
-        if (m_theorem)
-            k |= 8;
-        s << k << m_name << m_params << m_type;
-        if (m_value) {
-            s << *m_value;
-            if (!m_theorem)
-                s << m_weight;
-        }
-    }
 };
 
 definition g_dummy = mk_axiom(name(), param_names(), expr());
@@ -86,8 +64,6 @@ unsigned definition::get_weight() const { return m_ptr->m_weight; }
 module_idx definition::get_module_idx() const { return m_ptr->m_module_idx; }
 bool definition::use_conv_opt() const { return m_ptr->m_use_conv_opt; }
 
-void definition::write(serializer & s) const { m_ptr->write(s); }
-
 definition mk_definition(name const & n, param_names const & params, expr const & t, expr const & v,
                          bool opaque, unsigned weight, module_idx mod_idx, bool use_conv_opt) {
     return definition(new definition::cell(n, params, t, false, v, opaque, weight, mod_idx, use_conv_opt));
@@ -114,29 +90,4 @@ definition mk_axiom(name const & n, param_names const & params, expr const & t)
 definition mk_var_decl(name const & n, param_names const & params, expr const & t) {
     return definition(new definition::cell(n, params, t, false));
 }
-
-definition read_definition(deserializer & d, unsigned module_idx) {
-    char k = d.read_char();
-    bool has_value  = (k & 1) != 0;
-    bool is_theorem = (k & 8) != 0;
-    name n          = read_name(d);
-    param_names ps  = read_params(d);
-    expr t          = read_expr(d);
-    if (has_value) {
-        expr v      = read_expr(d);
-        if (is_theorem) {
-            return mk_theorem(n, ps, t, v);
-        } else {
-            unsigned w        = d.read_unsigned();
-            bool is_opaque    = (k & 2) != 0;
-            bool use_conv_opt = (k & 4) != 0;
-            return mk_definition(n, ps, t, v, is_opaque, w, module_idx, use_conv_opt);
-        }
-    } else {
-        if (is_theorem)
-            return mk_axiom(n, ps, t);
-        else
-            return mk_var_decl(n, ps, t);
-    }
-}
 }
diff --git a/src/kernel/definition.h b/src/kernel/definition.h
index 8446458d8..337e99d36 100644
--- a/src/kernel/definition.h
+++ b/src/kernel/definition.h
@@ -74,8 +74,6 @@ public:
     friend definition mk_theorem(name const & n, param_names const & params, expr const & t, expr const & v);
     friend definition mk_axiom(name const & n, param_names const & params, expr const & t);
     friend definition mk_var_decl(name const & n, param_names const & params, expr const & t);
-
-    void write(serializer & s) const;
 };
 
 inline optional<definition> none_definition() { return optional<definition>(); }
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 4a32662f2..49cad39ac 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -199,27 +199,6 @@ void macro_definition_cell::display(std::ostream & out) const { out << get_name(
 bool macro_definition_cell::is_atomic_pp(bool, bool) const { return true; }
 unsigned macro_definition_cell::hash() const { return get_name().hash(); }
 
-typedef std::unordered_map<std::string, macro_definition_cell::reader> macro_readers;
-static std::unique_ptr<macro_readers> g_macro_readers;
-macro_readers & get_macro_readers() {
-    if (!g_macro_readers)
-        g_macro_readers.reset(new macro_readers());
-    return *(g_macro_readers.get());
-}
-
-void macro_definition_cell::register_deserializer(std::string const & k, macro_definition_cell::reader rd) {
-    macro_readers & readers = get_macro_readers();
-    lean_assert(readers.find(k) == readers.end());
-    readers[k] = rd;
-}
-static expr read_macro_definition(deserializer & d, unsigned num, expr const * args) {
-    auto k  = d.read_string();
-    macro_readers & readers = get_macro_readers();
-    auto it = readers.find(k);
-    lean_assert(it != readers.end());
-    return it->second(d, num, args);
-}
-
 macro_definition::macro_definition(macro_definition_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr); m_ptr->inc_ref(); }
 macro_definition::macro_definition(macro_definition const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
 macro_definition::macro_definition(macro_definition && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
@@ -511,138 +490,4 @@ expr copy(expr const & a) {
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
-
-serializer & operator<<(serializer & s, expr_binder_info const & i) {
-    s.write_bool(i.is_implicit());
-    s.write_bool(i.is_cast());
-    return s;
-}
-
-static expr_binder_info read_expr_binder_info(deserializer & d) {
-    bool imp = d.read_bool();
-    bool cast = d.read_bool();
-    return expr_binder_info(imp, cast);
-}
-
-class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
-    typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
-    max_sharing_fn m_max_sharing_fn;
-
-    void write_core(expr const & a) {
-        auto k = a.kind();
-        super::write_core(a, static_cast<char>(k), [&]() {
-                serializer & s = get_owner();
-                switch (k) {
-                case expr_kind::Var:
-                    s << var_idx(a);
-                    break;
-                case expr_kind::Constant:
-                    s << const_name(a) << const_level_params(a);
-                    break;
-                case expr_kind::Sort:
-                    s << sort_level(a);
-                    break;
-                case expr_kind::Macro:
-                    s << macro_num_args(a);
-                    for (unsigned i = 0; i < macro_num_args(a); i++) {
-                        write_core(macro_arg(a, i));
-                    }
-                    macro_def(a).write(s);
-                    break;
-                case expr_kind::App:
-                    write_core(app_fn(a)); write_core(app_arg(a));
-                    break;
-                case expr_kind::Lambda: case expr_kind::Pi:
-                    s << binder_name(a) << binder_info(a); write_core(binder_domain(a)); write_core(binder_body(a));
-                    break;
-                case expr_kind::Let:
-                    s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a));
-                    break;
-                case expr_kind::Meta: case expr_kind::Local:
-                    s << mlocal_name(a); write_core(mlocal_type(a));
-                    break;
-                }
-            });
-    }
-public:
-    void write(expr const & a) {
-        write_core(m_max_sharing_fn(a));
-    }
-};
-
-class expr_deserializer : public object_deserializer<expr> {
-    typedef object_deserializer<expr> super;
-public:
-    expr read_binder(expr_kind k) {
-        deserializer & d = get_owner();
-        name n             = read_name(d);
-        expr_binder_info i = read_expr_binder_info(d);
-        expr t             = read();
-        return mk_binder(k, n, t, read(), i);
-    }
-
-    expr read() {
-        return super::read_core([&](char c) {
-                deserializer & d = get_owner();
-                auto k = static_cast<expr_kind>(c);
-                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_levels(d));
-                }
-                case expr_kind::Sort:
-                    return mk_sort(read_level(d));
-                case expr_kind::Macro: {
-                    unsigned n = d.read_unsigned();
-                    buffer<expr> args;
-                    for (unsigned i = 0; i < n; i++) {
-                        args.push_back(read());
-                    }
-                    return read_macro_definition(d, args.size(), args.data());
-                }
-                case expr_kind::App: {
-                    expr f = read();
-                    return mk_app(f, read());
-                }
-                case expr_kind::Lambda: case expr_kind::Pi:
-                    return read_binder(k);
-                case expr_kind::Let: {
-                    name n = read_name(d);
-                    expr t = read();
-                    expr v = read();
-                    return mk_let(n, t, v, read());
-                }
-                case expr_kind::Meta: {
-                    name n = read_name(d);
-                    return mk_metavar(n, read());
-                }
-                case expr_kind::Local: {
-                    name n = read_name(d);
-                    return mk_local(n, read());
-                }}
-                throw_corrupted_file(); // 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 876d11ab8..92dedb1e3 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -308,12 +308,6 @@ public:
     virtual unsigned hash() const;
     virtual void write(serializer & s) const = 0;
     typedef std::function<expr(deserializer&, unsigned, expr const *)> reader;
-    static void register_deserializer(std::string const & k, reader rd);
-    struct register_deserializer_fn {
-        register_deserializer_fn(std::string const & k, macro_definition_cell::reader rd) {
-            macro_definition_cell::register_deserializer(k, rd);
-        }
-    };
 };
 
 /** \brief Smart pointer for macro definitions */
@@ -625,12 +619,5 @@ expr update_constant(expr const & e, levels const & new_levels);
 expr update_macro(expr const & e, unsigned num, expr const * args);
 // =======================================
 
-// =======================================
-// 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/level.cpp b/src/kernel/level.cpp
index cb6aff886..a43c3753a 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "util/list.h"
 #include "util/debug.h"
 #include "util/hash.h"
-#include "util/object_serializer.h"
 #include "util/interrupt.h"
 #include "kernel/level.h"
 #include "kernel/environment.h"
@@ -351,90 +350,6 @@ bool is_lt(levels const & as, levels const & bs, bool use_hash) {
         return is_lt(car(as), car(bs), use_hash);
 }
 
-class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
-    typedef object_serializer<level, level::ptr_hash, level::ptr_eq> super;
-public:
-    void write(level const & l) {
-        super::write(l, [&]() {
-                serializer & s = get_owner();
-                auto k = kind(l);
-                s << static_cast<char>(k);
-                switch (k) {
-                case level_kind::Zero:
-                    break;
-                case level_kind::Param: case level_kind::Global: case level_kind::Meta:
-                    s << to_param_core(l).m_id;
-                    break;
-                case level_kind::Max: case level_kind::IMax:
-                    write(to_max_core(l).m_lhs);
-                    write(to_max_core(l).m_rhs);
-                    break;
-                case level_kind::Succ:
-                    write(succ_of(l));
-                    break;
-                }
-            });
-    }
-};
-
-class level_deserializer : public object_deserializer<level> {
-    typedef object_deserializer<level> super;
-public:
-    level read() {
-        return super::read([&]() -> level {
-                deserializer & d = get_owner();
-                auto k = static_cast<level_kind>(d.read_char());
-                switch (k) {
-                case level_kind::Zero:
-                    return mk_level_zero();
-                case level_kind::Param:
-                    return mk_param_univ(read_name(d));
-                case level_kind::Global:
-                    return mk_global_univ(read_name(d));
-                case level_kind::Meta:
-                    return mk_meta_univ(read_name(d));
-                case level_kind::Max: {
-                    level lhs = read();
-                    return mk_max(lhs, read());
-                }
-                case level_kind::IMax: {
-                    level lhs = read();
-                    return mk_imax(lhs, read());
-                }
-                case level_kind::Succ:
-                    return mk_succ(read());
-                }
-                throw_corrupted_file();
-            });
-    }
-};
-
-struct level_sd {
-    unsigned m_s_extid;
-    unsigned m_d_extid;
-    level_sd() {
-        m_s_extid = serializer::register_extension([](){
-                return std::unique_ptr<serializer::extension>(new level_serializer());
-            });
-        m_d_extid = deserializer::register_extension([](){
-                return std::unique_ptr<deserializer::extension>(new level_deserializer());
-            });
-    }
-};
-
-static level_sd g_level_sd;
-
-serializer & operator<<(serializer & s, level const & n) {
-    s.get_extension<level_serializer>(g_level_sd.m_s_extid).write(n);
-    return s;
-}
-
-level read_level(deserializer & d) { return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read(); }
-
-serializer & operator<<(serializer & s, levels const & ls) { return write_list<level>(s, ls); }
-
-levels read_levels(deserializer & d) { return read_list<level>(d, read_level); }
-
 bool has_param(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_param(l); }); }
 bool has_global(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_global(l); }); }
 bool has_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
diff --git a/src/kernel/level.h b/src/kernel/level.h
index d611c4df3..6324fd195 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/name.h"
 #include "util/optional.h"
-#include "util/serializer.h"
 #include "util/list.h"
 #include "util/sexpr/format.h"
 #include "util/sexpr/options.h"
@@ -198,13 +197,6 @@ std::ostream & operator<<(std::ostream & out, level const & l);
 */
 bool is_not_zero(level const & l);
 
-serializer & operator<<(serializer & s, level const & l);
-level read_level(deserializer & d);
-inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; }
-
-serializer & operator<<(serializer & s, levels const & ls);
-levels read_levels(deserializer & d);
-
 /** \brief Pretty print the given level expression, unicode characters are used if \c unicode is \c true. */
 format pp(level l, bool unicode, unsigned indent);
 /** \brief Pretty print the given level expression using the given configuration options. */
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 1d393968d..69018d82c 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
-  resolve_macro.cpp)
+  resolve_macro.cpp kernel_serializer.cpp)
 # placeholder.cpp fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
new file mode 100644
index 000000000..e4da4e8ba
--- /dev/null
+++ b/src/library/kernel_serializer.cpp
@@ -0,0 +1,300 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "util/object_serializer.h"
+#include "kernel/expr.h"
+#include "kernel/definition.h"
+#include "kernel/max_sharing.h"
+#include "library/kernel_serializer.h"
+
+// Procedures for serializing and deserializing kernel objects (levels, exprs, definitions)
+namespace lean {
+// Universe level serialization
+class level_serializer : public object_serializer<level, level::ptr_hash, level::ptr_eq> {
+    typedef object_serializer<level, level::ptr_hash, level::ptr_eq> super;
+public:
+    void write(level const & l) {
+        super::write(l, [&]() {
+                serializer & s = get_owner();
+                auto k = kind(l);
+                s << static_cast<char>(k);
+                switch (k) {
+                case level_kind::Zero:     break;
+                case level_kind::Param:    s << param_id(l);   break;
+                case level_kind::Global:   s << global_id(l);  break;
+                case level_kind::Meta:     s << meta_id(l);    break;
+                case level_kind::Max:      write(max_lhs(l));  write(max_rhs(l)); break;
+                case level_kind::IMax:     write(imax_lhs(l)); write(imax_rhs(l)); break;
+                case level_kind::Succ:     write(succ_of(l));  break;
+                }
+            });
+    }
+};
+
+class level_deserializer : public object_deserializer<level> {
+    typedef object_deserializer<level> super;
+public:
+    level read() {
+        return super::read([&]() -> level {
+                deserializer & d = get_owner();
+                auto k = static_cast<level_kind>(d.read_char());
+                switch (k) {
+                case level_kind::Zero:
+                    return mk_level_zero();
+                case level_kind::Param:
+                    return mk_param_univ(read_name(d));
+                case level_kind::Global:
+                    return mk_global_univ(read_name(d));
+                case level_kind::Meta:
+                    return mk_meta_univ(read_name(d));
+                case level_kind::Max: {
+                    level lhs = read();
+                    return mk_max(lhs, read());
+                }
+                case level_kind::IMax: {
+                    level lhs = read();
+                    return mk_imax(lhs, read());
+                }
+                case level_kind::Succ:
+                    return mk_succ(read());
+                }
+                throw_corrupted_file();
+            });
+    }
+};
+
+struct level_sd {
+    unsigned m_s_extid;
+    unsigned m_d_extid;
+    level_sd() {
+        m_s_extid = serializer::register_extension([](){
+                return std::unique_ptr<serializer::extension>(new level_serializer());
+            });
+        m_d_extid = deserializer::register_extension([](){
+                return std::unique_ptr<deserializer::extension>(new level_deserializer());
+            });
+    }
+};
+
+static level_sd g_level_sd;
+
+serializer & operator<<(serializer & s, level const & n) {
+    s.get_extension<level_serializer>(g_level_sd.m_s_extid).write(n);
+    return s;
+}
+
+level read_level(deserializer & d) { return d.get_extension<level_deserializer>(g_level_sd.m_d_extid).read(); }
+
+serializer & operator<<(serializer & s, levels const & ls) { return write_list<level>(s, ls); }
+
+levels read_levels(deserializer & d) { return read_list<level>(d, read_level); }
+
+// Expression serialization
+typedef std::unordered_map<std::string, macro_definition_cell::reader> macro_readers;
+static std::unique_ptr<macro_readers> g_macro_readers;
+macro_readers & get_macro_readers() {
+    if (!g_macro_readers)
+        g_macro_readers.reset(new macro_readers());
+    return *(g_macro_readers.get());
+}
+
+void register_macro_deserializer(std::string const & k, macro_definition_cell::reader rd) {
+    macro_readers & readers = get_macro_readers();
+    lean_assert(readers.find(k) == readers.end());
+    readers[k] = rd;
+}
+
+static expr read_macro_definition(deserializer & d, unsigned num, expr const * args) {
+    auto k  = d.read_string();
+    macro_readers & readers = get_macro_readers();
+    auto it = readers.find(k);
+    lean_assert(it != readers.end());
+    return it->second(d, num, args);
+}
+
+serializer & operator<<(serializer & s, expr_binder_info const & i) {
+    s.write_bool(i.is_implicit());
+    s.write_bool(i.is_cast());
+    return s;
+}
+
+static expr_binder_info read_expr_binder_info(deserializer & d) {
+    bool imp = d.read_bool();
+    bool cast = d.read_bool();
+    return expr_binder_info(imp, cast);
+}
+
+class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {
+    typedef object_serializer<expr, expr_hash_alloc, expr_eqp> super;
+    max_sharing_fn m_max_sharing_fn;
+
+    void write_core(expr const & a) {
+        auto k = a.kind();
+        super::write_core(a, static_cast<char>(k), [&]() {
+                serializer & s = get_owner();
+                switch (k) {
+                case expr_kind::Var:
+                    s << var_idx(a);
+                    break;
+                case expr_kind::Constant:
+                    s << const_name(a) << const_level_params(a);
+                    break;
+                case expr_kind::Sort:
+                    s << sort_level(a);
+                    break;
+                case expr_kind::Macro:
+                    s << macro_num_args(a);
+                    for (unsigned i = 0; i < macro_num_args(a); i++) {
+                        write_core(macro_arg(a, i));
+                    }
+                    macro_def(a).write(s);
+                    break;
+                case expr_kind::App:
+                    write_core(app_fn(a)); write_core(app_arg(a));
+                    break;
+                case expr_kind::Lambda: case expr_kind::Pi:
+                    s << binder_name(a) << binder_info(a); write_core(binder_domain(a)); write_core(binder_body(a));
+                    break;
+                case expr_kind::Let:
+                    s << let_name(a); write_core(let_type(a)); write_core(let_value(a)); write_core(let_body(a));
+                    break;
+                case expr_kind::Meta: case expr_kind::Local:
+                    s << mlocal_name(a); write_core(mlocal_type(a));
+                    break;
+                }
+            });
+    }
+public:
+    void write(expr const & a) {
+        write_core(m_max_sharing_fn(a));
+    }
+};
+
+class expr_deserializer : public object_deserializer<expr> {
+    typedef object_deserializer<expr> super;
+public:
+    expr read_binder(expr_kind k) {
+        deserializer & d = get_owner();
+        name n             = read_name(d);
+        expr_binder_info i = read_expr_binder_info(d);
+        expr t             = read();
+        return mk_binder(k, n, t, read(), i);
+    }
+
+    expr read() {
+        return super::read_core([&](char c) {
+                deserializer & d = get_owner();
+                auto k = static_cast<expr_kind>(c);
+                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_levels(d));
+                }
+                case expr_kind::Sort:
+                    return mk_sort(read_level(d));
+                case expr_kind::Macro: {
+                    unsigned n = d.read_unsigned();
+                    buffer<expr> args;
+                    for (unsigned i = 0; i < n; i++) {
+                        args.push_back(read());
+                    }
+                    return read_macro_definition(d, args.size(), args.data());
+                }
+                case expr_kind::App: {
+                    expr f = read();
+                    return mk_app(f, read());
+                }
+                case expr_kind::Lambda: case expr_kind::Pi:
+                    return read_binder(k);
+                case expr_kind::Let: {
+                    name n = read_name(d);
+                    expr t = read();
+                    expr v = read();
+                    return mk_let(n, t, v, read());
+                }
+                case expr_kind::Meta: {
+                    name n = read_name(d);
+                    return mk_metavar(n, read());
+                }
+                case expr_kind::Local: {
+                    name n = read_name(d);
+                    return mk_local(n, read());
+                }}
+                throw_corrupted_file(); // 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();
+}
+
+// Definition serialization
+static serializer & operator<<(serializer & s, param_names const & ps) { return write_list<name>(s, ps); }
+static param_names read_params(deserializer & d) { return read_list<name>(d); }
+serializer & operator<<(serializer & s, definition const & d) {
+    char k = 0;
+    if (d.is_definition()) {
+        k |= 1;
+        if (d.is_opaque())
+            k |= 2;
+        if (d.use_conv_opt())
+            k |= 4;
+    }
+    if (d.is_theorem())
+        k |= 8;
+    s << k << d.get_name() << d.get_params() << d.get_type();
+    if (d.is_definition()) {
+        s << d.get_value();
+        if (!d.is_theorem())
+            s << d.get_weight();
+    }
+    return s;
+}
+
+definition read_definition(deserializer & d, unsigned module_idx) {
+    char k = d.read_char();
+    bool has_value  = (k & 1) != 0;
+    bool is_theorem = (k & 8) != 0;
+    name n          = read_name(d);
+    param_names ps  = read_params(d);
+    expr t          = read_expr(d);
+    if (has_value) {
+        expr v      = read_expr(d);
+        if (is_theorem) {
+            return mk_theorem(n, ps, t, v);
+        } else {
+            unsigned w        = d.read_unsigned();
+            bool is_opaque    = (k & 2) != 0;
+            bool use_conv_opt = (k & 4) != 0;
+            return mk_definition(n, ps, t, v, is_opaque, w, module_idx, use_conv_opt);
+        }
+    } else {
+        if (is_theorem)
+            return mk_axiom(n, ps, t);
+        else
+            return mk_var_decl(n, ps, t);
+    }
+}
+}
diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h
new file mode 100644
index 000000000..7bf85c1e3
--- /dev/null
+++ b/src/library/kernel_serializer.h
@@ -0,0 +1,30 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/serializer.h"
+#include "kernel/definition.h"
+
+namespace lean {
+serializer & operator<<(serializer & s, level const & l);
+level read_level(deserializer & d);
+inline deserializer & operator>>(deserializer & d, level & l) { l = read_level(d); return d; }
+
+serializer & operator<<(serializer & s, levels const & ls);
+levels read_levels(deserializer & d);
+
+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; }
+
+serializer & operator<<(serializer & s, definition const & d);
+definition read_definition(deserializer & d, unsigned module_idx);
+
+void register_macro_deserializer(std::string const & k, macro_definition_cell::reader rd);
+struct register_macro_deserializer_fn {
+    register_macro_deserializer_fn(std::string const & k, macro_definition_cell::reader rd) { register_macro_deserializer(k, rd); }
+};
+}
diff --git a/src/library/resolve_macro.cpp b/src/library/resolve_macro.cpp
index 01856981a..f1ec6c7dc 100644
--- a/src/library/resolve_macro.cpp
+++ b/src/library/resolve_macro.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/free_vars.h"
 #include "library/kernel_bindings.h"
+#include "library/kernel_serializer.h"
 #include "library/bin_app.h"
 
 namespace lean {
@@ -288,7 +289,7 @@ expr mk_resolve_macro(expr const & l, expr const & H1, expr const & H2) {
     return mk_macro(g_resolve_macro_definition, 3, args);
 }
 
-macro_definition_cell::register_deserializer_fn
+register_macro_deserializer_fn
 resolve_macro_des_fn(g_resolve_opcode,
                      [](deserializer &, unsigned num, expr const * args) {
                          if (num != 3)
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index a4dc14b38..b47521231 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/max_sharing.h"
+#include "library/kernel_serializer.h"
 using namespace lean;
 
 static void check_serializer(expr const & e) {
diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp
index c507091fd..929a83abc 100644
--- a/src/tests/kernel/level.cpp
+++ b/src/tests/kernel/level.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/exception.h"
 #include "kernel/level.h"
+#include "library/kernel_serializer.h"
 using namespace lean;
 
 static void check_serializer(level const & l) {