diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
index e4f5c59a8..54d9c3ff3 100644
--- a/src/api/CMakeLists.txt
+++ b/src/api/CMakeLists.txt
@@ -1,4 +1,4 @@
-add_library(api OBJECT string.cpp exception.cpp name.cpp)
+add_library(api OBJECT string.cpp exception.cpp name.cpp options.cpp)
 
 FILE(GLOB LEAN_API_INCLUDE_FILES lean*.h)
 install(FILES ${LEAN_API_INCLUDE_FILES} DESTINATION include)
diff --git a/src/api/lean.h b/src/api/lean.h
index b6a17c4e0..0d460be39 100644
--- a/src/api/lean.h
+++ b/src/api/lean.h
@@ -12,5 +12,6 @@ Author: Leonardo de Moura
 #include "lean_string.h"        // NOLINT
 #include "lean_exception.h"     // NOLINT
 #include "lean_name.h"          // NOLINT
+#include "lean_options.h"       // NOLINT
 
 #endif
diff --git a/src/api/lean_name.h b/src/api/lean_name.h
index 8f430f51b..2e277a676 100644
--- a/src/api/lean_name.h
+++ b/src/api/lean_name.h
@@ -10,6 +10,15 @@ Author: Leonardo de Moura
 #ifdef __cplusplus
 extern "C" {
 #endif
+/**
+   \defgroup capi C API
+*/
+/*@{*/
+
+/**
+   @name Hierarchical names API
+*/
+/*@{*/
 
 LEAN_DEFINE_TYPE(lean_name);
 
@@ -22,7 +31,7 @@ lean_bool lean_name_mk_str(lean_name pre, char const * s, lean_name * r, lean_ex
     \pre !lean_name_is_anonymous(pre)
     \remark \c r must be disposed using #lean_name_del */
 lean_bool lean_name_mk_idx(lean_name pre, unsigned i, lean_name * r, lean_exception * ex);
-/** \brief Delete/dispose a Lean hierarchical name */
+/** \brief Delete/dispose the given hierarchical name */
 void lean_name_del(lean_name n);
 /** \brief Return lean_true iff \c n is the anonymous */
 lean_bool lean_name_is_anonymous(lean_name n);
@@ -51,6 +60,9 @@ lean_bool lean_name_get_idx(lean_name n, unsigned * r, lean_exception * ex);
 */
 lean_bool lean_name_to_string(lean_name n, char const **r, lean_exception * ex);
 
+/*@}*/
+/*@}*/
+
 #ifdef __cplusplus
 };
 #endif
diff --git a/src/api/lean_options.h b/src/api/lean_options.h
new file mode 100644
index 000000000..72e650175
--- /dev/null
+++ b/src/api/lean_options.h
@@ -0,0 +1,97 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifndef _LEAN_OPTIONS_H
+#define _LEAN_OPTIONS_H
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/**
+   \defgroup capi C API
+*/
+/*@{*/
+
+/**
+   @name Configuration options API
+
+   A configuration options is essentially a mapping from names to values.
+*/
+/*@{*/
+
+LEAN_DEFINE_TYPE(lean_options);
+
+/** \brief Create an empty configuration options object. */
+lean_bool lean_options_mk_empty(lean_options * r, lean_exception * ex);
+/** \brief r := o[n := v]
+    \remark \c r must be disposed using #lean_options_del */
+lean_bool lean_options_set_bool(lean_options o, lean_name n, lean_bool v, lean_options * r, lean_exception * ex);
+/** \brief r := o[n := v]
+    \remark \c r must be disposed using #lean_options_del */
+lean_bool lean_options_set_int(lean_options o, lean_name n, int v, lean_options * r, lean_exception * ex);
+/** \brief r := o[n := v]
+    \remark \c r must be disposed using #lean_options_del */
+lean_bool lean_options_set_unsigned(lean_options o, lean_name n, unsigned v, lean_options * r, lean_exception * ex);
+/** \brief r := o[n := v]
+    \remark \c r must be disposed using #lean_options_del */
+lean_bool lean_options_set_double(lean_options o, lean_name n, double v, lean_options * r, lean_exception * ex);
+/** \brief r := o[n := v]
+    \remark \c r must be disposed using #lean_options_del */
+lean_bool lean_options_set_string(lean_options o, lean_name n, char const * v, lean_options * r, lean_exception * ex);
+/** \brief Combine the options o1 and o2 and store the result in \c r.
+    \remark The assignments in o2 overrides the ones in o1.
+    \remark \c r must be disposed using #lean_options_del */
+lean_bool lean_options_join(lean_options o1, lean_options o2, lean_options * r, lean_exception * ex);
+
+/** \brief Delete/dispose the given options object.  */
+void lean_options_del(lean_options o);
+
+/** \brief Store in \c r a string representation of the given options object.
+    \remark \c r must be deleted using #lean_string_del
+*/
+lean_bool lean_options_to_string(lean_options o, char const ** r, lean_exception * ex);
+/** \brief Return true iff the two given options object are equal. */
+lean_bool lean_options_eq(lean_options o1, lean_options o2);
+/** \brief Return true iff the given options object is empty. */
+lean_bool lean_options_empty(lean_options o);
+/** \brief Return true iff the given options object contains the entry \c n. */
+lean_bool lean_options_contains(lean_options o, lean_name n);
+
+/** \brief Store in \c r the value assigned to \c n in the options \c o.
+    \pre lean_options_contains(o, n)
+    \remark If the value associated with \c n is not a Boolean, the result is lean_false
+*/
+lean_bool lean_options_get_bool(lean_options o, lean_name n, lean_bool * r, lean_exception * ex);
+/** \brief Store in \c r the value assigned to \c n in the options \c o.
+    \pre lean_options_contains(o, n)
+    \remark If the value associated with \c n is not a numeric value, the result is 0
+*/
+lean_bool lean_options_get_int(lean_options o, lean_name n, int * r, lean_exception * ex);
+/** \brief Store in \c r the value assigned to \c n in the options \c o.
+    \pre lean_options_contains(o, n)
+    \remark If the value associated with \c n is not a numeric value, the result is 0
+*/
+lean_bool lean_options_get_unsigned(lean_options o, lean_name n, unsigned * r, lean_exception * ex);
+/** \brief Store in \c r the value assigned to \c n in the options \c o.
+    \pre lean_options_contains(o, n)
+    \remark If the value associated with \c n is not a double, the result is 0.0
+*/
+lean_bool lean_options_get_double(lean_options o, lean_name n, double * r, lean_exception * ex);
+/** \brief Store in \c r the value assigned to \c n in the options \c o.
+    \pre lean_options_contains(o, n)
+    \remark If the value associated with \c n is not a double, the result is the empty string ""
+    \remark \c r must be deleted using #lean_string_del.
+*/
+lean_bool lean_options_get_string(lean_options o, lean_name n, char const ** r, lean_exception * ex);
+
+/*@}*/
+/*@}*/
+
+#ifdef __cplusplus
+};
+#endif
+#endif
diff --git a/src/api/options.cpp b/src/api/options.cpp
new file mode 100644
index 000000000..c77abdceb
--- /dev/null
+++ b/src/api/options.cpp
@@ -0,0 +1,133 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/sstream.h"
+#include "api/name.h"
+#include "api/string.h"
+#include "api/options.h"
+using namespace lean; // NOLINT
+
+lean_bool lean_options_mk_empty(lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    *r = of_options(new options());
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_set_bool(lean_options o, lean_name n, lean_bool v, lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o);
+    check_nonnull(n);
+    *r = of_options(new options(to_options_ref(o).update(to_name_ref(n), static_cast<bool>(v))));
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_set_int(lean_options o, lean_name n, int v, lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o);
+    check_nonnull(n);
+    *r = of_options(new options(to_options_ref(o).update(to_name_ref(n), v)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_set_unsigned(lean_options o, lean_name n, unsigned v, lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o);
+    check_nonnull(n);
+    *r = of_options(new options(to_options_ref(o).update(to_name_ref(n), v)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_set_double(lean_options o, lean_name n, double v, lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o);
+    check_nonnull(n);
+    *r = of_options(new options(to_options_ref(o).update(to_name_ref(n), v)));
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_set_string(lean_options o, lean_name n, char const * v, lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o);
+    check_nonnull(n);
+    check_nonnull(v);
+    *r = of_options(new options(to_options_ref(o).update(to_name_ref(n), std::string(v).c_str())));
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_join(lean_options o1, lean_options o2, lean_options * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o1);
+    check_nonnull(o2);
+    *r = of_options(new options(join(to_options_ref(o1), to_options_ref(o2))));
+    LEAN_CATCH;
+}
+
+void lean_options_del(lean_options o) {
+    delete to_options(o);
+}
+
+lean_bool lean_options_to_string(lean_options o, char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    check_nonnull(o);
+    std::ostringstream out;
+    out << to_options_ref(o);
+    *r = mk_string(out.str());
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_eq(lean_options o1, lean_options o2) {
+    return o1 && o2 && to_options_ref(o1) == to_options_ref(o2);
+}
+
+lean_bool lean_options_empty(lean_options o) {
+    return o && to_options_ref(o).empty();
+}
+
+lean_bool lean_options_contains(lean_options o, lean_name n) {
+    return o && n && to_options_ref(o).contains(to_name_ref(n));
+}
+
+static void check_entry(lean_options o, lean_name n) {
+    check_nonnull(o);
+    check_nonnull(n);
+    if (!lean_options_contains(o, n))
+        throw exception(sstream() << "options object does not contain entry '" << to_name_ref(n) << "'");
+}
+
+lean_bool lean_options_get_bool(lean_options o, lean_name n, lean_bool * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_entry(o, n);
+    *r = to_options_ref(o).get_bool(to_name_ref(n), false);
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_get_int(lean_options o, lean_name n, int * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_entry(o, n);
+    *r = to_options_ref(o).get_int(to_name_ref(n), 0);
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_get_unsigned(lean_options o, lean_name n, unsigned * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_entry(o, n);
+    *r = to_options_ref(o).get_unsigned(to_name_ref(n), 0);
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_get_double(lean_options o, lean_name n, double * r, lean_exception * ex) {
+    LEAN_TRY;
+    check_entry(o, n);
+    *r = to_options_ref(o).get_double(to_name_ref(n), 0.0);
+    LEAN_CATCH;
+}
+
+lean_bool lean_options_get_string(lean_options o, lean_name n, char const ** r, lean_exception * ex) {
+    LEAN_TRY;
+    check_entry(o, n);
+    *r = mk_string(to_options_ref(o).get_string(to_name_ref(n), ""));
+    LEAN_CATCH;
+}
diff --git a/src/api/options.h b/src/api/options.h
new file mode 100644
index 000000000..3d2aeb8bc
--- /dev/null
+++ b/src/api/options.h
@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2015 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/sexpr/options.h"
+#include "api/exception.h"
+#include "api/name.h"
+#include "api/lean_options.h"
+namespace lean {
+inline options * to_options(lean_options n) { return reinterpret_cast<options *>(n); }
+inline options const & to_options_ref(lean_options n) { return *reinterpret_cast<options *>(n); }
+inline lean_options of_options(options * n) { return reinterpret_cast<lean_options>(n); }
+}