diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,3 @@
+# Changelog for refinery
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2018, Reed Mullanix
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+* Redistributions of source code must retain the above copyright notice, this
+  list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright notice,
+  this list of conditions and the following disclaimer in the documentation
+  and/or other materials provided with the distribution.
+
+* Neither the name of the copyright holder nor the names of its
+  contributors may be used to endorse or promote products derived from
+  this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,8 @@
+# refinery
+
+`refinery` is a toolkit for building proof refinement/proof automation systems, based roughly on the [
+Algebraic Foundations of Proof Refinement](https://arxiv.org/abs/1703.05215).
+
+## Overview
+The main datatype of the library is `TacticT goal extract m a`, which is a monad transformer that behaves as a tactic.
+When creating your domain-specific tactics, you should use `RuleT` and `rule` to implement them.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/refinery.cabal b/refinery.cabal
new file mode 100644
--- /dev/null
+++ b/refinery.cabal
@@ -0,0 +1,66 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.1.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: f61ff60d97eac2723f257e2cb25ede1205a5cb260049a1708c66c7ab0d4669f8
+
+name:           refinery
+version:        0.1.0.0
+synopsis:       Toolkit for building proof automation systems
+description:    Please see the README on GitHub at <https://github.com/githubuser/refinery#readme>
+category:       Language
+homepage:       https://github.com/totbwf/refinery#readme
+bug-reports:    https://github.com/totbwf/refinery/issues
+author:         Reed Mullanix
+maintainer:     reedmullanix@gmail.com
+copyright:      2019 Reed Mullanix
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/totbwf/refinery
+
+library
+  exposed-modules:
+      Refinery.ProofState
+      Refinery.Tactic
+      Refinery.Tactic.Internal
+  other-modules:
+      Paths_refinery
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , containers >=0.5
+    , exceptions >=0.10
+    , mmorph >=1
+    , mtl >=2
+    , pipes >=4
+    , semigroupoids >=5
+  default-language: Haskell2010
+
+test-suite refinery-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_refinery
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , containers >=0.5
+    , exceptions >=0.10
+    , mmorph >=1
+    , mtl >=2
+    , pipes >=4
+    , refinery
+    , semigroupoids >=5
+  default-language: Haskell2010
diff --git a/src/Refinery/ProofState.hs b/src/Refinery/ProofState.hs
new file mode 100644
--- /dev/null
+++ b/src/Refinery/ProofState.hs
@@ -0,0 +1,72 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Refinery.ProofState
+-- Copyright   :  (c) Reed Mullanix 2019
+-- License     :  BSD-style
+-- Maintainer  :  reedmullanix@gmail.com
+--
+--
+module Refinery.ProofState
+  ( ProofStateT(..)
+  , axiom
+  , mapExtract
+  )
+where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Trans
+import Control.Monad.Catch
+import Control.Monad.Except
+import Control.Monad.Reader.Class
+import Control.Monad.State.Class
+import Control.Monad.IO.Class
+
+import Pipes.Core
+
+newtype ProofStateT ext m jdg = ProofStateT { unProofStateT :: Client jdg ext m ext }
+
+instance (Monad m) => Functor (ProofStateT ext m) where
+  fmap f (ProofStateT p) = ProofStateT $ (request . f) >\\ p
+
+instance (Monad m) => Applicative (ProofStateT ext m) where
+  pure a = ProofStateT $ request a
+  (ProofStateT pf) <*> (ProofStateT pa) = ProofStateT $ (\f -> (request . f) >\\ pa) >\\ pf
+
+instance (Monad m) => Monad (ProofStateT ext m) where
+  return = pure
+  (ProofStateT p) >>= k = ProofStateT $ (unProofStateT . k) >\\ p
+
+instance MonadTrans (ProofStateT ext) where
+  lift m = ProofStateT $ request =<< (lift m)
+
+instance (MonadIO m) => MonadIO (ProofStateT ext m) where
+  liftIO m = ProofStateT $ request =<< (liftIO m)
+
+instance (MonadError err m) => MonadError err (ProofStateT ext m) where
+  throwError e = ProofStateT $ lift $ throwError e
+  catchError (ProofStateT m) h = ProofStateT $ catchError m (unProofStateT . h)
+
+instance (MonadThrow m) => MonadThrow (ProofStateT ext m) where
+  throwM e = ProofStateT $ lift $ throwM e
+
+instance (MonadCatch m) => MonadCatch (ProofStateT ext m) where
+  catch (ProofStateT m) h = ProofStateT $ catch m (unProofStateT . h)
+
+instance (MonadReader env m) => MonadReader env (ProofStateT ext m) where
+  ask = lift ask
+  local f (ProofStateT m) = ProofStateT $ local f m
+
+instance (MonadState s m) => MonadState s (ProofStateT ext m) where
+  get = lift get
+  put = lift . put
+
+axiom :: (Monad m) => ext -> ProofStateT ext m jdg
+axiom e = ProofStateT $ return e
+
+mapExtract :: (Monad m) => (ext -> ext') -> (ext' -> ext) -> ProofStateT ext m jdg -> ProofStateT ext' m jdg
+mapExtract into out p = ProofStateT $ fmap into ((\j ->  fmap out $ request j) >\\ (unProofStateT p))
diff --git a/src/Refinery/Tactic.hs b/src/Refinery/Tactic.hs
new file mode 100644
--- /dev/null
+++ b/src/Refinery/Tactic.hs
@@ -0,0 +1,146 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Refinery.Tactic
+-- Copyright   :  (c) Reed Mullanix 2019
+-- License     :  BSD-style
+-- Maintainer  :  reedmullanix@gmail.com
+module Refinery.Tactic
+  ( TacticT
+  , runTacticT
+  -- * Tactic Combinators
+  , (<@>)
+  , try
+  , many_
+  , choice
+  , progress
+  -- * Subgoal Manipulation
+  , goal
+  , focus
+  , forSubgoals
+  -- * Tactic Creation
+  , MonadExtract(..)
+  , MonadRule(..)
+  , RuleT
+  , rule
+  , MonadProvable(..)
+  , ProvableT(..)
+  , Provable
+  , runProvable
+  -- * Re-Exports
+  , Alt(..)
+  ) where
+
+import Data.Functor.Alt
+import Control.Applicative
+import Control.Monad.Except
+import Control.Monad.Reader
+import Control.Monad.State.Strict
+import Control.Monad.Trans
+import Control.Monad.IO.Class
+import Control.Monad.Morph
+
+import Data.Bifunctor
+
+import Pipes.Core
+import Pipes.Lift (runStateP)
+
+import Refinery.ProofState
+import Refinery.Tactic.Internal
+
+-- | Create a tactic that applies each of the tactics in the list to one subgoal.
+--
+-- When the number of subgoals is greater than the number of provided tactics,
+-- the identity tactic is applied to the remainder. When the number of subgoals is
+-- less than the number of provided tactics, the remaining tactics are ignored.
+(<@>) :: (MonadProvable jdg m) => TacticT jdg ext m () -> [TacticT jdg ext m ()] -> TacticT jdg ext m ()
+t <@> ts = stateful t applyTac (ts ++ repeat (pure ()))
+  where
+    applyTac j = do
+      tac <- gets head
+      modify tail
+      hoist lift $ asRule j tac
+
+-- | Tries to run a tactic, backtracking on failure
+try :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()
+try t = t <!> pure ()
+
+-- | Runs a tactic repeatedly until it fails
+many_ :: (MonadProvable jdg m, MonadError err m) => TacticT jdg ext m () -> TacticT jdg ext m ()
+many_ t = try (t >> many_ t)
+
+-- | Get the current goal
+goal :: (Monad m) => TacticT jdg ext m jdg
+goal = TacticT $ get
+
+
+-- | @choice err ts@ tries to apply a series of tactics @ts@, and commits to the
+-- 1st tactic that succeeds. If they all fail, then @err@ is thrown
+choice :: (MonadProvable jdg m, MonadError err m) => err -> [TacticT jdg ext m a] -> TacticT jdg ext m a
+choice err [] = throwError err
+choice err (t:ts) = t <!> choice err ts
+
+-- | @progress eq err t@ applies the tactic @t@, and checks to see if the
+-- resulting subgoals are all equal to the initial goal by using @eq@. If they
+-- are, it throws @err@.
+progress :: (MonadProvable jdg m, MonadError err m) => (jdg -> jdg -> Bool) -> err ->  TacticT jdg ext m a -> TacticT jdg ext m a
+progress eq err t = do
+  j <- goal
+  a <- t
+  j' <- goal
+  if j `eq` j' then pure a else throwError err
+
+-- | Apply the first tactic, and then apply the second tactic focused on the @n@th subgoal.
+focus :: (MonadProvable jdg m, Monad m) => TacticT jdg ext m () -> Int -> TacticT jdg ext m () -> TacticT jdg ext m ()
+focus t ix t' = stateful t applyTac 0
+  where
+    applyTac j = do
+      n <- get
+      put (n + 1)
+      hoist lift $ asRule j (if n == ix then t' else pure ())
+
+-- | Applies @f@ to every subgoals resulting from the tactic @t@.
+forSubgoals :: (Monad m) => TacticT jdg ext m a -> (jdg -> m b) -> TacticT jdg ext m a
+forSubgoals t f = TacticT $ StateT $ \j -> ProofStateT $
+   action >\\ (unProofStateT $ runStateT (unTacticT t) j)
+  where
+    action (a, j) = do
+      lift $ f j
+      request (a, j)
+
+-- | Runs a tactic, producing the extract, along with a list of unsolved subgoals.
+runTacticT :: (MonadExtract ext m) => TacticT jdg ext m () -> jdg -> m (ext, [jdg])
+runTacticT (TacticT t) j =
+  fmap (second reverse) $ flip runStateT [] $ runEffect $ server +>> (hoist lift $ unProofStateT $ execStateT t j)
+  where
+    server :: (MonadExtract ext m) => jdg -> Server jdg ext (StateT [jdg] m) ext
+    server j = do
+      modify (j:)
+      h <- hole
+      respond h >>= server
+
+class (Monad m) => MonadExtract ext m | m -> ext where
+  -- | Generates a "hole" of type @ext@, which should represent
+  -- an incomplete extract.
+  hole :: m ext
+  default hole :: (MonadTrans t, MonadExtract ext m1, m ~ t m1) => m ext
+  hole = lift hole
+
+instance (MonadExtract ext m) => MonadExtract ext (Proxy a' a b' b m)
+instance (MonadExtract ext m) => MonadExtract ext (StateT s m)
+instance (MonadExtract ext m) => MonadExtract ext (ReaderT env m)
+instance (MonadExtract ext m) => MonadExtract ext (ExceptT err m)
+instance (MonadExtract ext m) => MonadExtract ext (RuleT jdg ext m)
+
+
+-- | Turn an inference rule into a tactic.
+rule :: (Monad m) => (jdg -> RuleT jdg ext m ext) -> TacticT jdg ext m ()
+rule r = TacticT $ StateT $ \j -> ProofStateT $ (\j' -> request ((), j')) >\\ unRuleT (r j)
diff --git a/src/Refinery/Tactic/Internal.hs b/src/Refinery/Tactic/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Refinery/Tactic/Internal.hs
@@ -0,0 +1,164 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Refinery.Tactic.Internal
+-- Copyright   :  (c) Reed Mullanix 2019
+-- License     :  BSD-style
+-- Maintainer  :  reedmullanix@gmail.com
+--
+--
+-- = WARNING
+-- This module is considered __internal__, and can
+-- change at any given time.
+module Refinery.Tactic.Internal
+  ( TacticT(..)
+  , mapTacticT
+  , stateful
+  , asRule
+  , MonadRule(..)
+  , RuleT(..)
+  , mapRuleT
+  , MonadProvable(..)
+  , ProvableT(..)
+  , Provable
+  , runProvable
+  )
+where
+
+import Data.Functor.Alt
+import Control.Applicative
+import Control.Monad.Identity
+import Control.Monad.Except
+import Control.Monad.Catch
+import Control.Monad.Reader
+import Control.Monad.State.Strict
+import Control.Monad.Trans
+import Control.Monad.IO.Class
+import Control.Monad.Morph
+
+import Data.Bifunctor
+
+import Pipes.Core
+import Pipes.Lift (evalStateP, runStateP)
+
+import Refinery.ProofState
+
+-- | A @'TacticT'@ is a monad transformer that performs proof refinement.
+-- The type variables signifiy:
+--
+-- * @jdg@ - The goal type. This is the thing we are trying to construct a proof of.
+-- * @ext@ - The extract type. This is what we will recieve after running the tactic.
+-- * @m@ - The base monad.
+-- * @a@ - The return value. This to make @'TacticT'@ a monad, and will always be @'()'@
+newtype TacticT jdg ext m a = TacticT { unTacticT :: StateT jdg (ProofStateT ext m) a }
+  deriving ( Functor
+           , MonadReader env
+           , MonadError err
+           , MonadIO
+           , MonadThrow
+           , MonadCatch
+           )
+
+instance (MonadProvable jdg m) => Applicative (TacticT jdg ext m) where
+  pure a = TacticT $ StateT $ proving >=> \j -> pure (a, j)
+  (<*>) = ap
+
+instance (MonadProvable jdg m) => Monad (TacticT jdg ext m) where
+  return = pure
+  t >>= k = TacticT $ StateT $ proving >=> \j -> do
+    (a, j') <- runStateT (unTacticT t) j
+    runStateT (unTacticT $ k a) =<< proving j'
+
+-- | Map the unwrapped computation using the given function
+mapTacticT :: (Monad m) => (m a -> m b) -> TacticT jdg ext m a -> TacticT jdg ext m b
+mapTacticT f (TacticT m) = TacticT $ m >>= (lift . lift . f . return)
+
+instance (MonadError err m) => Alt (TacticT jdg ext m) where
+  (TacticT t1) <!> (TacticT t2) = TacticT $ t1 `catchError` (const t2)
+
+instance MonadTrans (TacticT jdg ext) where
+  lift m = TacticT $ lift $ lift m
+
+instance (MonadProvable jdg m, MonadState s m) => MonadState s (TacticT jdg ext m) where
+  get = lift get
+  put = lift . put
+
+-- | Helper function for making "stateful" tactics like "<@>"
+stateful :: (Monad m) => TacticT jdg ext m a -> (jdg -> RuleT jdg ext (StateT s m) ext) -> s -> TacticT jdg ext m a
+stateful (TacticT t) f s = TacticT $ StateT $ \j -> ProofStateT $
+  evalStateP s $ action >\\ (hoist lift $ unProofStateT $ runStateT t j)
+  where
+    action (a, j) = (\j' -> request (a, j')) >\\ (unRuleT $ f j)
+
+-- | Transforms a tactic into a rule. Useful for doing things with @'stateful'@.
+asRule :: (Monad m) => jdg -> TacticT jdg ext m a -> RuleT jdg ext m ext
+asRule j t = RuleT $ unProofStateT $ execStateT (unTacticT t) j
+
+-- | A @'RuleT'@ is a monad transformer for creating inference rules.
+newtype RuleT jdg ext m a = RuleT { unRuleT :: Client jdg ext m a }
+  deriving ( Functor
+           , Applicative
+           , Monad
+           , MonadReader env
+           , MonadState s
+           , MonadError err
+           , MonadIO
+           , MonadThrow
+           , MonadCatch
+           , MonadTrans
+           , MFunctor
+           )
+
+
+-- | Map the unwrapped computation using the given function
+mapRuleT :: (Monad m) => (m a -> m b) -> RuleT jdg ext m a -> RuleT jdg ext m b
+mapRuleT f (RuleT m) = RuleT $ m >>= (lift . f . return)
+
+class (Monad m) => MonadRule jdg ext m | m -> jdg, m -> ext where
+  -- | Create a subgoal, and return the resulting extract.
+  subgoal :: jdg -> m ext
+  default subgoal :: (MonadTrans t, MonadRule jdg ext m1, m ~ t m1) => jdg -> m ext
+  subgoal = lift . subgoal
+
+instance (Monad m) => MonadRule jdg ext (RuleT jdg ext m) where
+  subgoal j = RuleT $ request j
+
+instance (MonadRule jdg ext m) => MonadRule jdg ext (ReaderT env m)
+instance (MonadRule jdg ext m) => MonadRule jdg ext (StateT env m)
+instance (MonadRule jdg ext m) => MonadRule jdg ext (ExceptT env m)
+instance (MonadRule jdg ext m) => MonadRule jdg ext (ProvableT env m)
+
+class (Monad m) => MonadProvable jdg m | m -> jdg where
+  -- | Applies a transformation of goals at every step of the tactic.
+  proving :: jdg -> m jdg
+  default proving :: (MonadTrans t, MonadProvable jdg m1, m ~ t m1) => jdg -> m jdg
+  proving = lift . proving
+
+instance (MonadProvable jdg m) => MonadProvable jdg (ProofStateT ext m)
+instance (MonadProvable jdg m) => MonadProvable jdg (ReaderT r m)
+instance (MonadProvable jdg m) => MonadProvable jdg (StateT s m)
+instance (MonadProvable jdg m) => MonadProvable jdg (ExceptT err m)
+instance (Monad m) => MonadProvable jdg (ProvableT jdg m) where
+  proving = pure
+
+-- | Helper newtype for when you don't have any need for the mechanisms of MonadProvable.
+newtype ProvableT jdg m a = ProvableT { runProvableT :: m a }
+  deriving (Functor, Applicative, Monad, MonadIO, MonadState s, MonadError err)
+
+type Provable jdg a = ProvableT jdg Identity a
+
+instance MonadTrans (ProvableT jdg) where
+  lift = ProvableT
+
+runProvable :: Provable jdg a -> a
+runProvable = runIdentity . runProvableT
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,2 @@
+main :: IO ()
+main = putStrLn "Test suite not yet implemented"