diff --git a/library/init/system/io.lean b/library/init/system/io.lean
index 4f8b2c0ea0..fc1f087ab1 100644
--- a/library/init/system/io.lean
+++ b/library/init/system/io.lean
@@ -119,7 +119,15 @@ constant handle.close (h : @& handle) : IO Unit := default _
 constant handle.getLine (h : @& handle) : IO String := default _
 
 @[extern 2 "lean_io_getenv"]
-constant getEnv (var : String) : IO (Option String) := default _
+constant getEnv (var : @& String) : IO (Option String) := default _
+@[extern 2 "lean_io_realpath"]
+constant realPath (fname : String) : IO String := default _
+@[extern 2 "lean_io_is_dir"]
+constant isDir (fname : @& String) : IO Bool := default _
+@[extern 2 "lean_io_file_exists"]
+constant fileExists (fname : @& String) : IO Bool := default _
+@[extern 1 "lean_io_app_dir"]
+constant appDir : IO String := default _
 
 @[inline] def liftIO {m : Type → Type} {α : Type} [monadIO m] (x : IO α) : m α :=
 monadLift x
@@ -131,17 +139,14 @@ variables {m : Type → Type} [Monad m] [monadIO m]
 private def putStr : String → m Unit :=
 Prim.liftIO ∘ Prim.putStr
 
-def print {α} [HasToString α] (s : α) : m Unit :=
-putStr ∘ toString $ s
-
-def println {α} [HasToString α] (s : α) : m Unit :=
-print s *> putStr "\n"
-
-def readTextFile : String → m String :=
-Prim.liftIO ∘ Prim.readTextFile
-
-def getEnv : String → m (Option String) :=
-Prim.liftIO ∘ Prim.getEnv
+def print {α} [HasToString α] (s : α) : m Unit := putStr ∘ toString $ s
+def println {α} [HasToString α] (s : α) : m Unit := print s *> putStr "\n"
+def readTextFile : String → m String := Prim.liftIO ∘ Prim.readTextFile
+def getEnv : String → m (Option String) := Prim.liftIO ∘ Prim.getEnv
+def realPath : String → m String := Prim.liftIO ∘ Prim.realPath
+def isDir : String → m Bool := Prim.liftIO ∘ Prim.isDir
+def fileExists : String → m Bool := Prim.liftIO ∘ Prim.fileExists
+def appDir : m String := Prim.liftIO Prim.appDir
 
 end
 
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index a3550f54de..87119ab1e0 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -6,6 +6,11 @@ Author: Leonardo de Moura
 */
 #if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
 #include <windows.h>
+#elif defined(__APPLE__)
+#include <mach-o/dyld.h>
+#else
+// Linux include files
+#include <unistd.h>
 #endif
 #include <iostream>
 #include <chrono>
@@ -153,7 +158,7 @@ extern "C" obj_res lean_io_allocprof(obj_arg, b_obj_arg msg, obj_arg fn, obj_arg
     return apply_1(fn, r);
 }
 
-extern "C" obj_res lean_io_getenv(obj_arg env_var, obj_arg r) {
+extern "C" obj_res lean_io_getenv(b_obj_arg env_var, obj_arg r) {
     char * val = std::getenv(string_cstr(env_var));
     if (val) {
         return set_io_result(r, mk_option_some(mk_string(val)));
@@ -204,6 +209,36 @@ extern "C" obj_res lean_io_file_exists(b_obj_arg fname, obj_arg r) {
     return set_io_result(r, box(b));
 }
 
+extern "C" obj_res lean_io_app_dir(obj_arg r) {
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+    HMODULE hModule = GetModuleHandleW(NULL);
+    WCHAR path[MAX_PATH];
+    GetModuleFileNameW(hModule, path, MAX_PATH);
+    return set_io_result(r, mk_string(path));
+#elif defined(__APPLE__)
+    char buf1[PATH_MAX];
+    char buf2[PATH_MAX];
+    uint32_t bufsize = PATH_MAX;
+    if (_NSGetExecutablePath(buf1, &bufsize) != 0)
+        return set_io_error(r, mk_string("failed to locate application"));
+    if (!realpath(buf1, buf2))
+        return set_io_error(r, mk_string("failed to resolve symbolic links when locating application"));
+    return set_io_result(r, mk_string(buf2));
+#else
+    // Linux version
+    char path[PATH_MAX];
+    char dest[PATH_MAX];
+    memset(dest, 0, PATH_MAX);
+    pid_t pid = getpid();
+    snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+    if (readlink(path, dest, PATH_MAX) == -1) {
+        return set_io_error(r, mk_string("failed to locate application"));
+    } else {
+        return set_io_result(r, mk_string(dest));
+    }
+#endif
+}
+
 // =======================================
 // IO ref primitives
 obj_res io_mk_ref(obj_arg a, obj_arg r) {
diff --git a/tests/playground/dir.lean b/tests/playground/dir.lean
new file mode 100644
index 0000000000..84d947e658
--- /dev/null
+++ b/tests/playground/dir.lean
@@ -0,0 +1,10 @@
+def main (xs : List String) : IO Unit :=
+do
+  b₁ ← IO.isDir xs.head;
+  b₂ ← IO.fileExists xs.head;
+  d₁ ← IO.appDir;
+  d₂ ← IO.realPath ".";
+  IO.println b₁;
+  IO.println b₂;
+  IO.println d₁;
+  IO.println d₂