diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt
index e9b6deda8e..ff704d188c 100644
--- a/src/bindings/lua/CMakeLists.txt
+++ b/src/bindings/lua/CMakeLists.txt
@@ -1 +1 @@
-add_library(lua util.cpp name.cpp numerics.cpp options.cpp)
+add_library(lua util.cpp name.cpp numerics.cpp options.cpp sexpr.cpp)
diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp
new file mode 100644
index 0000000000..17b6cc1988
--- /dev/null
+++ b/src/bindings/lua/sexpr.cpp
@@ -0,0 +1,105 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifdef LEAN_USE_LUA
+#include <sstream>
+#include <lua.hpp>
+#include "util/debug.h"
+#include "util/sexpr/sexpr.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/name.h"
+#include "bindings/lua/numerics.h"
+
+namespace lean {
+constexpr char const * sexpr_mt = "sexpr.mt";
+
+static int push_sexpr(lua_State * L, sexpr const & e) {
+    void * mem = lua_newuserdata(L, sizeof(sexpr));
+    new (mem) sexpr(e);
+    luaL_getmetatable(L, sexpr_mt);
+    lua_setmetatable(L, -2);
+    return 1;
+}
+
+bool is_sexpr(lua_State * L, int idx) {
+    return testudata(L, idx, sexpr_mt);
+}
+
+static sexpr to_sexpr(lua_State * L, int idx) {
+    if (lua_isnil(L, idx)) {
+        return sexpr();
+    } else if (lua_isboolean(L, idx)) {
+        return sexpr(lua_toboolean(L, idx));
+    } else if (lua_isnumber(L, idx)) {
+        // Remark: we convert to integer by default
+        return sexpr(static_cast<int>(lua_tointeger(L, idx)));
+    } else if (is_name(L, idx)) {
+        return sexpr(to_name(L, idx));
+    } else if (is_sexpr(L, idx)) {
+        return *static_cast<sexpr*>(lua_touserdata(L, idx));
+    } else if (is_mpz(L, idx)) {
+        return sexpr(to_mpz(L, idx));
+    } else if (is_mpq(L, idx)) {
+        return sexpr(to_mpq(L, idx));
+    } else {
+        return sexpr(lua_tostring(L, idx));
+    }
+}
+
+static int sexpr_gc(lua_State * L) {
+    to_sexpr(L, 1).~sexpr();
+    return 0;
+}
+
+static int sexpr_tostring(lua_State * L) {
+    std::ostringstream out;
+    out << to_sexpr(L, 1);
+    lua_pushfstring(L, out.str().c_str());
+    return 1;
+}
+
+static int mk_sexpr(lua_State * L) {
+    sexpr r;
+    int nargs = lua_gettop(L);
+    if (nargs == 0) {
+        r = sexpr();
+    } else {
+        int i = nargs;
+        r = to_sexpr(L, i);
+        i--;
+        for (; i >= 1; i--) {
+            r = sexpr(to_sexpr(L, i), r);
+        }
+    }
+    return push_sexpr(L, r);
+}
+
+static int sexpr_eq(lua_State * L) {
+    lua_pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2));
+    return 1;
+}
+
+static int sexpr_lt(lua_State * L) {
+    lua_pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2));
+    return 1;
+}
+
+static const struct luaL_Reg sexpr_m[] = {
+    {"__gc",       sexpr_gc}, // never throws
+    {"__tostring", safe_function<sexpr_tostring>},
+    {"__eq",       safe_function<sexpr_eq>},
+    {"__lt",       safe_function<sexpr_lt>},
+    {0, 0}
+};
+
+void open_sexpr(lua_State * L) {
+    luaL_newmetatable(L, sexpr_mt);
+    setfuncs(L, sexpr_m, 0);
+    lua_pushcfunction(L, safe_function<mk_sexpr>);
+    lua_setglobal(L, "sexpr");
+}
+}
+#endif
diff --git a/src/bindings/lua/sexpr.h b/src/bindings/lua/sexpr.h
new file mode 100644
index 0000000000..3ba3292eef
--- /dev/null
+++ b/src/bindings/lua/sexpr.h
@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifdef LEAN_USE_LUA
+#include <lua.hpp>
+namespace lean {
+class sexpr;
+void open_sexpr(lua_State * L);
+bool is_sexpr(lua_State * L, int idx);
+sexpr to_sexpr(lua_State * L, int idx);
+}
+#endif
diff --git a/src/shell/lua/leanlua.cpp b/src/shell/lua/leanlua.cpp
index 9c52a300db..55a30745d9 100644
--- a/src/shell/lua/leanlua.cpp
+++ b/src/shell/lua/leanlua.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/name.h"
 #include "bindings/lua/numerics.h"
 #include "bindings/lua/options.h"
+#include "bindings/lua/sexpr.h"
 
 int main(int argc, char ** argv) {
     int status, result;
@@ -23,6 +24,7 @@ int main(int argc, char ** argv) {
     lean::open_mpz(L);
     lean::open_mpq(L);
     lean::open_options(L);
+    lean::open_sexpr(L);
 
     for (int i = 1; i < argc; i++) {
         status = luaL_loadfile(L, argv[i]);
diff --git a/tests/lua/sexpr1.lua b/tests/lua/sexpr1.lua
new file mode 100644
index 0000000000..ce86da9947
--- /dev/null
+++ b/tests/lua/sexpr1.lua
@@ -0,0 +1,8 @@
+s = sexpr(1, 2, 3)
+print(s)
+s = sexpr(1, 2, 3, nil)
+print(s)
+s = sexpr(sexpr(1, 2), sexpr(3, 4), nil)
+print(s)
+s = sexpr(mpz("100000000000000"), mpq(3)/2, sexpr(1, 2, 3, nil), nil)
+print(s)
\ No newline at end of file