diff --git a/library/meta/default.lean b/library/meta/default.lean
index 88de998a2c..e2838b27c4 100644
--- a/library/meta/default.lean
+++ b/library/meta/default.lean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import meta.name meta.options meta.format meta.rb_map
-import meta.level
+import meta.level meta.expr
diff --git a/library/meta/expr.lean b/library/meta/expr.lean
new file mode 100644
index 0000000000..cf045de7c6
--- /dev/null
+++ b/library/meta/expr.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import meta.level
+
+inductive binder_info :=
+| default | implicit | strict_implicit | inst_implicit | other
+
+meta_constant macro_def : Type₁
+
+/- Reflect a C++ expr object. The VM replaces it with the C++ implementation. -/
+inductive expr :=
+| var      : unsigned → expr
+| sort     : level → expr
+| const    : name → list level → expr
+| meta     : name → expr → expr
+| free_var : name → name → binder_info → expr → expr
+| app      : expr → expr → expr
+| lam      : name → binder_info → expr → expr → expr
+| pi       : name → binder_info → expr → expr → expr
+| elet     : name → expr → expr → expr → expr
+| macro    : macro_def → ∀ n : unsigned, (fin (unsigned.to_nat n) → expr) → expr
+
+meta_constant expr.mk_macro (d : macro_def) : list expr → expr
+meta_definition expr.mk_var (n : nat) : expr :=
+expr.var (unsigned.of_nat n)
+
+meta_constant expr.has_decidable_eq : decidable_eq expr
+attribute [instance] expr.has_decidable_eq
+meta_constant expr.alpha_eqv : expr → expr → bool
+notation a ` =ₐ `:50 b:50 := expr.alpha_eqv a b = bool.tt
+
+meta_constant expr.to_string : expr → string
+meta_definition expr.has_to_string [instance] : has_to_string expr :=
+has_to_string.mk expr.to_string
+
+meta_constant expr.lt : expr → expr → bool
+meta_constant expr.lex_lt : expr → expr → bool
+meta_definition expr.cmp (a b : expr) : cmp_result :=
+if expr.lt a b = bool.tt then cmp_result.lt
+else if a = b then cmp_result.eq
+else cmp_result.gt
+
+meta_constant expr.fold {A :Type} : expr → A → (expr → unsigned → A → A) → A
+
+meta_constant expr.abstract_fv  : expr → name → expr
+meta_constant expr.abstract_fvs : expr → list name → expr
+
+meta_constant expr.instantiate_var  : expr → expr → expr
+meta_constant expr.instantiate_vars : expr → list expr → expr
diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt
index 028d52428b..dbb3799d00 100644
--- a/src/library/vm/CMakeLists.txt
+++ b/src/library/vm/CMakeLists.txt
@@ -1,2 +1,3 @@
-add_library(vm OBJECT vm.cpp vm_nat.cpp vm_string.cpp vm_io.cpp vm_name.cpp vm_options.cpp
-  vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_aux.cpp optimize.cpp init_module.cpp)
\ No newline at end of file
+add_library(vm OBJECT vm.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
+  vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp
+  optimize.cpp init_module.cpp)
\ No newline at end of file
diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp
index e82f9d5077..14efe18661 100644
--- a/src/library/vm/init_module.cpp
+++ b/src/library/vm/init_module.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_format.h"
 #include "library/vm/vm_rb_map.h"
 #include "library/vm/vm_level.h"
+#include "library/vm/vm_expr.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -25,8 +26,10 @@ void initialize_vm_core_module() {
     initialize_vm_format();
     initialize_vm_rb_map();
     initialize_vm_level();
+    initialize_vm_expr();
 }
 void finalize_vm_core_module() {
+    finalize_vm_expr();
     finalize_vm_level();
     finalize_vm_rb_map();
     finalize_vm_format();
@@ -40,6 +43,7 @@ void finalize_vm_core_module() {
 
 void initialize_vm_module() {
     initialize_vm();
+    initialize_vm_expr_builtin_idxs();
 }
 void finalize_vm_module() {
     finalize_vm();
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index a83b1db27a..70179dd808 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -54,6 +54,25 @@ vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * data) {
     return mk_vm_composite(vm_obj_kind::Constructor, cidx, sz, data);
 }
 
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1) {
+    return mk_vm_constructor(cidx, 1, &o1);
+}
+
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2) {
+    vm_obj args[2] = {o1, o2};
+    return mk_vm_constructor(cidx, 2, args);
+}
+
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm_obj const & o3) {
+    vm_obj args[3] = {o1, o2, o3};
+    return mk_vm_constructor(cidx, 3, args);
+}
+
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm_obj const & o3, vm_obj const & o4) {
+    vm_obj args[4] = {o1, o2, o3, o4};
+    return mk_vm_constructor(cidx, 4, args);
+}
+
 vm_obj mk_vm_closure(unsigned fn_idx, unsigned sz, vm_obj const * data) {
     return mk_vm_composite(vm_obj_kind::Closure, fn_idx, sz, data);
 }
@@ -734,8 +753,12 @@ struct vm_decls : public environment_extension {
 };
 
 struct vm_decls_reg {
-    unsigned m_ext_id;
-    vm_decls_reg() { m_ext_id = environment::register_extension(std::make_shared<vm_decls>()); }
+    std::shared_ptr<vm_decls> m_init_decls;
+    unsigned                  m_ext_id;
+    vm_decls_reg() {
+        m_init_decls = std::make_shared<vm_decls>();
+        m_ext_id     = environment::register_extension(m_init_decls);
+    }
 };
 
 static vm_decls_reg * g_ext = nullptr;
@@ -811,6 +834,14 @@ optional<unsigned> get_vm_constant_idx(environment const & env, name const & n)
         return optional<unsigned>();
 }
 
+optional<unsigned> get_vm_builtin_idx(name const & n) {
+    lean_assert(g_ext);
+    if (auto r = g_ext->m_init_decls->m_name2idx.find(n))
+        return optional<unsigned>(*r);
+    else
+        return optional<unsigned>();
+}
+
 static std::string * g_vm_reserve_key = nullptr;
 static std::string * g_vm_code_key = nullptr;
 
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 8df5aaacc0..4b80df77d3 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -132,6 +132,10 @@ public:
 // Constructors
 vm_obj mk_vm_simple(unsigned cidx);
 vm_obj mk_vm_constructor(unsigned cidx, unsigned sz, vm_obj const * args);
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &);
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &);
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_closure(unsigned fnidx, unsigned sz, vm_obj const * args);
 vm_obj mk_vm_mpz(mpz const & n);
 vm_obj mk_vm_external(vm_external * cell);
@@ -605,6 +609,10 @@ bool is_vm_function(environment const & env, name const & fn);
 
 optional<vm_decl> get_vm_decl(environment const & env, name const & n);
 
+/** \brief Return the function idx of a builtin function.
+    \remark This function must only be invoked after initialize_vm was invoked. */
+optional<unsigned> get_vm_builtin_idx(name const & fn);
+
 /** \brief Return true iff \c fn is implemented in C++. */
 bool is_vm_builtin_function(name const & fn);
 /** \brief Return the name of the C++ function that implements the builtin named \c fn.
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
new file mode 100644
index 0000000000..dfa0f78f8f
--- /dev/null
+++ b/src/library/vm/vm_expr.cpp
@@ -0,0 +1,267 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include <iostream>
+#include "kernel/expr.h"
+#include "library/expr_lt.h"
+#include "library/vm/vm.h"
+#include "library/vm/vm_nat.h"
+#include "library/vm/vm_string.h"
+#include "library/vm/vm_name.h"
+#include "library/vm/vm_format.h"
+#include "library/vm/vm_options.h"
+#include "library/vm/vm_level.h"
+
+namespace lean {
+struct vm_macro_definition : public vm_external {
+    macro_definition m_val;
+    vm_macro_definition(macro_definition const & v):m_val(v) {}
+    virtual ~vm_macro_definition() {}
+};
+
+macro_definition const & to_macro_definition(vm_obj const & o) {
+    lean_assert(is_external(o));
+    lean_assert(dynamic_cast<vm_macro_definition*>(to_external(o)));
+    return static_cast<vm_macro_definition*>(to_external(o))->m_val;
+}
+
+vm_obj to_obj(macro_definition const & d) {
+    return mk_vm_external(new vm_macro_definition(d));
+}
+
+struct vm_expr : public vm_external {
+    expr m_val;
+    vm_expr(expr const & v):m_val(v) {}
+    virtual ~vm_expr() {}
+};
+
+expr const & to_expr(vm_obj const & o) {
+    lean_assert(is_external(o));
+    lean_assert(dynamic_cast<vm_expr*>(to_external(o)));
+    return static_cast<vm_expr*>(to_external(o))->m_val;
+}
+
+vm_obj to_obj(expr const & e) {
+    return mk_vm_external(new vm_expr(e));
+}
+
+list<expr> to_list_expr(vm_obj const & o) {
+    if (is_simple(o))
+        return list<expr>();
+    else
+        return list<expr>(to_expr(cfield(o, 0)), to_list_expr(cfield(o, 1)));
+}
+
+void to_buffer_expr(vm_obj const & o, buffer<expr> & r) {
+    if (is_simple(o)) {
+        return;
+    } else {
+        r.push_back(to_expr(cfield(o, 0)));
+        to_buffer_expr(cfield(o, 1), r);
+    }
+}
+
+vm_obj to_obj(buffer<expr> const & ls) {
+    vm_obj r = mk_vm_simple(0);
+    unsigned i = ls.size();
+    while (i > 0) {
+        --i;
+        r = mk_vm_constructor(1, to_obj(ls[i]), r);
+    }
+    return r;
+}
+
+vm_obj to_obj(list<expr> const & ls) {
+    buffer<expr> ls_buff;
+    to_buffer(ls, ls_buff);
+    return to_obj(ls_buff);
+}
+
+binder_info to_binder_info(vm_obj const & o) {
+    lean_assert(is_simple(o));
+    /*
+      inductive binder_info :=
+      | default | implicit | strict_implicit | inst_implicit | other
+    */
+    switch (cidx(o)) {
+    case 0:  return binder_info();
+    case 1:  return mk_implicit_binder_info();
+    case 2:  return mk_strict_implicit_binder_info();
+    case 3:  return mk_inst_implicit_binder_info();
+    default: return mk_rec_info(true);
+    }
+}
+
+vm_obj to_obj(binder_info const & bi) {
+    if (bi.is_implicit())
+        return mk_vm_simple(1);
+    else if (bi.is_strict_implicit())
+        return mk_vm_simple(2);
+    else if (bi.is_inst_implicit())
+        return mk_vm_simple(3);
+    else if (bi.is_rec())
+        return mk_vm_simple(4);
+    else
+        return mk_vm_simple(0);
+}
+
+vm_obj expr_var(vm_obj const & n) {
+    return to_obj(mk_var(to_unsigned(n)));
+}
+
+vm_obj expr_sort(vm_obj const & l) {
+    return to_obj(mk_sort(to_level(l)));
+}
+
+vm_obj expr_const(vm_obj const & n, vm_obj const & ls) {
+    return to_obj(mk_constant(to_name(n), to_list_level(ls)));
+}
+
+vm_obj expr_meta(vm_obj const & n, vm_obj const & t) {
+    return to_obj(mk_metavar(to_name(n), to_expr(t)));
+}
+
+vm_obj expr_free_var(vm_obj const & n, vm_obj const & ppn, vm_obj const & bi, vm_obj const & t) {
+    return to_obj(mk_local(to_name(n), to_name(ppn), to_expr(t), to_binder_info(bi)));
+}
+
+vm_obj expr_app(vm_obj const & f, vm_obj const & a) {
+    return to_obj(mk_app(to_expr(f), to_expr(a)));
+}
+
+vm_obj expr_lam(vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
+    return to_obj(mk_lambda(to_name(n), to_expr(t), to_expr(b), to_binder_info(bi)));
+}
+
+vm_obj expr_pi(vm_obj const & n, vm_obj const & bi, vm_obj const & t, vm_obj const & b) {
+    return to_obj(mk_pi(to_name(n), to_expr(t), to_expr(b), to_binder_info(bi)));
+}
+
+vm_obj expr_elet(vm_obj const & n, vm_obj const & t, vm_obj const & v, vm_obj const & b) {
+    return to_obj(mk_let(to_name(n), to_expr(t), to_expr(v), to_expr(b)));
+}
+
+vm_obj expr_macro(vm_obj const & d, vm_obj const & n, vm_obj const & fn) {
+    unsigned sz = to_unsigned(n);
+    buffer<expr> args;
+    for (unsigned i = 0; i < sz; i++) {
+        args.push_back(to_expr(invoke(fn, mk_vm_nat(i))));
+    }
+    return to_obj(mk_macro(to_macro_definition(d), args.size(), args.data()));
+}
+
+vm_obj expr_macro_arg(vm_obj const & m, vm_obj const & i) {
+    return to_obj(macro_arg(to_expr(m), to_unsigned(i)));
+}
+
+static unsigned g_expr_macro_arg_fun_idx = -1;
+
+unsigned expr_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
+    expr const & e = to_expr(o);
+    switch (e.kind()) {
+    case expr_kind::Var:
+        data.push_back(mk_vm_nat(var_idx(e)));
+        break;
+    case expr_kind::Sort:
+        data.push_back(to_obj(sort_level(e)));
+        break;
+    case expr_kind::Constant:
+        data.push_back(to_obj(const_name(e)));
+        data.push_back(to_obj(const_levels(e)));
+        break;
+    case expr_kind::Meta:
+        data.push_back(to_obj(mlocal_name(e)));
+        data.push_back(to_obj(mlocal_type(e)));
+        break;
+    case expr_kind::Local:
+        data.push_back(to_obj(mlocal_name(e)));
+        data.push_back(to_obj(local_pp_name(e)));
+        data.push_back(to_obj(local_info(e)));
+        data.push_back(to_obj(mlocal_type(e)));
+        break;
+    case expr_kind::App:
+        data.push_back(to_obj(app_fn(e)));
+        data.push_back(to_obj(app_arg(e)));
+        break;
+    case expr_kind::Lambda:
+    case expr_kind::Pi:
+        data.push_back(to_obj(binding_name(e)));
+        data.push_back(to_obj(binding_info(e)));
+        data.push_back(to_obj(binding_domain(e)));
+        data.push_back(to_obj(binding_body(e)));
+        break;
+    case expr_kind::Let:
+        data.push_back(to_obj(let_name(e)));
+        data.push_back(to_obj(let_type(e)));
+        data.push_back(to_obj(let_value(e)));
+        data.push_back(to_obj(let_body(e)));
+        break;
+    case expr_kind::Macro:
+        data.push_back(to_obj(macro_def(e)));
+        data.push_back(to_obj(macro_num_args(e)));
+        data.push_back(mk_vm_closure(g_expr_macro_arg_fun_idx, 1, &o));
+        break;
+    }
+    return static_cast<unsigned>(e.kind());
+}
+
+vm_obj expr_mk_macro(vm_obj const & d, vm_obj const & es) {
+    buffer<expr> args;
+    to_buffer_expr(es, args);
+    return to_obj(mk_macro(to_macro_definition(d), args.size(), args.data()));
+}
+
+vm_obj expr_has_decidable_eq(vm_obj const & o1, vm_obj const & o2) {
+    return mk_vm_bool(is_bi_equal(to_expr(o1), to_expr(o2)));
+}
+
+vm_obj expr_alpha_eqv(vm_obj const & o1, vm_obj const & o2) {
+    return mk_vm_bool(to_expr(o1) == to_expr(o2));
+}
+
+vm_obj expr_to_string(vm_obj const & l) {
+    std::ostringstream out;
+    out << to_expr(l);
+    return to_obj(out.str());
+}
+
+vm_obj expr_lt(vm_obj const & o1, vm_obj const & o2) {
+    return mk_vm_bool(is_lt(to_expr(o1), to_expr(o2), true));
+}
+
+vm_obj expr_lex_lt(vm_obj const & o1, vm_obj const & o2) {
+    return mk_vm_bool(is_lt(to_expr(o1), to_expr(o2), false));
+}
+
+void initialize_vm_expr() {
+    DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var);
+    DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort);
+    DECLARE_VM_BUILTIN(name({"expr", "const"}),            expr_const);
+    DECLARE_VM_BUILTIN(name({"expr", "meta"}),             expr_meta);
+    DECLARE_VM_BUILTIN(name({"expr", "free_var"}),         expr_free_var);
+    DECLARE_VM_BUILTIN(name({"expr", "app"}),              expr_app);
+    DECLARE_VM_BUILTIN(name({"expr", "lam"}),              expr_lam);
+    DECLARE_VM_BUILTIN(name({"expr", "pi"}),               expr_pi);
+    DECLARE_VM_BUILTIN(name({"expr", "elet"}),             expr_elet);
+    DECLARE_VM_BUILTIN("_expr_macro_arg",                  expr_macro_arg);
+    DECLARE_VM_BUILTIN(name({"expr", "macro"}),            expr_macro);
+    DECLARE_VM_BUILTIN(name({"expr", "mk_macro"}),         expr_mk_macro);
+    DECLARE_VM_BUILTIN(name({"expr", "has_decidable_eq"}), expr_has_decidable_eq);
+    DECLARE_VM_BUILTIN(name({"expr", "alpha_eqv"}),        expr_alpha_eqv);
+    DECLARE_VM_BUILTIN(name({"expr", "to_string"}),        expr_to_string);
+    DECLARE_VM_BUILTIN(name({"expr", "lt"}),               expr_lt);
+    DECLARE_VM_BUILTIN(name({"expr", "lex_lt"}),           expr_lex_lt);
+    DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}),   expr_cases_on);
+}
+
+void finalize_vm_expr() {
+}
+
+void initialize_vm_expr_builtin_idxs() {
+    g_expr_macro_arg_fun_idx = *get_vm_builtin_idx(name("_expr_macro_arg"));
+}
+}
diff --git a/src/library/vm/vm_expr.h b/src/library/vm/vm_expr.h
new file mode 100644
index 0000000000..9d4a381640
--- /dev/null
+++ b/src/library/vm/vm_expr.h
@@ -0,0 +1,26 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/vm/vm.h"
+#include "kernel/expr.h"
+
+namespace lean {
+binder_info to_binder_info(vm_obj const & o);
+vm_obj to_obj(binder_info const & bi);
+macro_definition const & to_macro_definition(vm_obj const & o);
+vm_obj to_obj(macro_definition const & d);
+expr const & to_expr(vm_obj const & o);
+vm_obj to_obj(expr const & e);
+list<expr> to_list_expr(vm_obj const & o);
+/* Given an object o : list expr, store its contents at \c r */
+void to_buffer_expr(vm_obj const & o, buffer<expr> & r);
+vm_obj to_obj(buffer<expr> const & ls);
+vm_obj to_obj(list<expr> const & ls);
+void initialize_vm_expr();
+void finalize_vm_expr();
+void initialize_vm_expr_builtin_idxs();
+}
diff --git a/src/library/vm/vm_level.cpp b/src/library/vm/vm_level.cpp
index 106a8407ff..147f91b5bb 100644
--- a/src/library/vm/vm_level.cpp
+++ b/src/library/vm/vm_level.cpp
@@ -30,6 +30,29 @@ vm_obj to_obj(level const & n) {
     return mk_vm_external(new vm_level(n));
 }
 
+list<level> to_list_level(vm_obj const & o) {
+    if (is_simple(o))
+        return list<level>();
+    else
+        return list<level>(to_level(cfield(o, 0)), to_list_level(cfield(o, 1)));
+}
+
+vm_obj to_obj(buffer<level> const & ls) {
+    vm_obj r = mk_vm_simple(0);
+    unsigned i = ls.size();
+    while (i > 0) {
+        --i;
+        r = mk_vm_constructor(1, to_obj(ls[i]), r);
+    }
+    return r;
+}
+
+vm_obj to_obj(list<level> const & ls) {
+    buffer<level> ls_buff;
+    to_buffer(ls, ls_buff);
+    return to_obj(ls_buff);
+}
+
 vm_obj level_zero() {
     return to_obj(mk_level_zero());
 }
diff --git a/src/library/vm/vm_level.h b/src/library/vm/vm_level.h
index 4e1f3e7a9f..8a0072be27 100644
--- a/src/library/vm/vm_level.h
+++ b/src/library/vm/vm_level.h
@@ -11,6 +11,10 @@ Author: Leonardo de Moura
 namespace lean {
 level const & to_level(vm_obj const & o);
 vm_obj to_obj(level const & n);
+list<level> to_list_level(vm_obj const & o);
+/* Convert buffer of levels into a lean (list level) object */
+vm_obj to_obj(buffer<level> const & ls);
+vm_obj to_obj(list<level> const & ls);
 void initialize_vm_level();
 void finalize_vm_level();
 }
diff --git a/tests/lean/run/meta_expr1.lean b/tests/lean/run/meta_expr1.lean
new file mode 100644
index 0000000000..8f12fef6ab
--- /dev/null
+++ b/tests/lean/run/meta_expr1.lean
@@ -0,0 +1,4 @@
+import meta
+open unsigned list
+
+vm_eval expr.app (expr.app (expr.const "f" []) (expr.mk_var 1)) (expr.const "a" [])