diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index fe202179a..f717554ec 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -31,19 +31,27 @@ include(cmake/FindGMP.cmake)
 set(EXTRA_LIBS ${EXTRA_LIBS} ${GMP_LIBRARIES})
 
 # tcmalloc
-include(cmake/FindTcmalloc.cmake)
-if(${TCMALLOC_FOUND})
-  set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
+option(tcmalloc "tcmalloc" ON)
+if("${tcmalloc}" MATCHES "ON")
+  include(cmake/FindTcmalloc.cmake)
+  if(${TCMALLOC_FOUND})
+    set(EXTRA_LIBS ${EXTRA_LIBS} ${TCMALLOC_LIBRARIES})
+  endif()
+else()
+  message("-- Using standard malloc.")
 endif()
 
 include_directories(${LEAN_SOURCE_DIR}/util)
 include_directories(${LEAN_SOURCE_DIR}/numerics)
 include_directories(${LEAN_SOURCE_DIR}/interval)
+include_directories(${LEAN_SOURCE_DIR}/sexpr)
 
 add_subdirectory(util)
 set(EXTRA_LIBS ${EXTRA_LIBS} util)
 add_subdirectory(numerics)
 set(EXTRA_LIBS ${EXTRA_LIBS} numerics)
+add_subdirectory(sexpr)
+set(EXTRA_LIBS ${EXTRA_LIBS} sexpr)
 add_subdirectory(interval)
 set(EXTRA_LIBS ${EXTRA_LIBS} interval)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
@@ -51,3 +59,4 @@ add_subdirectory(shell)
 add_subdirectory(tests/util)
 add_subdirectory(tests/numerics)
 add_subdirectory(tests/interval)
+add_subdirectory(tests/sexpr)
diff --git a/src/sexpr/CMakeLists.txt b/src/sexpr/CMakeLists.txt
new file mode 100644
index 000000000..48c379a3a
--- /dev/null
+++ b/src/sexpr/CMakeLists.txt
@@ -0,0 +1,2 @@
+add_library(sexpr sexpr.cpp)
+target_link_libraries(sexpr ${EXTRA_LIBS})
diff --git a/src/sexpr/sexpr.cpp b/src/sexpr/sexpr.cpp
new file mode 100644
index 000000000..b3a23f689
--- /dev/null
+++ b/src/sexpr/sexpr.cpp
@@ -0,0 +1,227 @@
+/*
+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 <cstring>
+#include "rc.h"
+#include "hash.h"
+#include "sexpr.h"
+#include "name.h"
+#include "mpz.h"
+#include "mpq.h"
+
+namespace lean {
+
+struct sexpr_cell {
+    void dealloc();
+    MK_LEAN_RC()
+    sexpr::kind  m_kind;
+    unsigned     m_hash;
+
+    sexpr_cell(sexpr::kind k, unsigned h):m_rc(1), m_kind(k), m_hash(h) {}
+};
+
+struct sexpr_string : public sexpr_cell {
+    std::string m_value;
+    sexpr_string(char const * v):
+        sexpr_cell(sexpr::kind::STRING, hash(v, strlen(v), 13)),
+        m_value(v) {}
+    sexpr_string(std::string const & v):
+        sexpr_cell(sexpr::kind::STRING, hash(v.c_str(), v.size(), 13)),
+        m_value(v) {}
+};
+
+struct sexpr_int : public sexpr_cell {
+    int m_value;
+    sexpr_int(int v):
+        sexpr_cell(sexpr::kind::INT, v),
+        m_value(v) {}
+};
+
+struct sexpr_double : public sexpr_cell {
+    double m_value;
+    sexpr_double(double v):
+        sexpr_cell(sexpr::kind::DOUBLE, static_cast<unsigned>(v)),
+        m_value(v) {}
+};
+
+struct sexpr_name : public sexpr_cell {
+    name m_value;
+    sexpr_name(name const & v):
+        sexpr_cell(sexpr::kind::NAME, v.hash()),
+        m_value(v) {}
+};
+
+struct sexpr_mpz : public sexpr_cell {
+    mpz m_value;
+    sexpr_mpz(mpz const & v):
+        sexpr_cell(sexpr::kind::MPZ, v.hash()),
+        m_value(v) {}
+};
+
+struct sexpr_mpq : public sexpr_cell {
+    mpq m_value;
+    sexpr_mpq(mpq const & v):
+        sexpr_cell(sexpr::kind::MPQ, v.hash()),
+        m_value(v) {}
+};
+
+struct sexpr_cons : public sexpr_cell {
+    sexpr m_head;
+    sexpr m_tail;
+    sexpr_cons(sexpr const & h, sexpr const & t):
+        sexpr_cell(sexpr::kind::CONS, hash(h.hash(), t.hash())),
+        m_head(h),
+        m_tail(t) {}
+};
+
+void sexpr_cell::dealloc() {
+    switch (m_kind) {
+    case sexpr::kind::NIL:         lean_unreachable();                      break;
+    case sexpr::kind::STRING:      delete static_cast<sexpr_string*>(this); break;
+    case sexpr::kind::INT:         delete static_cast<sexpr_int*>(this);    break;
+    case sexpr::kind::DOUBLE:      delete static_cast<sexpr_double*>(this); break;
+    case sexpr::kind::NAME:        delete static_cast<sexpr_name*>(this);   break;
+    case sexpr::kind::MPZ:         delete static_cast<sexpr_mpz*>(this);    break;
+    case sexpr::kind::MPQ:         delete static_cast<sexpr_mpq*>(this);    break;
+    case sexpr::kind::CONS:        delete static_cast<sexpr_cons*>(this);   break;
+    }
+}
+
+sexpr::sexpr(char const * v):m_ptr(new sexpr_string(v)) {}
+sexpr::sexpr(std::string const & v):m_ptr(new sexpr_string(v)) {}
+sexpr::sexpr(int v):m_ptr(new sexpr_int(v)) {}
+sexpr::sexpr(double v):m_ptr(new sexpr_double(v)) {}
+sexpr::sexpr(name const & v):m_ptr(new sexpr_name(v)) {}
+sexpr::sexpr(mpz const & v):m_ptr(new sexpr_mpz(v)) {}
+sexpr::sexpr(mpq const & v):m_ptr(new sexpr_mpq(v)) {}
+sexpr::sexpr(sexpr const & h, sexpr const & t):m_ptr(new sexpr_cons(h, t)) {}
+sexpr::sexpr(sexpr const & s):m_ptr(s.m_ptr) {
+    if (m_ptr)
+        m_ptr->inc_ref();
+}
+sexpr::sexpr(sexpr && s):m_ptr(s.m_ptr) {
+    s.m_ptr = 0;
+}
+sexpr::~sexpr() {
+    if (m_ptr)
+        m_ptr->dec_ref();
+}
+
+sexpr::kind sexpr::get_kind() const { return m_ptr ? m_ptr->m_kind : kind::NIL; }
+sexpr const & head(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_head; }
+sexpr const & tail(sexpr const & s) { lean_assert(is_cons(s)); return static_cast<sexpr_cons*>(s.m_ptr)->m_tail; }
+std::string const & sexpr::get_string() const { return static_cast<sexpr_string*>(m_ptr)->m_value; }
+int sexpr::get_int() const { return static_cast<sexpr_int*>(m_ptr)->m_value; }
+double sexpr::get_double() const { return static_cast<sexpr_double*>(m_ptr)->m_value; }
+name const & sexpr::get_name() const { return static_cast<sexpr_name*>(m_ptr)->m_value; }
+mpz const & sexpr::get_mpz() const { return static_cast<sexpr_mpz*>(m_ptr)->m_value; }
+mpq const & sexpr::get_mpq() const { return static_cast<sexpr_mpq*>(m_ptr)->m_value; }
+
+unsigned sexpr::hash() const { return m_ptr == nullptr ? 23 : m_ptr->m_hash; }
+
+sexpr & sexpr::operator=(sexpr 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;
+}
+
+sexpr & sexpr::operator=(sexpr && s) {
+    if (m_ptr)
+        m_ptr->dec_ref();
+    m_ptr   = s.m_ptr;
+    s.m_ptr = 0;
+    return *this;
+}
+
+bool is_list(sexpr const & s) {
+    if (is_nil(s))
+        return true;
+    if (!is_cons(s))
+        return false;
+    sexpr const * curr = &s;
+    while (true) {
+        lean_assert(is_cons(*curr));
+        curr = &tail(*curr);
+        if (is_nil(*curr))
+            return true;
+        if (!is_cons(*curr))
+            return false;
+    }
+}
+
+unsigned length(sexpr const & s) {
+    unsigned r = 0;
+    sexpr const * curr = &s;
+    while (true) {
+        if (is_nil(*curr))
+            return r;
+        lean_assert(is_cons(*curr));
+        r++;
+        curr = &tail(*curr);
+    }
+}
+
+bool operator==(sexpr const & a, sexpr const & b) {
+    sexpr::kind ka = a.get_kind();
+    sexpr::kind kb = b.get_kind();
+    if (ka != kb)
+        return false;
+    // if (a.hash() != b.hash())
+    //     return false;
+    switch (ka) {
+    case sexpr::kind::NIL:         return true;
+    case sexpr::kind::STRING:      return to_string(a) == to_string(b);
+    case sexpr::kind::INT:         return to_int(a) == to_int(b);
+    case sexpr::kind::DOUBLE:      return to_double(a) == to_double(b);
+    case sexpr::kind::NAME:        return to_name(a) == to_name(b);
+    case sexpr::kind::MPZ:         return to_mpz(a) == to_mpz(b);
+    case sexpr::kind::MPQ:         return to_mpq(a) == to_mpq(b);
+    case sexpr::kind::CONS:        return head(a) == head(b) && tail(a) == tail(b);
+    }
+    return false;
+}
+
+bool operator<(sexpr const & a, sexpr const & b) {
+    // TODO
+    return false;
+}
+
+std::ostream & operator<<(std::ostream & out, sexpr const & s) {
+    switch (s.get_kind()) {
+    case sexpr::kind::NIL:         out << "nil"; break;
+    case sexpr::kind::STRING:      out << "\"" << to_string(s) << "\""; break;
+    case sexpr::kind::INT:         out << to_int(s); break;
+    case sexpr::kind::DOUBLE:      out << to_double(s); break;
+    case sexpr::kind::NAME:        out << to_name(s); break;
+    case sexpr::kind::MPZ:         out << to_mpz(s); break;
+    case sexpr::kind::MPQ:         out << to_mpq(s); break;
+    case sexpr::kind::CONS: {
+        out << "(";
+        sexpr const * curr = &s;
+        while (true) {
+            out << head(*curr);
+            curr = &tail(*curr);
+            if (is_nil(*curr)) {
+                break;
+            }
+            else if (!is_cons(*curr)) {
+                out << " . ";
+                out << *curr;
+                break;
+            }
+            else {
+                out << " ";
+            }
+        }
+        out << ")";
+    }}
+    return out;
+}
+
+}
diff --git a/src/sexpr/sexpr.h b/src/sexpr/sexpr.h
new file mode 100644
index 000000000..2f740fe83
--- /dev/null
+++ b/src/sexpr/sexpr.h
@@ -0,0 +1,121 @@
+/*
+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>
+
+namespace lean {
+class name;
+class mpq;
+class mpz;
+struct sexpr_cell;
+
+/**
+   \brief Simple LISP-like S-expressions.
+   1. Atoms: nil, string, int, name, mpz or mpq
+   2. Pair: (x . y) where x and y are S-expressions.
+
+   S-expressions are used for tracking configuration options, statistics, etc.
+
+   Remark: this datastructure does not allow destructive updates.
+*/
+class sexpr {
+    sexpr_cell * m_ptr;
+public:
+    enum class kind { NIL, STRING, INT, DOUBLE, NAME, MPZ, MPQ, CONS };
+    sexpr():m_ptr(nullptr) {}
+    sexpr(char const * v);
+    sexpr(std::string const & v);
+    sexpr(int v);
+    sexpr(double v);
+    sexpr(name const & v);
+    sexpr(mpz const & v);
+    sexpr(mpq const & v);
+    sexpr(sexpr const & h, sexpr const & t);
+    sexpr(char const * v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(std::string const & v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(int v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(double v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(name const & v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(mpz const & v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(mpq const & v, sexpr const & t):sexpr(sexpr(v), t) {}
+    sexpr(sexpr const & s);
+    sexpr(sexpr && s);
+    template<typename T>
+    sexpr(std::initializer_list<T> const & l):sexpr() {
+        auto it = l.end();
+        while (it != l.begin()) {
+            --it;
+            *this = sexpr(*it, *this);
+        }
+    }
+    ~sexpr();
+
+    kind get_kind() const;
+
+    friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; }
+    friend sexpr const & head(sexpr const & s);
+    friend sexpr const & tail(sexpr const & s);
+
+    std::string const & get_string() const;
+    int get_int() const;
+    double get_double() const;
+    name const & get_name() const;
+    mpz const & get_mpz() const;
+    mpq const & get_mpq() const;
+
+    unsigned hash() const;
+
+    sexpr & operator=(sexpr const & s);
+    sexpr & operator=(sexpr&& s);
+    sexpr & operator=(char const * v) { return operator=(sexpr(v)); }
+    sexpr & operator=(std::string const & v) { return operator=(sexpr(v)); }
+    sexpr & operator=(int v) { return operator=(sexpr(v)); }
+    sexpr & operator=(mpz const & v) { return operator=(sexpr(v)); }
+    sexpr & operator=(mpq const & v) { return operator=(sexpr(v)); }
+
+    friend void swap(sexpr & a, sexpr & b) { std::swap(a.m_ptr, b.m_ptr); }
+
+    // Pointer equality
+    friend bool eqp(sexpr const & a, sexpr const & b) { return a.m_ptr == b.m_ptr; }
+
+    friend std::ostream & operator<<(std::ostream & out, sexpr const & s);
+
+};
+
+inline sexpr nil() { return sexpr(); }
+inline sexpr cons(sexpr const & head, sexpr const & tail) { return sexpr(head, tail); }
+inline sexpr const & car(sexpr const & s) { return head(s); }
+inline sexpr const & cdr(sexpr const & s) { return tail(s); }
+inline bool is_atom(sexpr const & s) { return s.get_kind() != sexpr::kind::CONS; }
+inline bool is_cons(sexpr const & s) { return s.get_kind() == sexpr::kind::CONS; }
+
+inline bool is_string(sexpr const & s) { return s.get_kind() == sexpr::kind::STRING; }
+inline bool is_int(sexpr const & s) { return s.get_kind() == sexpr::kind::INT; }
+inline bool is_double(sexpr const & s) { return s.get_kind() == sexpr::kind::DOUBLE; }
+inline bool is_name(sexpr const & s) { return s.get_kind() == sexpr::kind::NAME; }
+inline bool is_mpz(sexpr const & s) { return s.get_kind() == sexpr::kind::MPZ; }
+inline bool is_mpq(sexpr const & s) { return s.get_kind() == sexpr::kind::MPQ; }
+
+inline std::string const & to_string(sexpr const & s) { return s.get_string(); }
+inline int to_int(sexpr const & s) { return s.get_int(); }
+inline double to_double(sexpr const & s) { return s.get_double(); }
+inline name const & to_name(sexpr const & s) { return s.get_name(); }
+inline mpz const & to_mpz(sexpr const & s) { return s.get_mpz(); }
+inline mpq const & to_mpq(sexpr const & s) { return s.get_mpq(); }
+
+bool is_list(sexpr const & s);
+unsigned length(sexpr const & s);
+inline unsigned len(sexpr const & s) { return length(s); }
+
+bool operator==(sexpr const & a, sexpr const & b);
+bool operator<(sexpr const & a, sexpr const & b);
+inline bool operator!=(sexpr const & a, sexpr const & b) { return !(a == b); }
+inline bool operator>(sexpr const & a, sexpr const & b) { return b < a; }
+inline bool operator<=(sexpr const & a, sexpr const & b) { return !(a > b); }
+inline bool operator>=(sexpr const & a, sexpr const & b) { return !(a < b); }
+
+}
diff --git a/src/tests/sexpr/CMakeLists.txt b/src/tests/sexpr/CMakeLists.txt
new file mode 100644
index 000000000..686bcd03d
--- /dev/null
+++ b/src/tests/sexpr/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_executable(sexpr_tst sexpr.cpp)
+target_link_libraries(sexpr_tst ${EXTRA_LIBS})
+add_test(sexpr ${CMAKE_CURRENT_BINARY_DIR}/sexpr_tst)
diff --git a/src/tests/sexpr/sexpr.cpp b/src/tests/sexpr/sexpr.cpp
new file mode 100644
index 000000000..6b7c61f3e
--- /dev/null
+++ b/src/tests/sexpr/sexpr.cpp
@@ -0,0 +1,57 @@
+/*
+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 "sexpr.h"
+#include "mpq.h"
+#include "name.h"
+#include "test.h"
+using namespace lean;
+
+static void tst1() {
+    sexpr s1(30, nil());
+    sexpr s2("name", s1);
+    std::cout << s2 << "\n";
+    std::cout << sexpr(s2, s2) << "\n";
+    lean_assert(len(s2) == 2);
+    lean_assert(is_nil(nil()));
+    lean_assert(!is_nil(s2));
+    lean_assert(is_cons(s2));
+    lean_assert(is_cons(sexpr(s2, s2)));
+    lean_assert(is_list(s2));
+    lean_assert(is_cons(sexpr(s2, s2)));
+    lean_assert(is_list(sexpr(s2, s2)));
+    lean_assert(!is_list(sexpr(s2, sexpr(10))));
+    lean_assert(s2 == sexpr("name", sexpr(30, nil())));
+    lean_assert(s2 != sexpr("name", sexpr(11.2, nil())));
+    lean_assert(s2 != sexpr("name", sexpr(20, nil())));
+    lean_assert(s2 == sexpr("name", sexpr(30, nil())));
+    lean_assert(cdr(s2) == sexpr(30, nil()));
+    lean_assert(car(s2) == sexpr("name"));
+    std::cout << sexpr(name(name("foo"), 1), s2) << "\n";
+    lean_assert(to_mpq(sexpr(mpq("1/3"))) == mpq(1, 3));
+    lean_assert(to_int(sexpr(1)) == 1);
+    lean_assert(is_int(sexpr(1)));
+    lean_assert(!is_nil(sexpr(2)));
+    std::cout << sexpr(sexpr(10), sexpr(20)) << "\n";
+    std::cout << sexpr{10, 20, 30, 40} << "\n";
+    std::cout << sexpr{"foo", "bla", "tst"} << "\n";
+    std::cout << sexpr{10.20, 3.2, 4.3} << "\n";
+    std::cout << sexpr(10.2) << "\n";
+    std::cout << sexpr{10.2} << "\n";
+    lean_assert(!is_list(sexpr(10.2)));
+    lean_assert(is_list(sexpr{10.2}));
+    lean_assert(len(sexpr{10.2}) == 1);
+    // list of pairs
+    std::cout << sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) } << "\n";
+    // list of lists
+    std::cout << sexpr{ sexpr{1,2}, sexpr{2,3}, sexpr{0,1} } << "\n";
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    return 0;
+}
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 32d313735..410441219 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1 +1 @@
-add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp interrupt.cpp hash.cpp)
+add_library(util trace.cpp debug.cpp name.cpp exception.cpp verbosity.cpp interrupt.cpp hash.cpp escaped.cpp)
diff --git a/src/util/escaped.cpp b/src/util/escaped.cpp
new file mode 100644
index 000000000..be32470e1
--- /dev/null
+++ b/src/util/escaped.cpp
@@ -0,0 +1,44 @@
+/*
+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 "escaped.h"
+
+namespace lean {
+
+char const * escaped::end() const {
+    if (m_str == 0) return 0;
+    char const * it = m_str;
+    char const * e  = m_str;
+    while (*it) {
+        if (!m_trim_nl || *it != '\n') {
+            ++it;
+            e = it;
+        }
+        else {
+            ++it;
+        }
+    }
+    return e;
+}
+
+std::ostream & operator<<(std::ostream & out, escaped const & s) {
+    char const * it = s.m_str;
+    char const * e  = s.end();
+    for (; it != e; ++it) {
+        char c = *it;
+        if (c == '"') {
+            out << '\\';
+        }
+        out << c;
+        if (c == '\n') {
+            for (unsigned i = 0; i < s.m_indent; i++)
+                out << " ";
+        }
+    }
+    return out;
+}
+
+}
diff --git a/src/util/escaped.h b/src/util/escaped.h
new file mode 100644
index 000000000..cd1b27c80
--- /dev/null
+++ b/src/util/escaped.h
@@ -0,0 +1,23 @@
+/*
+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>
+
+namespace lean {
+
+class escaped {
+    char const * m_str;
+    bool         m_trim_nl; // if true -> eliminate '\n' in the end of m_str.
+    unsigned     m_indent;
+    char const * end() const;
+public:
+    escaped(char const * str, bool trim_nl = false, unsigned indent = 0):m_str(str), m_trim_nl(trim_nl), m_indent(indent) {}
+    friend std::ostream & operator<<(std::ostream & out, escaped const & s);
+};
+
+}