diff --git a/.clang-format b/.clang-format
new file mode 100644
index 0000000000..698eec9f32
--- /dev/null
+++ b/.clang-format
@@ -0,0 +1,5 @@
+---
+
+BreakBeforeBraces: 'Attach'
+
+IndentWidth: 4
diff --git a/library/system/io.lean b/library/system/io.lean
index c690696d89..d3cfb5953c 100644
--- a/library/system/io.lean
+++ b/library/system/io.lean
@@ -1,9 +1,10 @@
 /-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
 -/
 import data.buffer
+import system.process
 
 inductive io.error
 | other     : string → io.error
@@ -16,9 +17,8 @@ structure io.terminal (m : Type → Type → Type) :=
 inductive io.mode
 | read | write | read_write | append
 
-structure io.file_system (m : Type → Type → Type) :=
+structure io.file_system (handle : Type) (m : Type → Type → Type) :=
 /- Remark: in Haskell, they also provide  (Maybe TextEncoding) and  NewlineMode -/
-(handle         : Type)
 (read_file      : string → bool → m io.error char_buffer)
 (mk_file_handle : string → io.mode → bool → m io.error handle)
 (is_eof         : handle → m io.error bool)
@@ -36,8 +36,12 @@ class io.interface :=
 (monad    : Π e, monad (m e))
 (catch    : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α)
 (fail     : Π e α, e → m e α)
+-- Primitive Types
+(handle   : Type)
+-- Interface Extensions
 (term     : io.terminal m)
-(fs       : io.file_system m)
+(fs       : io.file_system handle m)
+(process  : io.process io.error handle m)
 
 variable [io.interface]
 
@@ -74,7 +78,7 @@ def print_ln {α} [has_to_string α] (s : α) : io unit :=
 print s >> put_str "\n"
 
 def handle : Type :=
-interface.fs.handle
+interface.handle
 
 def mk_file_handle (s : string) (m : mode) (bin : bool := ff) : io handle :=
 interface.fs.mk_file_handle s m bin
@@ -137,4 +141,23 @@ format.print_using (to_fmt a) o
 meta definition pp {α : Type} [has_to_format α] (a : α) : io unit :=
 format.print (to_fmt a)
 
+/-- Run the external process named by `cmd`, supplied with the arguments `args`.
+
+    The process will run to completion with its output captured by a pipe, and
+    read into `string` which is then returned.
+-/
+def io.cmd [io.interface] (cmd : string) (args : list string) : io string :=
+do let proc : process := {
+    cmd := cmd,
+    args := args,
+    stdout := process.stdio.piped
+  },
+  child ← interface.process^.spawn proc,
+  let inh := child^.stdin,
+  let outh := child^.stdout,
+  let errh := child^.stderr,
+  buf ← io.fs.read outh 1024,
+  return buf^.to_string
+
+/-- Lift a monadic `io` action into the `tactic` monad. -/
 meta constant tactic.run_io {α : Type} : (Π ioi : io.interface, @io ioi α) → tactic α
diff --git a/library/system/process.lean b/library/system/process.lean
new file mode 100644
index 0000000000..d2dbb6aa99
--- /dev/null
+++ b/library/system/process.lean
@@ -0,0 +1,25 @@
+import init.data.list.basic
+
+inductive process.stdio
+| piped
+| inherit
+| null
+
+structure process :=
+(cmd : string)
+/- Add an argument to pass to the process. -/
+(args : list string)
+/- Configuration for the process's stdin handle. -/
+(stdin := stdio.inherit)
+/- Configuration for the process's stdout handle. -/
+(stdout := stdio.inherit)
+/- Configuration for the process's stderr handle. -/
+(stderr := stdio.inherit)
+
+structure process.child (handle : Type) :=
+(stdin : handle)
+(stdout : handle)
+(stderr : handle)
+
+structure io.process (err : Type) (handle : Type) (m : Type → Type → Type) :=
+(spawn : process → m err (process.child handle))
diff --git a/library/tools/smt2/builder.lean b/library/tools/smt2/builder.lean
new file mode 100644
index 0000000000..a924f16930
--- /dev/null
+++ b/library/tools/smt2/builder.lean
@@ -0,0 +1,48 @@
+import .syntax
+
+@[reducible] def smt2.builder (α : Type) := state (list smt2.cmd) α
+
+meta def smt2.builder.to_format {α : Type} (build : smt2.builder α) : format :=
+format.join $ list.map to_fmt $ (build [])^.snd
+
+meta instance (α : Type) : has_to_format (smt2.builder α) :=
+⟨ smt2.builder.to_format ⟩
+
+namespace smt2
+
+namespace builder
+
+def add_command (c : cmd) : builder unit := do
+cs ← state.read,
+state.write (c :: cs)
+
+def echo (msg : string) : builder unit :=
+add_command (cmd.echo msg)
+
+def check_sat : builder unit :=
+add_command cmd.check_sat
+
+def pop (n : nat) : builder unit :=
+add_command $ cmd.pop n
+
+def push (n : nat) : builder unit :=
+add_command $ cmd.push n
+
+def scope {α} (level : nat) (action : builder α) : builder α :=
+do push level,
+   res ← action,
+   pop level,
+   return res
+
+def reset : builder unit :=
+add_command cmd.reset
+
+def exit' : builder unit :=
+add_command cmd.exit_cmd
+
+def declare_const (sym : string) (s : sort) : builder unit :=
+add_command $ cmd.declare_const sym s
+
+end builder
+
+end smt2
diff --git a/library/tools/smt2/default.lean b/library/tools/smt2/default.lean
new file mode 100644
index 0000000000..d723affe60
--- /dev/null
+++ b/library/tools/smt2/default.lean
@@ -0,0 +1,37 @@
+import system.io
+import system.process
+import .solvers.z3
+import .syntax
+import .builder
+
+meta def smt2 [io.interface] (build : smt2.builder unit) : io string :=
+do z3 ← z3_instance.start,
+   io.put_str (to_string $ to_fmt build),
+   res ← z3^.raw (to_string $ to_fmt build),
+   io.put_str res,
+   return res
+
+open tactic
+open smt2
+open smt2.builder
+
+meta def reflect_prop (e : expr) : tactic (builder unit) :=
+do p ← is_prop e,
+   if p
+   then do
+       trace e,
+       n ← mk_fresh_name,
+       return $ declare_const (to_string n) "Bool"
+   else return (return ())
+
+meta def reflect_context : tactic (builder unit) :=
+do ls ← local_context,
+   bs ← monad.mapm reflect_prop ls,
+   return $ list.foldl (λ (a b : builder unit), a >> b) (return ()) bs
+
+meta def reflect : tactic unit :=
+do tgt ← target,
+   b ← reflect_context,
+   str ← run_io (λ ioi, @smt2 ioi b),
+   tactic.trace str,
+   return ()
diff --git a/library/tools/smt2/solvers/z3.lean b/library/tools/smt2/solvers/z3.lean
new file mode 100644
index 0000000000..48575ed62f
--- /dev/null
+++ b/library/tools/smt2/solvers/z3.lean
@@ -0,0 +1,30 @@
+import system.io
+import system.process
+import data.buffer
+
+open process
+
+structure z3_instance [io.interface] : Type :=
+  (process : child io.handle)
+
+def spawn [ioi : io.interface] : process → io (child io.handle) :=
+io.interface.process^.spawn
+
+def z3_instance.start  [io.interface] : io z3_instance :=
+do let proc : process := {
+       cmd := "z3",
+       args := ["-smt2", "-in"],
+       stdin := stdio.piped,
+       stdout := stdio.piped
+    },
+    z3_instance.mk <$> spawn proc
+
+def z3_instance.raw [io.interface] (z3 : z3_instance) (cmd : string) : io string :=
+do let z3_stdin := z3^.process^.stdin,
+   let z3_stdout := z3^.process^.stdout,
+   let cs := cmd^.reverse^.to_buffer,
+   io.fs.write z3_stdin cs,
+   io.fs.close z3_stdin,
+   -- need read all
+   res ← io.fs.read z3_stdout 1024,
+   return res^.to_string
diff --git a/library/tools/smt2/syntax.lean b/library/tools/smt2/syntax.lean
new file mode 100644
index 0000000000..02cebae465
--- /dev/null
+++ b/library/tools/smt2/syntax.lean
@@ -0,0 +1,87 @@
+namespace smt2
+
+@[reducible] def symbol : Type := string
+@[reducible] def identifier : Type := string
+
+inductive special_constant : Type
+| number : int → special_constant
+| string : string → special_constant
+
+inductive sort : Type
+| id : identifier → sort
+| apply : identifier → list sort → sort
+
+instance : has_coe string sort :=
+⟨ fun str, sort.id str ⟩
+
+meta def sort.to_format : sort → format
+| (sort.id i) := to_fmt i
+| (sort.apply _ _) := "NYI"
+
+meta instance sort_has_to_fmt : has_to_format sort :=
+⟨ sort.to_format ⟩
+
+inductive attr : Type
+
+inductive qualified_name : Type
+| id : identifier → qualified_name
+| qual_id : identifier → sort → qualified_name
+
+inductive term : Type
+| qual_id : qualified_name → term
+| const : special_constant → term
+| apply : qualified_name → list term → term
+| letb : list (name × term) → term → term
+| forallq : list (symbol × sort) → term → term
+| existsq : list (symbol × sort) → term → term
+| annotate : term → list attr → term
+
+inductive fun_def : Type
+inductive info_flag : Type
+inductive keyword : Type
+inductive option : Type
+
+inductive cmd : Type
+| assert_cmd : term → cmd
+| check_sat : cmd
+| check_sat_assuming : term → cmd -- not complete
+| declare_const : symbol → sort → cmd
+| declare_fun : symbol → list sort → cmd
+| declare_sort : symbol → nat → cmd
+| define_fun : fun_def → cmd
+| define_fun_rec : fun_def → cmd
+| define_funs_rec : cmd -- not complete
+| define_sort : symbol → list symbol → sort → cmd
+| echo : string → cmd
+| exit_cmd : cmd
+| get_assertions : cmd
+| get_assignment : cmd
+| get_info : info_flag → cmd
+| get_model : cmd
+| get_option : keyword → cmd
+| get_proof : cmd
+| get_unsat_assumtpions : cmd
+| get_unsat_core : cmd
+| get_value : cmd -- not complete
+| pop : nat → cmd
+| push : nat → cmd
+| reset : cmd
+| reset_assertions : cmd
+| set_info : attr → cmd
+| set_logic : symbol → cmd
+| set_opt : option → cmd
+
+open cmd
+
+meta def string_lit (s : string) : format :=
+format.bracket "\"" "\"" (to_fmt s)
+
+meta def cmd.to_format : cmd → format
+| (echo msg) := "(echo " ++ string_lit msg ++ ")\n"
+| (declare_const sym srt) := "(declare-const " ++ sym ++ " " ++ to_fmt srt ++ ")"
+| _ := "NYI"
+
+meta instance : has_to_format cmd :=
+⟨ cmd.to_format ⟩
+
+end smt2
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 6459d5de08..e42ba97a02 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -19,4 +19,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   mt_task_queue.cpp st_task_queue.cpp
   library_task_builder.cpp
   messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
-  documentation.cpp check.cpp arith_instance.cpp parray.cpp)
+  documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp
+  pipe.cpp handle.cpp)
diff --git a/src/library/handle.cpp b/src/library/handle.cpp
new file mode 100644
index 0000000000..186323cf2f
--- /dev/null
+++ b/src/library/handle.cpp
@@ -0,0 +1,77 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author:  Leonardo de Moura & Jared Roesch
+*/
+#include <string>
+#include <fstream>
+#include <iostream>
+#include <iomanip>
+#include <utility>
+#include <stdio.h>
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#include <windows.h>
+#include <tchar.h>
+#include <strsafe.h>
+#else
+#include <sys/wait.h>
+#include <unistd.h>
+#endif
+
+#include "library/process.h"
+#include "library/handle.h"
+#include "util/buffer.h"
+#include "library/pipe.h"
+
+
+namespace lean {
+
+void handle::write(buffer<char> & buf) {
+    auto sz = buf.size();
+    if (fwrite(buf.data(), 1, sz, m_file) != sz) {
+        std::cout << "write_error: " << errno << std::endl;
+        clearerr(m_file);
+        throw handle_exception("write failed");
+    }
+}
+
+void handle::flush() {
+    if (fflush(m_file) != 0) {
+        clearerr(m_file);
+        throw handle_exception("flush failed");
+    }
+}
+
+handle::~handle() {
+    if (m_file && m_file != stdin &&
+        m_file != stderr && m_file != stdout) {
+        fclose(m_file);
+    }
+}
+
+bool handle::is_stdin() {
+    return m_file == stdin;
+}
+
+bool handle::is_stdout() {
+    return m_file == stdout;
+}
+
+bool handle::is_stderr() {
+    return m_file == stderr;
+}
+
+void handle::close() {
+    if (fclose(m_file) == 0) {
+        m_file = nullptr;
+    } else {
+        clearerr(m_file);
+        throw handle_exception("close failed");
+    }
+}
+
+bool handle::is_closed() { return !m_file; }
+
+}
diff --git a/src/library/handle.h b/src/library/handle.h
new file mode 100644
index 0000000000..5a3668eb8e
--- /dev/null
+++ b/src/library/handle.h
@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author:  Leonardo de Moura & Jared Roesch
+*/
+#pragma once
+
+#include <iostream>
+#include <string>
+#include <unistd.h>
+#include "util/buffer.h"
+#include "library/pipe.h"
+
+namespace lean {
+
+class handle_exception : exception {
+public:
+    handle_exception(std::string msg) : exception(msg) {}
+};
+
+class handle {
+public:
+    FILE * m_file;
+    handle(FILE * file_desc):m_file(file_desc) {}
+
+    void close();
+
+    ~handle();
+
+    void write(buffer<char> & data);
+    void read(buffer<char> & data);
+    void flush();
+
+    bool is_stdin();
+    bool is_stdout();
+    bool is_stderr();
+    bool is_closed();
+};
+
+typedef std::shared_ptr<handle> handle_ref;
+
+}
diff --git a/src/library/native_compiler/cpp_compiler.cpp b/src/library/native_compiler/cpp_compiler.cpp
index 68b3ed4833..c60968ab6c 100644
--- a/src/library/native_compiler/cpp_compiler.cpp
+++ b/src/library/native_compiler/cpp_compiler.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jared Roesch
 */
 #include <string>
-#include "util/process.h"
+#include "library/process.h"
 #include "library/native_compiler/cpp_compiler.h"
 
 namespace lean {
diff --git a/src/library/pipe.cpp b/src/library/pipe.cpp
new file mode 100644
index 0000000000..8a3537c70a
--- /dev/null
+++ b/src/library/pipe.cpp
@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Jared Roesch
+*/
+
+#include "library/pipe.h"
+#include "util/exception.h"
+
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#else
+#include <unistd.h>
+#endif
+
+namespace lean {
+
+pipe::pipe() {
+    #if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+    #else
+    int fds[2];
+    if (::pipe(fds) == -1) {
+        throw exception("unable to create pipe");
+    } else {
+        m_read_fd = fds[0];
+        m_write_fd = fds[1];
+    }
+    #endif
+}
+
+}
diff --git a/src/library/pipe.h b/src/library/pipe.h
new file mode 100644
index 0000000000..a75595c635
--- /dev/null
+++ b/src/library/pipe.h
@@ -0,0 +1,43 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Jared Roesch
+*/
+#pragma once
+
+#include <iostream>
+#include <string>
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+typedef void* HANDLE;
+#else
+#endif
+
+namespace lean  {
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+
+struct pipe {
+    HANDLE m_read_fd;
+    HANDLE m_write_fd;
+    pipe();
+    pipe(HANDLE read_fd, HANDLE write_fd) :
+        m_read_fd(read_fd), m_write_fd(write_fd) {}
+    pipe(pipe const & p) :
+        m_read_fd(p.m_read_fd), m_write_fd(p.m_write_fd) {}
+};
+#else
+struct pipe {
+    int m_read_fd;
+    int m_write_fd;
+    pipe();
+    pipe(int read_fd, int write_fd) :
+        m_read_fd(read_fd), m_write_fd(write_fd) {}
+    pipe(pipe const & p) :
+        m_read_fd(p.m_read_fd), m_write_fd(p.m_write_fd) {}
+};
+
+#endif
+
+}
diff --git a/src/library/process.cpp b/src/library/process.cpp
new file mode 100644
index 0000000000..3d0f940280
--- /dev/null
+++ b/src/library/process.cpp
@@ -0,0 +1,332 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Jared Roesch
+*/
+#include <string>
+#include <fstream>
+#include <iostream>
+#include <iomanip>
+#include <utility>
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+#include <windows.h>
+#include <Fcntl.h>
+#include <io.h>
+#include <tchar.h>
+#include <stdio.h>
+#include <strsafe.h>
+#else
+#include <sys/wait.h>
+#endif
+
+#include "library/process.h"
+#include "util/buffer.h"
+#include "library/pipe.h"
+
+namespace lean {
+
+process::process(std::string n): m_proc_name(n), m_args() {
+    m_args.push_back(m_proc_name);
+}
+
+process & process::arg(std::string a) {
+    m_args.push_back(a);
+    return *this;
+}
+
+process & process::set_stdin(stdio cfg) {
+    m_stdin = optional<stdio>(cfg);
+    return *this;
+}
+
+process & process::set_stdout(stdio cfg) {
+    m_stdout = optional<stdio>(cfg);
+    return *this;
+}
+
+process & process::set_stderr(stdio cfg) {
+    m_stderr = optional<stdio>(cfg);
+    return *this;
+}
+
+#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
+
+HANDLE to_win_handle(FILE * file) {
+    intptr_t handle = _get_osfhandle(fileno(file));
+    return reinterpret_cast<HANDLE>(handle);
+}
+
+FILE * from_win_handle(HANDLE handle, char const * mode) {
+    int fd = _open_osfhandle(reinterpret_cast<intptr_t>(handle), _O_APPEND);
+    return fdopen(fd, mode);
+}
+
+void create_child_process(std::string cmd_name, HANDLE hstdin, HANDLE hstdout, HANDLE hstderr);
+
+// TODO(@jroesch): unify this code between platforms better.
+static optional<pipe> setup_stdio(SECURITY_ATTRIBUTES * saAttr, optional<stdio> cfg) {
+    /* Setup stdio based on process configuration. */
+    if (cfg) {
+        switch (*cfg) {
+        /* We should need to do nothing in this case */
+        case stdio::INHERIT:
+            return optional<pipe>();
+        case stdio::PIPED: {
+            HANDLE readh;
+            HANDLE writeh;
+            if (!CreatePipe(&readh, &writeh, saAttr, 0))
+                throw new exception("unable to create pipe");
+            return optional<pipe>(lean::pipe(readh, writeh));
+        }
+        case stdio::NUL: {
+            /* We should map /dev/null. */
+            return optional<pipe>();
+        }
+        default:
+           lean_unreachable();
+        }
+    } else {
+        return optional<pipe>();
+    }
+}
+
+// This code is adapted from: https://msdn.microsoft.com/en-us/library/windows/desktop/ms682499(v=vs.85).aspx
+child process::spawn() {
+    HANDLE child_stdin = stdin;
+    HANDLE child_stdout = stdout;
+    HANDLE child_stderr = stderr;
+    HANDLE parent_stdin = stdin;
+    HANDLE parent_stdout = stdout;
+    HANDLE parent_stderr = stderr;
+
+    SECURITY_ATTRIBUTES saAttr;
+
+    // Set the bInheritHandle flag so pipe handles are inherited.
+    saAttr.nLength = sizeof(SECURITY_ATTRIBUTES);
+    saAttr.bInheritHandle = TRUE;
+    saAttr.lpSecurityDescriptor = NULL;
+
+    auto stdin_pipe = setup_stdio(&saAttr, m_stdin);
+    auto stdout_pipe = setup_stdio(&saAttr, m_stdout);
+    auto stderr_pipe = setup_stdio(&saAttr, m_stderr);
+
+    if (stdin_pipe) {
+        // Ensure the write handle to the pipe for STDIN is not inherited.
+        if (!SetHandleInformation(stdin_pipe->m_write_fd, HANDLE_FLAG_INHERIT, 0))
+            throw new exception("unable to configure stdin pipe");
+        child_stdin = stdin_pipe->m_read_fd;
+    }
+
+    // Create a pipe for the child process's STDOUT.
+    if (stdout_pipe) {
+        // Ensure the read handle to the pipe for STDOUT is not inherited.
+        if (!SetHandleInformation(stdout_pipe->m_read_fd, HANDLE_FLAG_INHERIT, 0))
+            throw new exception("unable to configure stdout pipe");
+        child_stdout = stdout_pipe->m_write_fd;
+    }
+
+    if (stderr_pipe) {
+        // Ensure the read handle to the pipe for STDOUT is not inherited.
+        if (!SetHandleInformation(stderr_pipe->m_read_fd, HANDLE_FLAG_INHERIT, 0))
+            throw new exception("unable to configure stdout pipe");
+        child_stderr = stderr_pipe->m_write_fd;
+    }
+
+    std::string command;
+
+    // This needs some thought, on Windows we must pass a command string
+    // which is a valid command, that is a fully assembled command to be executed.
+    //
+    // We must escape the arguments to preseving spacing and other characters,
+    // we might need to revisit escaping here.
+    bool once_through = false;
+    for (auto arg : m_args) {
+        if (once_through) {
+            command += " \"";
+        }
+        command += arg;
+        if (once_through) {
+            command += "\"";
+        }
+        once_through = true;
+    }
+
+    // Create the child process.
+    create_child_process(command, child_stdin, child_stdout, child_stderr);
+
+    if (stdin_pipe) {
+        CloseHandle(stdin_pipe->m_read_fd);
+        parent_stdin = stdin_pipe->m_write_fd;
+    }
+
+    if (stdout_pipe) {
+        CloseHandle(stdout_pipe->m_write_fd);
+        parent_stdout = stdout_pipe->m_read_fd;
+    }
+
+    if (stderr_pipe) {
+        CloseHandle(stderr_pipe->m_write_fd);
+        parent_stderr = stderr_pipe->m_read_fd;
+    }
+
+    return child(
+        0,
+        std::make_shared<handle>(from_win_handle(parent_stdin, "w")),
+        std::make_shared<handle>(from_win_handle(parent_stdout, "r")),
+        std::make_shared<handle>(from_win_handle(parent_stderr, "r")));
+}
+
+// Create a child process that uses the previously created pipes for STDIN and STDOUT.
+void create_child_process(std::string command, HANDLE hstdin, HANDLE hstdout, HANDLE hstderr) {
+    PROCESS_INFORMATION piProcInfo;
+    STARTUPINFO siStartInfo;
+    BOOL bSuccess = FALSE;
+
+    // Set up members of the PROCESS_INFORMATION structure.
+    ZeroMemory(&piProcInfo, sizeof(PROCESS_INFORMATION));
+
+    // Set up members of the STARTUPINFO structure.
+    // This structure specifies the STDIN and STDOUT handles for redirection.
+
+    ZeroMemory(&siStartInfo, sizeof(STARTUPINFO));
+    siStartInfo.cb = sizeof(STARTUPINFO);
+    siStartInfo.hStdError = hstderr;
+    siStartInfo.hStdOutput = hstdout;
+    siStartInfo.hStdInput = hstdin;
+    siStartInfo.dwFlags |= STARTF_USESTDHANDLES;
+
+    // Create the child process.
+    // std::cout << command << std::endl;
+    bSuccess = CreateProcess(
+        NULL,
+        const_cast<char *>(command.c_str()), // command line
+        NULL,                                // process security attributes
+        NULL,                                // primary thread security attributes
+        TRUE,                                // handles are inherited
+        0,                                   // creation flags
+        NULL,                                // use parent's environment
+        NULL,                                // use parent's current directory
+        &siStartInfo,                        // STARTUPINFO pointer
+        &piProcInfo);                        // receives PROCESS_INFORMATION
+
+    // If an error occurs, exit the application.
+    if (!bSuccess) {
+        throw exception("failed to start child process");
+    } else {
+        // Close handles to the child process and its primary thread.
+        // Some applications might keep these handles to monitor the status
+        // of the child process, for example.
+
+        CloseHandle(piProcInfo.hProcess);
+        CloseHandle(piProcInfo.hThread);
+    }
+}
+
+void process::run() {
+     throw exception("process::run not supported on Windows");
+}
+
+#else
+
+optional<pipe> setup_stdio(optional<stdio> cfg) {
+    /* Setup stdio based on process configuration. */
+    if (cfg) {
+        switch (*cfg) {
+        /* We should need to do nothing in this case */
+        case stdio::INHERIT:
+            return optional<pipe>();
+        case stdio::PIPED: {
+            return optional<pipe>(lean::pipe());
+        }
+        case stdio::NUL: {
+            /* We should map /dev/null. */
+            return optional<pipe>();
+        }
+        default:
+           lean_unreachable();
+        }
+    } else {
+        return optional<pipe>();
+    }
+}
+
+child process::spawn() {
+    /* Setup stdio based on process configuration. */
+    auto stdin_pipe = setup_stdio(m_stdin);
+    auto stdout_pipe = setup_stdio(m_stdout);
+    auto stderr_pipe = setup_stdio(m_stderr);
+
+    int pid = fork();
+
+    if (pid == 0) {
+        if (stdin_pipe) {
+            dup2(stdin_pipe->m_read_fd, STDIN_FILENO);
+            close(stdin_pipe->m_write_fd);
+        }
+
+        if (stdout_pipe) {
+            dup2(stdout_pipe->m_write_fd, STDOUT_FILENO);
+            close(stdout_pipe->m_read_fd);
+        }
+
+        if (stderr_pipe) {
+            dup2(stderr_pipe->m_write_fd, STDERR_FILENO);
+            close(stderr_pipe->m_read_fd);
+        }
+
+        buffer<char*> pargs;
+
+        for (auto arg : this->m_args) {
+            auto str = new char[arg.size() + 1];
+            arg.copy(str, arg.size());
+            str[arg.size()] = '\0';
+            pargs.push_back(str);
+        }
+
+        pargs.data()[pargs.size()] = NULL;
+
+        auto err = execvp(pargs.data()[0], pargs.data());
+        if (err < 0) {
+            throw std::runtime_error("executing process failed: ...");
+        }
+    } else if (pid == -1) {
+        throw std::runtime_error("forking process failed: ...");
+    }
+
+    /* We want to setup the parent's view of the file descriptors. */
+    int parent_stdin = STDIN_FILENO;
+    int parent_stdout = STDOUT_FILENO;
+    int parent_stderr = STDERR_FILENO;
+
+    if (stdin_pipe) {
+        close(stdin_pipe->m_read_fd);
+        parent_stdin = stdin_pipe->m_write_fd;
+    }
+
+    if (stdout_pipe) {
+        close(stdout_pipe->m_write_fd);
+        parent_stdout = stdout_pipe->m_read_fd;
+    }
+
+    if (stderr_pipe) {
+        close(stderr_pipe->m_write_fd);
+        parent_stderr = stderr_pipe->m_read_fd;
+    }
+
+    return child(pid,
+         std::make_shared<handle>(fdopen(parent_stdin, "w")),
+         std::make_shared<handle>(fdopen(parent_stdout, "r")),
+         std::make_shared<handle>(fdopen(parent_stderr, "r")));
+}
+
+void process::run() {
+    child ch = spawn();
+    int status;
+    waitpid(ch.m_pid, &status, 0);
+}
+
+#endif
+
+}
diff --git a/src/library/process.h b/src/library/process.h
new file mode 100644
index 0000000000..0c381d9e60
--- /dev/null
+++ b/src/library/process.h
@@ -0,0 +1,65 @@
+/*
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Jared Roesch
+*/
+#pragma once
+
+#include <iostream>
+#include <string>
+#include "library/handle.h"
+#include "util/buffer.h"
+#include "library/pipe.h"
+
+namespace lean  {
+
+enum stdio {
+    INHERIT,
+    PIPED,
+    NUL,
+};
+
+struct child {
+    handle_ref m_stdin;
+    handle_ref m_stdout;
+    handle_ref m_stderr;
+    int m_pid;
+
+    child(child const & ch) :
+        m_stdin(ch.m_stdin),
+        m_stdout(ch.m_stdout),
+        m_stderr(ch.m_stderr),
+        m_pid(ch.m_pid) {}
+
+    child(int pid, handle_ref hstdin, handle_ref hstdout, handle_ref hstderr) :
+        m_stdin(hstdin),
+        m_stdout(hstdout),
+        m_stderr(hstderr),
+        m_pid(pid) {}
+
+    void wait();
+};
+
+class process {
+    std::string m_proc_name;
+    buffer<std::string> m_args;
+    optional<stdio> m_stdout;
+    optional<stdio> m_stdin;
+    optional<stdio> m_stderr;
+public:
+    process(process const & proc) :
+        m_proc_name(proc.m_proc_name),
+        m_args(proc.m_args),
+        m_stdout(proc.m_stdout),
+        m_stdin(proc.m_stdin),
+        m_stderr(proc.m_stderr) {}
+    process(std::string exe_name);
+    process & arg(std::string arg_str);
+    process & set_stdin(stdio cfg);
+    process & set_stdout(stdio cfg);
+    process & set_stderr(stdio cfg);
+    child spawn();
+    void run();
+};
+}
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index cf38c241a7..7682e70d2b 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -699,6 +699,7 @@ vm_obj tactic_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) {
         return tactic::mk_exception(io_error_to_string(*e), tactic::to_state(s));
     }
 }
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),            tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}),    tactic_state_format_expr);
diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp
index d1b122822f..226539e26b 100644
--- a/src/library/vm/init_module.cpp
+++ b/src/library/vm/init_module.cpp
@@ -48,6 +48,7 @@ void initialize_vm_core_module() {
     initialize_vm_parser();
     initialize_vm_array();
 }
+
 void finalize_vm_core_module() {
     finalize_vm_array();
     finalize_vm_parser();
diff --git a/src/library/vm/vm_array.h b/src/library/vm/vm_array.h
index e90426f7d6..5b712da528 100644
--- a/src/library/vm/vm_array.h
+++ b/src/library/vm/vm_array.h
@@ -5,11 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+
 #include "library/parray.h"
 #include "library/vm/vm.h"
+
 namespace lean {
+
 parray<vm_obj> const & to_array(vm_obj const & o);
 vm_obj to_obj(parray<vm_obj> const & a);
+
 void initialize_vm_array();
 void finalize_vm_array();
 void initialize_vm_array_builtin_idxs();
diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index df5dd23511..c2ceca179a 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -8,11 +8,14 @@ Author: Leonardo de Moura
 #include <cstdio>
 #include <iostream>
 #include "util/sstream.h"
+#include "library/handle.h"
 #include "library/io_state.h"
 #include "library/tactic/tactic_state.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_array.h"
 #include "library/vm/vm_string.h"
+#include "library/vm/vm_io.h"
+#include "library/process.h"
 
 namespace lean {
 vm_obj mk_io_result(vm_obj const & r) {
@@ -57,14 +60,6 @@ static vm_obj mk_terminal() {
     return mk_vm_constructor(0, 2, fields);
 }
 
-struct handle {
-    FILE * m_handle;
-    handle(FILE * h):m_handle(h) {}
-    ~handle() { if (m_handle && m_handle != stdin && m_handle != stderr && m_handle != stdout) fclose(m_handle); }
-};
-
-typedef std::shared_ptr<handle> handle_ref;
-
 struct vm_handle : public vm_external {
     handle_ref m_handle;
     vm_handle(handle_ref const & h):m_handle(h) {}
@@ -116,42 +111,46 @@ static vm_obj mk_handle_has_been_closed_error() {
     return mk_io_failure("invalid io action, handle has been closed");
 }
 
-static bool has_been_closed(handle_ref const & href) {
-    return href->m_handle == nullptr;
-}
-
 static vm_obj fs_is_eof(vm_obj const & h, vm_obj const &) {
     handle_ref const & href = to_handle(h);
-    if (has_been_closed(href)) return mk_handle_has_been_closed_error();
-    bool r = feof(href->m_handle) != 0;
+    if (href->is_closed()) return mk_handle_has_been_closed_error();
+    bool r = feof(href->m_file) != 0;
     return mk_io_result(mk_vm_bool(r));
 }
 
 static vm_obj fs_flush(vm_obj const & h, vm_obj const &) {
     handle_ref const & href = to_handle(h);
-    if (has_been_closed(href)) return mk_handle_has_been_closed_error();
-    if (fflush(href->m_handle) == 0) {
+
+    if (href->is_closed()) {
+        return mk_handle_has_been_closed_error();
+    }
+
+    try {
+        href->flush();
         return mk_io_result(mk_vm_unit());
-    } else {
-        clearerr(href->m_handle);
+    } catch (handle_exception e) {
         return mk_io_failure("flush failed");
     }
 }
 
 static vm_obj fs_close(vm_obj const & h, vm_obj const &) {
     handle_ref const & href = to_handle(h);
-    if (has_been_closed(href)) return mk_handle_has_been_closed_error();
-    if (href->m_handle == stdin)
+
+    if (href->is_closed()) {
+        return mk_handle_has_been_closed_error();
+    }
+
+    if (href->is_stdin())
         return mk_io_failure("close failed, stdin cannot be closed");
-    if (href->m_handle == stdout)
+    if (href->is_stdout())
         return mk_io_failure("close failed, stdout cannot be closed");
-    if (href->m_handle == stderr)
+    if (href->is_stderr())
         return mk_io_failure("close failed, stderr cannot be closed");
-    if (fclose(href->m_handle) == 0) {
-        href->m_handle = nullptr;
+
+    try {
+        href->close();
         return mk_io_result(mk_vm_unit());
-    } else {
-        clearerr(href->m_handle);
+    } catch (handle_exception e) {
         return mk_io_failure("close failed");
     }
 }
@@ -162,13 +161,13 @@ static vm_obj mk_buffer(parray<vm_obj> const & a) {
 
 static vm_obj fs_read(vm_obj const & h, vm_obj const & n, vm_obj const &) {
     handle_ref const & href = to_handle(h);
-    if (has_been_closed(href)) return mk_handle_has_been_closed_error();
+    if (href->is_closed()) return mk_handle_has_been_closed_error();
     buffer<char> tmp;
     unsigned num = force_to_unsigned(n); /* TODO(Leo): handle size_t */
     tmp.resize(num, 0);
-    size_t sz = fread(tmp.data(), 1, num, href->m_handle);
-    if (ferror(href->m_handle)) {
-        clearerr(href->m_handle);
+    size_t sz = fread(tmp.data(), 1, num, href->m_file);
+    if (ferror(href->m_file)) {
+        clearerr(href->m_file);
         return mk_io_failure("read failed");
     }
     parray<vm_obj> r;
@@ -180,28 +179,38 @@ static vm_obj fs_read(vm_obj const & h, vm_obj const & n, vm_obj const &) {
 
 static vm_obj fs_write(vm_obj const & h, vm_obj const & b, vm_obj const &) {
     handle_ref const & href = to_handle(h);
-    if (has_been_closed(href)) return mk_handle_has_been_closed_error();
+
+    if (href->is_closed()) {
+        return mk_handle_has_been_closed_error();
+    }
+
     buffer<char> tmp;
     parray<vm_obj> const & a = to_array(cfield(b, 1));
     unsigned sz = a.size();
     for (unsigned i = 0; i < sz; i++) {
         tmp.push_back(static_cast<unsigned char>(cidx(a[i])));
     }
-    if (fwrite(tmp.data(), 1, sz, href->m_handle) != sz) {
-        clearerr(href->m_handle);
+
+    try {
+        href->write(tmp);
+        return mk_io_result(mk_vm_unit());
+    } catch (handle_exception e) {
         return mk_io_failure("write failed");
     }
-    return mk_io_result(mk_vm_unit());
 }
 
 static vm_obj fs_get_line(vm_obj const & h, vm_obj const &) {
     handle_ref const & href = to_handle(h);
-    if (has_been_closed(href)) return mk_handle_has_been_closed_error();
+
+    if (href->is_closed()) {
+        return mk_handle_has_been_closed_error();
+    }
+
     parray<vm_obj> r;
     while (true) {
-        int c = fgetc(href->m_handle);
-        if (ferror(href->m_handle)) {
-            clearerr(href->m_handle);
+        int c = fgetc(href->m_file);
+        if (ferror(href->m_file)) {
+            clearerr(href->m_file);
             return mk_io_failure("get_line failed");
         }
         if (c == EOF)
@@ -251,7 +260,6 @@ static vm_obj fs_stderr(vm_obj const &) {
 }
 
 /*
-(handle         : Type)
 (read_file      : string → bool → m io.error char_buffer)
 (mk_file_handle : string → io.mode → bool → m io.error handle)
 (is_eof         : handle → m io.error bool)
@@ -281,6 +289,71 @@ static vm_obj mk_fs() {
     return mk_vm_constructor(0, 11, fields);
 }
 
+stdio to_stdio(vm_obj const & o) {
+    switch (cidx(o)) {
+    case 0:
+        return stdio::PIPED;
+    case 1:
+        return stdio::INHERIT;
+    case 2:
+        return stdio::NUL;
+    default:
+        lean_unreachable()
+    }
+}
+
+/*
+structure process :=
+  (cmd : string)
+  /- Add an argument to pass to the process. -/
+  (args : list string)
+  /- Configuration for the process's stdin handle. -/
+  (stdin := stdio.inherit)
+  /- Configuration for the process's stdout handle. -/
+  (stdout := stdio.inherit)
+  /- Configuration for the process's stderr handle. -/
+  (stderr := stdio.inherit)
+*/
+static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) {
+    std::string cmd = to_string(cfield(process_obj, 0));
+
+    list<std::string> args = to_list<std::string>(cfield(process_obj, 1), [&] (vm_obj const & o) -> std::string {
+        return to_string(o);
+    });
+    auto stdin_stdio = to_stdio(cfield(process_obj, 2));
+    auto stdout_stdio = to_stdio(cfield(process_obj, 3));
+    auto stderr_stdio = to_stdio(cfield(process_obj, 4));
+
+    lean::process proc(cmd);
+
+    for (auto arg : args) {
+        proc.arg(arg);
+    }
+
+    proc.set_stdin(stdin_stdio);
+    proc.set_stdout(stdout_stdio);
+    proc.set_stderr(stderr_stdio);
+
+    child ch = proc.spawn();
+
+    auto child_obj = mk_vm_constructor(0, {
+        to_obj(ch.m_stdin),
+        to_obj(ch.m_stdout),
+        to_obj(ch.m_stderr)
+    });
+
+    // Should add helper functions for building real io.result
+    return mk_io_result(child_obj);
+}
+
+/*
+structure io.process (Err : Type) (handle : Type) (m : Type → Type → Type) :=
+  (spawn        : process → m Err child)
+*/
+static vm_obj mk_process() {
+    return mk_native_closure(io_process_spawn);
+}
+
 static vm_obj io_return(vm_obj const &, vm_obj const & a, vm_obj const &) {
     return mk_io_result(a);
 }
@@ -320,24 +393,29 @@ static vm_obj io_m(vm_obj const &, vm_obj const &) {
 }
 
 /*
-structure io.interface :=
+class io.interface :=
 (m        : Type → Type → Type)
 (monad    : Π e, monad (m e))
 (catch    : ∀ e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α)
 (fail     : ∀ e α, e → m e α)
+-- Primitive Types
+(handle   : Type)
+-- Interface Extensions
 (term     : io.terminal m)
-(fs       : io.file_system m)
+(fs       : io.file_system handle m)
+(process  : io.process io.error handle m)
 */
 vm_obj mk_io_interface() {
-    vm_obj fields[6] = {
+    vm_obj fields[7] = {
         mk_native_closure(io_m), /* TODO(Leo): delete after we improve code generator */
         mk_native_closure(io_monad),
         mk_native_closure(io_catch),
         mk_native_closure(io_fail),
         mk_terminal(),
-        mk_fs()
+        mk_fs(),
+        mk_process()
     };
-    return mk_vm_constructor(0, 6, fields);
+    return mk_vm_constructor(0, 7, fields);
 }
 
 optional<vm_obj> is_io_result(vm_obj const & o) {
diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h
index ca1b2e2ac6..ad58fcf22f 100644
--- a/src/library/vm/vm_io.h
+++ b/src/library/vm/vm_io.h
@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "library/vm/vm.h"
+#include "library/handle.h"
+
 namespace lean {
 vm_obj mk_io_result(vm_obj const & r);
 vm_obj mk_io_interface();
@@ -18,6 +20,11 @@ optional<vm_obj> is_io_result(vm_obj const & o);
 optional<vm_obj> is_io_error(vm_obj const & o);
 /* Convert an io.error object into a string */
 std::string io_error_to_string(vm_obj const & o);
+
+bool is_handle(vm_obj const & o);
+handle_ref const & to_handle(vm_obj const & o);
+vm_obj to_obj(handle_ref const & h);
+
 void initialize_vm_io();
 void finalize_vm_io();
 }
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index f83b2163b4..7d18008098 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -6,5 +6,4 @@ add_library(util OBJECT debug.cpp name.cpp name_set.cpp fresh_name.cpp
   utf8.cpp name_map.cpp list_fn.cpp null_ostream.cpp file_lock.cpp
   timer.cpp task.cpp task_builder.cpp cancellable.cpp
   log_tree.cpp
-  small_object_allocator.cpp subscripted_name_set.cpp process.cpp
-  parser_exception.cpp)
+  small_object_allocator.cpp subscripted_name_set.cpp parser_exception.cpp)
diff --git a/src/util/process.cpp b/src/util/process.cpp
deleted file mode 100644
index ccf575da30..0000000000
--- a/src/util/process.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Jared Roesch
-*/
-#include <string>
-#include <fstream>
-#include <iostream>
-#include <iomanip>
-#include <utility>
-#include <unistd.h>
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
-//
-#else
-#include <sys/wait.h>
-#endif
-#include "util/process.h"
-#include "util/buffer.h"
-
-namespace lean {
-// TODO(jroesch): make this cross platform
-process::process(std::string n): m_proc_name(n), m_args() {
-    m_args.push_back(m_proc_name);
-}
-
-process & process::arg(std::string a) {
-    m_args.push_back(a);
-    return *this;
-}
-
-#if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
-void process::run() {
-    throw exception("process::run not supported on Windows");
-}
-#else
-
-void process::run() {
-    int pid = fork();
-    if (pid == 0) {
-        buffer<char*> pargs;
-
-        for (auto arg : m_args) {
-            auto str = new char[arg.size() + 1];
-            arg.copy(str, arg.size());
-            str[arg.size()] = '\0';
-            pargs.push_back(str);
-        }
-
-        pargs.data()[pargs.size()] = NULL;
-
-        auto err = execvp(pargs.data()[0], pargs.data());
-        if (err < 0) {
-            throw std::runtime_error("executing process failed: ...");
-        }
-    } else if (pid == -1) {
-        throw std::runtime_error("forking process failed: ...");
-    } else {
-        int status;
-        waitpid(pid, &status, 0);
-    }
-}
-#endif
-
-}
diff --git a/src/util/process.h b/src/util/process.h
deleted file mode 100644
index 5fe329c18e..0000000000
--- a/src/util/process.h
+++ /dev/null
@@ -1,23 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Jared Roesch
-*/
-#pragma once
-
-#include <iostream>
-#include <string>
-#include "util/buffer.h"
-
-namespace lean  {
-
-class process {
-    std::string m_proc_name;
-    buffer<std::string> m_args;
-public:
-    process(std::string exe_name);
-    process & arg(std::string arg_str);
-    void run();
-};
-}
diff --git a/tests/lean/run/io_process_echo.lean b/tests/lean/run/io_process_echo.lean
new file mode 100644
index 0000000000..5aa496957e
--- /dev/null
+++ b/tests/lean/run/io_process_echo.lean
@@ -0,0 +1,13 @@
+import system.io
+import system.process
+
+open process
+
+variable [io.interface]
+
+def main : io unit := do
+  out ← io.cmd "echo" ["Hello World!"],
+  io.put_str out,
+  return ()
+
+#eval main
diff --git a/tests/lean/run/io_process_echo.lean.expected.out b/tests/lean/run/io_process_echo.lean.expected.out
new file mode 100644
index 0000000000..ea2fd5c3fa
--- /dev/null
+++ b/tests/lean/run/io_process_echo.lean.expected.out
@@ -0,0 +1,2 @@
+Hello World!
+