diff --git a/.gitignore b/.gitignore
index 0c55b4fcf..c04896fe9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,4 +5,5 @@ build
 GPATH
 GRTAGS
 GSYMS
-GTAGS
\ No newline at end of file
+GTAGS
+Makefile
\ No newline at end of file
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index f717554ec..af6c71651 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -45,6 +45,7 @@ include_directories(${LEAN_SOURCE_DIR}/util)
 include_directories(${LEAN_SOURCE_DIR}/numerics)
 include_directories(${LEAN_SOURCE_DIR}/interval)
 include_directories(${LEAN_SOURCE_DIR}/sexpr)
+include_directories(${LEAN_SOURCE_DIR}/kernel)
 
 add_subdirectory(util)
 set(EXTRA_LIBS ${EXTRA_LIBS} util)
@@ -54,9 +55,12 @@ add_subdirectory(sexpr)
 set(EXTRA_LIBS ${EXTRA_LIBS} sexpr)
 add_subdirectory(interval)
 set(EXTRA_LIBS ${EXTRA_LIBS} interval)
+add_subdirectory(kernel)
+set(EXTRA_LIBS ${EXTRA_LIBS} kernel)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
 add_subdirectory(shell)
 add_subdirectory(tests/util)
 add_subdirectory(tests/numerics)
 add_subdirectory(tests/interval)
 add_subdirectory(tests/sexpr)
+add_subdirectory(tests/kernel)
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
new file mode 100644
index 000000000..86a769aca
--- /dev/null
+++ b/src/kernel/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_library(kernel expr.cpp)
+target_link_libraries(kernel ${EXTRA_LIBS})
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
new file mode 100644
index 000000000..c867151d1
--- /dev/null
+++ b/src/kernel/expr.cpp
@@ -0,0 +1,236 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <vector>
+#include "expr.h"
+#include "expr_set.h"
+#include "hash.h"
+
+namespace lean {
+
+unsigned hash_args(unsigned size, expr const * args) {
+    return hash(size, [&args](unsigned i){ return args[i].hash(); });
+}
+
+unsigned hash_vars(unsigned size, uvar const * vars) {
+    return hash(size, [&vars](unsigned i){ return vars[i].second.hash(); });
+}
+
+expr_cell::expr_cell(expr_kind k, unsigned h):
+    m_kind(k),
+    m_hash(h),
+    m_rc(1) {}
+
+expr_var::expr_var(unsigned idx):
+    expr_cell(expr_kind::Var, idx),
+    m_vidx(idx) {}
+
+expr_const::expr_const(name const & n, unsigned pos):
+    expr_cell(expr_kind::Constant, m_name.hash()),
+    m_name(n),
+    m_pos(pos) {}
+
+expr_app::expr_app(unsigned num_args):
+    expr_cell(expr_kind::App, 0),
+    m_num_args(num_args) {
+}
+expr_app::~expr_app() {
+    for (unsigned i = 0; i < m_num_args; i++)
+        (m_args+i)->~expr();
+}
+expr app(unsigned num_args, expr const * args) {
+    lean_assert(num_args > 1);
+    unsigned _num_args;
+    unsigned _num_args0;
+    expr const & arg0 = args[0];
+    // Remark: we represet ((app a b) c) as (app a b c)
+    if (is_app(arg0)) {
+        _num_args0 = get_num_args(arg0);
+        _num_args  = num_args + _num_args0 - 1;
+    }
+    else {
+        _num_args = num_args;
+    }
+    char * mem   = new char[sizeof(expr_app) + _num_args*sizeof(expr)];
+    expr r(new (mem) expr_app(_num_args));
+    expr * m_args = to_app(r)->m_args;
+    unsigned i = 0;
+    unsigned j = 0;
+    if (_num_args != num_args) {
+        for (; i < _num_args0; i++)
+            new (m_args+i) expr(get_arg(arg0, i));
+        j++;
+    }
+    for (; i < _num_args; ++i, ++j) {
+        lean_assert(j < num_args);
+        new (m_args+i) expr(args[j]);
+    }
+    to_app(r)->m_hash = hash_args(_num_args, m_args);
+    return r;
+}
+
+expr_abstraction::expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e):
+    expr_cell(k, ::lean::hash(t.hash(), e.hash())),
+    m_name(n),
+    m_type(t),
+    m_expr(e) {
+}
+expr_lambda::expr_lambda(name const & n, expr const & t, expr const & e):
+    expr_abstraction(expr_kind::Lambda, n, t, e) {}
+expr_pi::expr_pi(name const & n, expr const & t, expr const & e):
+    expr_abstraction(expr_kind::Pi, n, t, e) {}
+
+expr_type::expr_type(unsigned size, uvar const * vars):
+    expr_cell(expr_kind::Type, hash_vars(size, vars)),
+    m_size(size) {
+    for (unsigned i = 0; i < m_size; i++)
+        new (m_vars + i) uvar(vars[i]);
+}
+expr_type::~expr_type() {
+    for (unsigned i = 0; i < m_size; i++)
+        (m_vars+i)->~uvar();
+}
+expr type(unsigned size, uvar const * vars) {
+    char * mem = new char[sizeof(expr_type) + size*sizeof(uvar)];
+    return expr(new (mem) expr_type(size, vars));
+}
+
+expr_numeral::expr_numeral(mpz const & n):
+    expr_cell(expr_kind::Numeral, n.hash()),
+    m_numeral(n) {}
+
+void expr_cell::dealloc() {
+    switch (m_kind) {
+    case expr_kind::Var:        delete static_cast<expr_var*>(this); break;
+    case expr_kind::Constant:   delete static_cast<expr_const*>(this); break;
+    case expr_kind::App:        static_cast<expr_app*>(this)->~expr_app(); delete[] reinterpret_cast<char*>(this); break;
+    case expr_kind::Lambda:     delete static_cast<expr_lambda*>(this); break;
+    case expr_kind::Pi:         delete static_cast<expr_pi*>(this); break;
+    case expr_kind::Prop:       delete static_cast<expr_prop*>(this); break;
+    case expr_kind::Type:       static_cast<expr_type*>(this)->~expr_type(); delete[] reinterpret_cast<char*>(this); break;
+    case expr_kind::Numeral:    delete static_cast<expr_numeral*>(this); break;
+    }
+}
+
+bool operator==(expr const & a, expr const & b) {
+    if (eqp(a, b))
+        return true;
+    if (a.hash() != b.hash() || a.kind() != b.kind())
+        return false;
+    static thread_local std::vector<expr_cell_pair> todo;
+    static thread_local expr_cell_pair_set visited;
+    auto visit = [&](expr_cell * a, expr_cell * b) -> bool {
+        if (a == b)
+            return true;
+        if (a->hash() != b->hash())
+            return false;
+        if (a->kind() != b->kind())
+            return false;
+        if (a->kind() == expr_kind::Prop)
+            return true;
+        if (a->kind() == expr_kind::Var)
+            return get_var_idx(a) == get_var_idx(b);
+        expr_cell_pair p(a, b);
+        if (visited.find(p) != visited.end())
+            return true;
+        todo.push_back(p);
+        visited.insert(p);
+        return true;
+    };
+    todo.clear();
+    visited.clear();
+    visit(a.raw(), b.raw());
+    while (!todo.empty()) {
+        auto p = todo.back();
+        expr_cell * a = p.first;
+        expr_cell * b = p.second;
+        todo.pop_back();
+        lean_assert(a != b);
+        lean_assert(a->hash() == b->hash());
+        lean_assert(a->kind() == b->kind());
+        switch (a->kind()) {
+        case expr_kind::Var:
+            lean_unreachable();
+            break;
+        case expr_kind::Constant:
+            if (get_const_name(a) != get_const_name(b))
+                return false;
+            break;
+        case expr_kind::App:
+            if (get_num_args(a) != get_num_args(b))
+                return false;
+            for (unsigned i = 0; i < get_num_args(a); i++) {
+                if (!visit(get_arg(a, i).raw(), get_arg(b, i).raw()))
+                    return false;
+            }
+            break;
+        case expr_kind::Lambda:
+        case expr_kind::Pi:
+            // Lambda and Pi
+            // Remark: we ignore get_abs_name because we want alpha-equivalence
+            if (!visit(get_abs_type(a).raw(), get_abs_type(b).raw()) ||
+                !visit(get_abs_expr(a).raw(), get_abs_expr(b).raw()))
+                return false;
+            break;
+        case expr_kind::Prop:
+            lean_unreachable();
+            break;
+        case expr_kind::Type:
+            if (get_ty_num_vars(a) != get_ty_num_vars(b))
+                return false;
+            for (unsigned i = 0; i < get_ty_num_vars(a); i++) {
+                uvar v1 = get_ty_var(a, i);
+                uvar v2 = get_ty_var(b, i);
+                if (v1.first != v2.first || v1.second != v2.second)
+                    return false;
+            }
+            break;
+        case expr_kind::Numeral:
+            if (get_numeral(a) != get_numeral(b))
+                return false;
+            break;
+        }
+    }
+    return true;
+}
+
+// Low-level pretty printer
+std::ostream & operator<<(std::ostream & out, expr const & a) {
+    switch (a.kind()) {
+    case expr_kind::Var:
+        out << "#" << get_var_idx(a);
+        break;
+    case expr_kind::Constant:
+        out << get_const_name(a);
+        break;
+    case expr_kind::App:
+        out << "(";
+        for (unsigned i = 0; i < get_num_args(a); i++) {
+            if (i > 0) out << " ";
+            out << get_arg(a, i);
+        }
+        out << ")";
+        break;
+    case expr_kind::Lambda:
+        out << "(fun (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")";
+        break;
+    case expr_kind::Pi:
+        out << "(forall (" << get_abs_name(a) << " : " << get_abs_type(a) << ") " << get_abs_expr(a) << ")";
+        break;
+    case expr_kind::Prop:
+        out << "Prop";
+        break;
+    case expr_kind::Type:
+        out << "Type";
+        break;
+    case expr_kind::Numeral:
+        out << get_numeral(a);
+        break;
+    }
+    return out;
+}
+
+}
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
new file mode 100644
index 000000000..df912f869
--- /dev/null
+++ b/src/kernel/expr.h
@@ -0,0 +1,293 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <iostream>
+#include <limits>
+#include "name.h"
+#include "rc.h"
+#include "mpz.h"
+
+namespace lean {
+/* =======================================
+   Expressions
+   expr ::=   Var      idx
+          |   Constant name
+          |   App      [expr]
+          |   Lambda   name expr expr
+          |   Pi       name expr expr
+          |   Prop
+          |   Type     universe
+          |   Numeral  value
+
+TODO: add meta-variables, let, constructor references and match.
+
+The main API is divided in the following sections
+- Testers
+- Constructors
+- Accessors
+- Miscellaneous
+======================================= */
+enum class expr_kind { Var, Constant, App, Lambda, Pi, Prop, Type, Numeral };
+
+/**
+    \brief Base class used to represent expressions.
+
+    In principle, the expr_cell class and subclasses should be located in the .cpp file.
+    However, this is performance critical code, and we want to be able to have
+    inline definitions.
+*/
+class expr_cell {
+protected:
+    expr_kind m_kind;
+    unsigned  m_hash;
+    MK_LEAN_RC(); // Declare m_rc counter
+    void dealloc();
+public:
+    expr_cell(expr_kind k, unsigned h);
+    expr_kind kind() const { return m_kind; }
+    unsigned  hash() const { return m_hash; }
+};
+
+/**
+   \brief Instead of fixed universes, we use universe variables with
+   explicit user-declared constraints between universe variables.
+
+   Each universe variable is associated with a name.
+
+   If the Boolean in the following pair is true, then we are taking
+   the successor of the universe variable.
+
+   For additional information, see:
+   Explicit universes for the calculus of constructions, Courant J (2002).
+*/
+typedef std::pair<bool, name> universe_variable;
+typedef universe_variable uvar;
+
+/**
+   \brief Exprs for encoding formulas/expressions, types and proofs.
+*/
+class expr {
+private:
+    expr_cell * m_ptr;
+    explicit expr(expr_cell * ptr):m_ptr(ptr) {}
+public:
+    expr():m_ptr(0) {}
+    expr(expr const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    expr(expr && s):m_ptr(s.m_ptr) { s.m_ptr = 0; }
+    ~expr() { if (m_ptr) m_ptr->dec_ref(); }
+
+    friend void swap(expr & a, expr & b) { std::swap(a.m_ptr, b.m_ptr); }
+
+    expr & operator=(expr const & s) {
+        if (s.m_ptr)
+            s.m_ptr->inc_ref();
+        if (m_ptr)
+            m_ptr->dec_ref();
+        m_ptr = s.m_ptr;
+        return *this;
+    }
+    expr & operator=(expr && s) {
+        if (m_ptr)
+            m_ptr->dec_ref();
+        m_ptr = s.m_ptr;
+        s.m_ptr = 0;
+        return *this;
+    }
+
+    expr_kind kind() const { return m_ptr->kind(); }
+    unsigned  hash() const { return m_ptr->hash(); }
+
+    expr_cell * raw() const { return m_ptr; }
+
+    friend expr var(unsigned idx);
+    friend expr constant(name const & n);
+    friend expr constant(name const & n, unsigned pos);
+    friend expr app(unsigned num_args, expr const * args);
+    friend expr app(std::initializer_list<expr> const & l);
+    friend expr lambda(name const & n, expr const & t, expr const & e);
+    friend expr pi(name const & n, expr const & t, expr const & e);
+    friend expr prop();
+    friend expr type(unsigned size, uvar const * vars);
+    friend expr type(std::initializer_list<uvar> const & l);
+    friend expr numeral(mpz const & n);
+
+    friend bool eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
+};
+
+// =======================================
+// Expr Representation
+// 1. Free variables
+class expr_var : public expr_cell {
+    unsigned m_vidx; // de Bruijn index
+public:
+    expr_var(unsigned idx);
+    unsigned get_vidx() const { return m_vidx; }
+};
+// 2. Constants
+class expr_const : public expr_cell {
+    name     m_name;
+    unsigned m_pos;  // position in the environment.
+public:
+    expr_const(name const & n, unsigned pos = std::numeric_limits<unsigned>::max());
+    name const & get_name() const { return m_name; }
+    unsigned     get_pos() const { return m_pos; }
+};
+// 3. Applications
+class expr_app : public expr_cell {
+    unsigned m_num_args;
+    expr     m_args[0];
+    friend expr app(unsigned num_args, expr const * args);
+public:
+    expr_app(unsigned size);
+    ~expr_app();
+    unsigned     get_num_args() const        { return m_num_args; }
+    expr const & get_arg(unsigned idx) const { lean_assert(idx < m_num_args); return m_args[idx]; }
+};
+// 4. Abstraction
+class expr_abstraction : public expr_cell {
+    name     m_name;
+    expr     m_type;
+    expr     m_expr;
+public:
+    expr_abstraction(expr_kind k, name const & n, expr const & t, expr const & e);
+    name const & get_name() const { return m_name; }
+    expr const & get_type() const { return m_type; }
+    expr const & get_expr() const { return m_expr; }
+};
+// 5. Lambda
+class expr_lambda : public expr_abstraction {
+public:
+    expr_lambda(name const & n, expr const & t, expr const & e);
+};
+// 6. Pi
+class expr_pi : public expr_abstraction {
+public:
+    expr_pi(name const & n, expr const & t, expr const & e);
+};
+// 7. Prop
+class expr_prop : public expr_cell {
+public:
+    expr_prop():expr_cell(expr_kind::Prop, 17) {}
+};
+// 8. Type lvl
+class expr_type : public expr_cell {
+    unsigned m_size;
+    uvar     m_vars[0];
+public:
+    expr_type(unsigned size, uvar const * vars);
+    ~expr_type();
+    unsigned size() const { return m_size; }
+    uvar const & get_var(unsigned idx) const { lean_assert(idx < m_size); return m_vars[idx]; }
+};
+// 9. Numerals
+class expr_numeral : public expr_cell {
+    mpz   m_numeral;
+public:
+    expr_numeral(mpz const & n);
+    mpz const & get_num() const { return m_numeral; }
+};
+// =======================================
+
+// =======================================
+// Testers
+inline bool is_var(expr_cell * e)         { return e->kind() == expr_kind::Var; }
+inline bool is_constant(expr_cell * e)    { return e->kind() == expr_kind::Constant; }
+inline bool is_app(expr_cell * e)         { return e->kind() == expr_kind::App; }
+inline bool is_lambda(expr_cell * e)      { return e->kind() == expr_kind::Lambda; }
+inline bool is_pi(expr_cell * e)          { return e->kind() == expr_kind::Pi; }
+inline bool is_prop(expr_cell * e)        { return e->kind() == expr_kind::Prop; }
+inline bool is_type(expr_cell * e)        { return e->kind() == expr_kind::Type; }
+inline bool is_numeral(expr_cell * e)     { return e->kind() == expr_kind::Numeral; }
+inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); }
+inline bool is_sort(expr_cell * e)        { return is_prop(e) || is_type(e); }
+
+inline bool is_var(expr const & e)         { return e.kind() == expr_kind::Var; }
+inline bool is_constant(expr const & e)    { return e.kind() == expr_kind::Constant; }
+inline bool is_app(expr const & e)         { return e.kind() == expr_kind::App; }
+inline bool is_lambda(expr const & e)      { return e.kind() == expr_kind::Lambda; }
+inline bool is_pi(expr const & e)          { return e.kind() == expr_kind::Pi; }
+inline bool is_prop(expr const & e)        { return e.kind() == expr_kind::Prop; }
+inline bool is_type(expr const & e)        { return e.kind() == expr_kind::Type; }
+inline bool is_numeral(expr const & e)     { return e.kind() == expr_kind::Numeral; }
+inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
+inline bool is_sort(expr const & e)        { return is_prop(e) || is_type(e); }
+// =======================================
+
+// =======================================
+// Constructors
+inline expr var(unsigned idx) { return expr(new expr_var(idx)); }
+inline expr constant(name const & n) { return expr(new expr_const(n)); }
+inline expr constant(name const & n, unsigned pos) { return expr(new expr_const(n, pos)); }
+       expr app(unsigned num_args, expr const * args);
+inline expr app(std::initializer_list<expr> const & l) { return app(l.size(), l.begin()); }
+inline expr lambda(name const & n, expr const & t, expr const & e) { return expr(new expr_lambda(n, t, e)); }
+inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new expr_pi(n, t, e)); }
+inline expr prop() { return expr(new expr_prop()); }
+       expr type(unsigned size, uvar const * vars);
+inline expr type(std::initializer_list<uvar> const & l) { return type(l.size(), l.begin()); }
+inline expr numeral(mpz const & n) { return expr(new expr_numeral(n)); }
+// =======================================
+
+// =======================================
+// Casting
+inline expr_var *         to_var(expr_cell * e)         { lean_assert(is_var(e));         return static_cast<expr_var*>(e); }
+inline expr_const *       to_constant(expr_cell * e)    { lean_assert(is_constant(e));    return static_cast<expr_const*>(e); }
+inline expr_app *         to_app(expr_cell * e)         { lean_assert(is_app(e));         return static_cast<expr_app*>(e); }
+inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstraction(e)); return static_cast<expr_abstraction*>(e); }
+inline expr_lambda *      to_lambda(expr_cell * e)      { lean_assert(is_lambda(e));      return static_cast<expr_lambda*>(e); }
+inline expr_pi *          to_pi(expr_cell * e)          { lean_assert(is_pi(e));          return static_cast<expr_pi*>(e); }
+inline expr_prop *        to_prop(expr_cell * e)        { lean_assert(is_prop(e));        return static_cast<expr_prop*>(e); }
+inline expr_type *        to_type(expr_cell * e)        { lean_assert(is_type(e));        return static_cast<expr_type*>(e); }
+inline expr_numeral *     to_numeral(expr_cell * e)     { lean_assert(is_numeral(e));     return static_cast<expr_numeral*>(e); }
+
+inline expr_var *         to_var(expr const & e)         { return to_var(e.raw()); }
+inline expr_const *       to_constant(expr const & e)    { return to_constant(e.raw()); }
+inline expr_app *         to_app(expr const & e)         { return to_app(e.raw()); }
+inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction(e.raw()); }
+inline expr_lambda *      to_lambda(expr const & e)      { return to_lambda(e.raw()); }
+inline expr_pi *          to_pi(expr const & e)          { return to_pi(e.raw()); }
+inline expr_prop *        to_prop(expr const & e)        { return to_prop(e.raw()); }
+inline expr_type *        to_type(expr const & e)        { return to_type(e.raw()); }
+inline expr_numeral *     to_numeral(expr const & e)     { return to_numeral(e.raw()); }
+// =======================================
+
+// =======================================
+// Accessors
+inline unsigned     get_var_idx(expr_cell * e)              { return to_var(e)->get_vidx(); }
+inline name const & get_const_name(expr_cell * e)           { return to_constant(e)->get_name(); }
+inline unsigned     get_const_pos(expr_cell * e)            { return to_constant(e)->get_pos(); }
+inline unsigned     get_num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
+inline expr const & get_arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
+inline name const & get_abs_name(expr_cell * e)             { return to_abstraction(e)->get_name(); }
+inline expr const & get_abs_type(expr_cell * e)             { return to_abstraction(e)->get_type(); }
+inline expr const & get_abs_expr(expr_cell * e)             { return to_abstraction(e)->get_expr(); }
+inline unsigned     get_ty_num_vars(expr_cell * e)          { return to_type(e)->size(); }
+inline uvar const & get_ty_var(expr_cell * e, unsigned idx) { return to_type(e)->get_var(idx); }
+inline mpz const &  get_numeral(expr_cell * e)              { return to_numeral(e)->get_num(); }
+
+inline unsigned     get_var_idx(expr const & e)              { return to_var(e)->get_vidx(); }
+inline name const & get_const_name(expr const & e)           { return to_constant(e)->get_name(); }
+inline unsigned     get_const_pos(expr const & e)            { return to_constant(e)->get_pos(); }
+inline unsigned     get_num_args(expr const & e)             { return to_app(e)->get_num_args(); }
+inline expr const & get_arg(expr const & e, unsigned idx)    { return to_app(e)->get_arg(idx); }
+inline name const & get_abs_name(expr const & e)             { return to_abstraction(e)->get_name(); }
+inline expr const & get_abs_type(expr const & e)             { return to_abstraction(e)->get_type(); }
+inline expr const & get_abs_expr(expr const & e)             { return to_abstraction(e)->get_expr(); }
+inline unsigned     get_ty_num_vars(expr const & e)          { return to_type(e)->size(); }
+inline uvar const & get_ty_var(expr const & e, unsigned idx) { return to_type(e)->get_var(idx); }
+inline mpz const &  get_numeral(expr const & e)              { return to_numeral(e)->get_num(); }
+// =======================================
+
+// =======================================
+// Structural equality
+       bool operator==(expr const & a, expr const & b);
+inline bool operator!=(expr const & a, expr const & b) { return !operator==(a, b); }
+// =======================================
+
+std::ostream & operator<<(std::ostream & out, expr const & a);
+
+}
diff --git a/src/kernel/expr_set.h b/src/kernel/expr_set.h
new file mode 100644
index 000000000..0e7d7d7ef
--- /dev/null
+++ b/src/kernel/expr_set.h
@@ -0,0 +1,60 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <unordered_set>
+#include "expr.h"
+#include "hash.h"
+
+namespace lean {
+
+// =======================================
+// Expression Set
+// Remark: to expressions are assumed to be equal if they are "pointer-equal"
+struct expr_hash {
+    unsigned operator()(expr const & e) const { return e.hash(); }
+};
+struct expr_eqp {
+    bool operator()(expr const & e1, expr const & e2) const { return eqp(e1, e2); }
+};
+typedef std::unordered_set<expr, expr_hash, expr_eqp> expr_set;
+// =======================================
+
+// =======================================
+// (low level) Expression Cell Set
+// Remark: to expressions are assumed to be equal if they are "pointer-equal"
+//
+// WARNING: use with care, this kind of set
+// does not prevent an expression from being
+// garbage collected.
+struct expr_cell_hash {
+    unsigned operator()(expr_cell * e) const { return e->hash(); }
+};
+struct expr_cell_eqp {
+    bool operator()(expr_cell * e1, expr_cell * e2) const { return e1 == e2; }
+};
+typedef std::unordered_set<expr_cell*, expr_cell_hash, expr_cell_eqp> expr_cell_set;
+// =======================================
+
+// =======================================
+// (low level) Expression Cell pair Set
+// Remark: to expressions are assumed to be equal if they are "pointer-equal"
+//
+// WARNING: use with care, this kind of set
+// does not prevent an expression from being
+// garbage collected.
+typedef std::pair<expr_cell *, expr_cell *> expr_cell_pair;
+struct expr_cell_pair_hash {
+    unsigned operator()(expr_cell_pair const & p) const { return hash(p.first->hash(), p.second->hash()); }
+};
+struct expr_cell_pair_eqp {
+    bool operator()(expr_cell_pair const & p1, expr_cell_pair const & p2) const {
+        return p1.first == p2.first && p1.second == p2.second;
+    }
+};
+typedef std::unordered_set<expr_cell_pair, expr_cell_pair_hash, expr_cell_pair_eqp> expr_cell_pair_set;
+// =======================================
+}
diff --git a/src/util/hash.h b/src/util/hash.h
index 0e95a2f3f..9d4ddfe5a 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -5,9 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "debug.h"
 
 namespace lean {
 
+void mix(unsigned & a, unsigned & b, unsigned & c);
+
 unsigned hash(char const * str, unsigned length, unsigned init_value);
 
 inline unsigned hash(unsigned h1, unsigned h2) {
@@ -17,4 +20,54 @@ inline unsigned hash(unsigned h1, unsigned h2) {
     return h2;
 }
 
+template<typename H>
+unsigned hash(unsigned n, H h, unsigned init_value = 31) {
+    unsigned a, b, c;
+    lean_assert(n > 0);
+
+    a = b = 0x9e3779b9;
+    c = 11;
+
+    switch (n) {
+    case 1:
+        a += init_value;
+        b  = h(0);
+        mix(a, b, c);
+        return c;
+    case 2:
+        a += init_value;
+        b += h(0);
+        c += h(1);
+        mix(a, b, c);
+        return c;
+    case 3:
+        a += h(0);
+        b += h(1);
+        c += h(2);
+        mix(a, b, c);
+        a += init_value;
+        mix(a, b, c);
+        return c;
+    default:
+        while (n >= 3) {
+            n--;
+            a += h(n);
+            n--;
+            b += h(n);
+            n--;
+            c += h(n);
+            mix(a, b, c);
+        }
+
+        a += init_value;
+        switch (n) {
+        case 2: b += h(1);
+        case 1: c += h(0);
+        }
+        mix(a, b, c);
+        return c;
+    }
+}
+
+
 }
diff --git a/src/util/rc.h b/src/util/rc.h
index d60776bb2..1ffdc59df 100644
--- a/src/util/rc.h
+++ b/src/util/rc.h
@@ -12,7 +12,9 @@ Author: Leonardo de Moura
 
 #ifdef LEAN_THREAD_UNSAFE_REF_COUNT
 #define MK_LEAN_RC()                                                    \
+private:                                                                \
 unsigned m_rc;                                                          \
+public:                                                                 \
 unsigned get_rc() const { return m_rc; }                                \
 void inc_ref() { m_rc++; }                                              \
 bool dec_ref_core() { lean_assert(get_rc() > 0);  m_rc--; return m_rc == 0; } \
@@ -20,7 +22,9 @@ void dec_ref() { if (dec_ref_core()) dealloc(); }
 #else
 #include <atomic>
 #define MK_LEAN_RC()                                                    \
+private:                                                                \
 std::atomic<unsigned> m_rc;                                             \
+public:                                                                 \
 unsigned get_rc() const { return std::atomic_load(&m_rc); }             \
 void inc_ref() { std::atomic_fetch_add_explicit(&m_rc, 1u, std::memory_order_relaxed); } \
 bool dec_ref_core() { lean_assert(get_rc() > 0); return std::atomic_fetch_sub_explicit(&m_rc, 1u, std::memory_order_relaxed) == 1u; } \