diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean
index 23a6b80966..42306680fe 100644
--- a/library/init/lean/compiler/ir/emitcpp.lean
+++ b/library/init/lean/compiler/ir/emitcpp.lean
@@ -11,8 +11,8 @@ import init.lean.compiler.ir.emitutil
 
 namespace Lean
 namespace IR
--- TODO: @[export]
-constant getExportNameFor (env : Environment) (n : Name) : Option Name := default _
+@[extern "lean_get_export_name_for"]
+constant getExportNameFor (env : @& Environment) (n : @& Name) : Option Name := default _
 
 namespace EmitCpp
 
@@ -54,7 +54,7 @@ def toCppType : IRType → String
 
 def openNamespacesAux : Name → M Unit
 | Name.anonymous      := pure ()
-| (Name.mkString p s) := openNamespacesAux p *> emitLn ("namespace " ++ s ++ "{")
+| (Name.mkString p s) := openNamespacesAux p *> emitLn ("namespace " ++ s ++ " {")
 | n                   := throw ("invalid namespace '" ++ toString n ++ "'")
 
 def openNamespaces (n : Name) : M Unit :=
@@ -100,11 +100,10 @@ do env ← getEnv,
    | some _                   := throw "invalid export name"
    | none                     := pure ("_init_" ++ n.mangle)
 
-def emitFnDeclAux (decl : Decl) (extern : Bool) : M Unit :=
+def emitFnDeclAux (decl : Decl) (cppBaseName : String) (addExternForConsts : Bool) : M Unit :=
 do
-cppBaseName ← toBaseCppName decl.name,
 let ps := decl.params,
-when (ps.isEmpty && extern) (emit "extern "),
+when (ps.isEmpty && addExternForConsts) (emit "extern "),
 emit (toCppType decl.resultType ++ " " ++ cppBaseName),
 unless (ps.isEmpty) $ do {
   emit "(",
@@ -116,12 +115,27 @@ unless (ps.isEmpty) $ do {
 },
 emitLn ";"
 
-def emitFnDecl (decl : Decl) (extern : Bool) : M Unit :=
+def emitFnDecl (decl : Decl) (addExternForConsts : Bool) : M Unit :=
 do
 openNamespacesFor decl.name,
-emitFnDeclAux decl extern,
+cppBaseName ← toBaseCppName decl.name,
+emitFnDeclAux decl cppBaseName addExternForConsts,
 closeNamespacesFor decl.name
 
+def cppQualifiedNameToName (s : String) : Name :=
+(s.split "::").foldl Name.mkString Name.anonymous
+
+def emitExternDeclAux (decl : Decl) (cppName : String) : M Unit :=
+do
+let qCppName := cppQualifiedNameToName cppName,
+openNamespaces qCppName,
+env ← getEnv,
+let extC := isExternC env decl.name,
+when extC (emit "extern \"C\" "),
+(Name.mkString _ qCppBaseName) ← pure qCppName | throw "invalid name",
+emitFnDeclAux decl qCppBaseName (!extC),
+closeNamespaces qCppName
+
 def emitFnDecls : M Unit :=
 do env ← getEnv,
    let decls := getDecls env,
@@ -130,8 +144,9 @@ do env ← getEnv,
    let usedDecls := usedDecls.toList,
    usedDecls.mfor $ λ n, do {
      decl ← getDecl n,
-     -- TODO: check extern
-     emitFnDecl decl (!modDecls.contains n)
+     match getExternNameFor env `cpp decl.name with
+     | some cppName := emitExternDeclAux decl cppName
+     | none         := emitFnDecl decl (!modDecls.contains n)
    }
 
 def emitMainFn : M Unit :=
diff --git a/library/init/lean/extern.lean b/library/init/lean/extern.lean
index cf9526ffbb..214acb8de7 100644
--- a/library/init/lean/extern.lean
+++ b/library/init/lean/extern.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.lean.expr init.data.option.basic
+import init.lean.environment
 
 namespace Lean
 
@@ -96,4 +97,22 @@ def mkExternCall (d : ExternAttrData) (backend : Name) (args : List String) : Op
 do e ← getExternEntryFor d backend,
    expandExternEntry e args
 
+@[extern "lean_get_extern_attr_data"]
+constant getExternAttrData (env : @& Environment) (fn : @& Name) : Option ExternAttrData := default _
+
+/- We say a Lean function marked as `[extern "<c_fn_nane>"]` is for all backends, and it is implemented using `extern "C"`.
+   Thus, there is no name mangling. -/
+def isExternC (env : Environment) (fn : Name) : Bool :=
+match getExternAttrData env fn with
+| some { entries := [ ExternEntry.standard `all _ ], .. } := true
+| _ := false
+
+def getExternNameFor (env : Environment) (backend : Name) (fn : Name) : Option String :=
+do data ← getExternAttrData env fn,
+   entry ← getExternEntryFor data backend,
+   match entry with
+   | ExternEntry.standard _ n := pure n
+   | ExternEntry.foreign _ n  := pure n
+   | _ := failure
+
 end Lean
diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean
index c0253b7bab..d65ed26467 100644
--- a/library/init/lean/name_mangling.lean
+++ b/library/init/lean/name_mangling.lean
@@ -37,18 +37,16 @@ private def String.mangleAux : Nat → String.Iterator → String → String
 def String.mangle (s : String) : String :=
 String.mangleAux s.length s.mkIterator ""
 
-private def Name.mangleAux (pre : String) : Name → String
-| Name.anonymous       := pre
+private def Name.mangleAux : Name → String
+| Name.anonymous      := ""
 | (Name.mkString p s) :=
   let m := String.mangle s in
   match p with
   | Name.anonymous := m
-  | _              := (Name.mangleAux p) ++ "_" ++ m
-| (Name.mkNumeral p n) :=
-  let r := Name.mangleAux p in
-  r ++ "_" ++ toString n ++ "_"
+  | _              := Name.mangleAux p ++ "_" ++ m
+| (Name.mkNumeral p n) := Name.mangleAux p ++ "_" ++ toString n ++ "_"
 
-def Name.mangle (n : Name) (pre : String := "_l") : String :=
-Name.mangleAux pre n
+def Name.mangle (n : Name) (pre : String := "l_") : String :=
+pre ++ Name.mangleAux n
 
 end Lean
diff --git a/src/library/compiler/export_attribute.cpp b/src/library/compiler/export_attribute.cpp
index 21827218a9..1c218f36a0 100644
--- a/src/library/compiler/export_attribute.cpp
+++ b/src/library/compiler/export_attribute.cpp
@@ -40,6 +40,10 @@ optional<name> get_export_name_for(environment const & env, name const & n) {
     }
 }
 
+extern "C" obj_res lean_get_export_name_for(b_obj_arg env, b_obj_arg n) {
+    return to_object(get_export_name_for(environment(env, true), name(n, true)));
+}
+
 void initialize_export_attribute() {
     register_system_attribute(export_attr("export", "name to be used by code generators",
                                           [](environment const & env, io_state const &, name const & n, unsigned, bool persistent) {
diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp
index 8b1baad6b0..8e35fb43a2 100644
--- a/src/library/compiler/extern_attribute.cpp
+++ b/src/library/compiler/extern_attribute.cpp
@@ -141,6 +141,10 @@ optional<extern_attr_data_value> get_extern_attr_data(environment const & env, n
     }
 }
 
+extern "C" object * lean_get_extern_attr_data(b_obj_arg env, b_obj_arg fn) {
+    return to_object(get_extern_attr_data(environment(env, true), name(fn, true)));
+}
+
 optional<std::string> get_extern_name_for(environment const & env, name const & backend, name const & fn) {
     if (std::shared_ptr<extern_attr_data> const & data = get_extern_attr().get(env, fn)) {
         extern_attr_data_value const & v = data->m_value;
diff --git a/src/util/object_ref.h b/src/util/object_ref.h
index 8916cccdd6..99b188d9f9 100644
--- a/src/util/object_ref.h
+++ b/src/util/object_ref.h
@@ -62,64 +62,64 @@ inline object_ref mk_cnstr(unsigned tag, object * o1, object * o2, object * o3,
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 1, scalar_sz);
-    cnstr_set(r, 0, o.raw()); inc(o.raw());
+    cnstr_set(r, 0, o.to_obj_arg());
     return object_ref(r);
 }
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const & o2, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 2, scalar_sz);
-    cnstr_set(r, 0, o1.raw()); inc(o1.raw());
-    cnstr_set(r, 1, o2.raw()); inc(o2.raw());
+    cnstr_set(r, 0, o1.to_obj_arg());
+    cnstr_set(r, 1, o2.to_obj_arg());
     return object_ref(r);
 }
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const & o2, object_ref const & o3, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 3, scalar_sz);
-    cnstr_set(r, 0, o1.raw()); inc(o1.raw());
-    cnstr_set(r, 1, o2.raw()); inc(o2.raw());
-    cnstr_set(r, 2, o3.raw()); inc(o3.raw());
+    cnstr_set(r, 0, o1.to_obj_arg());
+    cnstr_set(r, 1, o2.to_obj_arg());
+    cnstr_set(r, 2, o3.to_obj_arg());
     return object_ref(r);
 }
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const & o2, object_ref const & o3, object_ref const & o4, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 4, scalar_sz);
-    cnstr_set(r, 0, o1.raw()); inc(o1.raw());
-    cnstr_set(r, 1, o2.raw()); inc(o2.raw());
-    cnstr_set(r, 2, o3.raw()); inc(o3.raw());
-    cnstr_set(r, 3, o4.raw()); inc(o4.raw());
+    cnstr_set(r, 0, o1.to_obj_arg());
+    cnstr_set(r, 1, o2.to_obj_arg());
+    cnstr_set(r, 2, o3.to_obj_arg());
+    cnstr_set(r, 3, o4.to_obj_arg());
     return object_ref(r);
 }
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const & o2, object_ref const & o3, object_ref const & o4, object_ref const & o5, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 5, scalar_sz);
-    cnstr_set(r, 0, o1.raw()); inc(o1.raw());
-    cnstr_set(r, 1, o2.raw()); inc(o2.raw());
-    cnstr_set(r, 2, o3.raw()); inc(o3.raw());
-    cnstr_set(r, 3, o4.raw()); inc(o4.raw());
-    cnstr_set(r, 4, o5.raw()); inc(o5.raw());
+    cnstr_set(r, 0, o1.to_obj_arg());
+    cnstr_set(r, 1, o2.to_obj_arg());
+    cnstr_set(r, 2, o3.to_obj_arg());
+    cnstr_set(r, 3, o4.to_obj_arg());
+    cnstr_set(r, 4, o5.to_obj_arg());
     return object_ref(r);
 }
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const & o2, object_ref const & o3, object_ref const & o4, object_ref const & o5, object_ref const & o6, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 6, scalar_sz);
-    cnstr_set(r, 0, o1.raw()); inc(o1.raw());
-    cnstr_set(r, 1, o2.raw()); inc(o2.raw());
-    cnstr_set(r, 2, o3.raw()); inc(o3.raw());
-    cnstr_set(r, 3, o4.raw()); inc(o4.raw());
-    cnstr_set(r, 4, o5.raw()); inc(o5.raw());
-    cnstr_set(r, 5, o6.raw()); inc(o6.raw());
+    cnstr_set(r, 0, o1.to_obj_arg());
+    cnstr_set(r, 1, o2.to_obj_arg());
+    cnstr_set(r, 2, o3.to_obj_arg());
+    cnstr_set(r, 3, o4.to_obj_arg());
+    cnstr_set(r, 4, o5.to_obj_arg());
+    cnstr_set(r, 5, o6.to_obj_arg());
     return object_ref(r);
 }
 
 inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const & o2, object_ref const & o3, object_ref const & o4, object_ref const & o5, object_ref const & o6, object_ref const & o7, unsigned scalar_sz = 0) {
     object * r = alloc_cnstr(tag, 7, scalar_sz);
-    cnstr_set(r, 0, o1.raw()); inc(o1.raw());
-    cnstr_set(r, 1, o2.raw()); inc(o2.raw());
-    cnstr_set(r, 2, o3.raw()); inc(o3.raw());
-    cnstr_set(r, 3, o4.raw()); inc(o4.raw());
-    cnstr_set(r, 4, o5.raw()); inc(o5.raw());
-    cnstr_set(r, 5, o6.raw()); inc(o6.raw());
-    cnstr_set(r, 6, o7.raw()); inc(o7.raw());
+    cnstr_set(r, 0, o1.to_obj_arg());
+    cnstr_set(r, 1, o2.to_obj_arg());
+    cnstr_set(r, 2, o3.to_obj_arg());
+    cnstr_set(r, 3, o4.to_obj_arg());
+    cnstr_set(r, 4, o5.to_obj_arg());
+    cnstr_set(r, 5, o6.to_obj_arg());
+    cnstr_set(r, 6, o7.to_obj_arg());
     return object_ref(r);
 }
 
@@ -149,4 +149,14 @@ template<typename T> optional<T> to_optional(b_obj_arg o, bool) {
     T r(cnstr_get(o, 0), true);
     return optional<T>(r);
 }
+
+template<typename T> obj_res to_object(optional<T> const & o) {
+    if (o) {
+        obj_res r = alloc_cnstr(1, 1, 0);
+        cnstr_set(r, 0, o->to_obj_arg());
+        return r;
+    } else {
+        return box(0);
+    }
+}
 }