diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal
index 1e74be8..9ba936b 100644
--- a/NominalAngluin.cabal
+++ b/NominalAngluin.cabal
@@ -1,30 +1,32 @@
--- Initial NominalAngluin.cabal generated by cabal init.  For further 
--- documentation, see http://haskell.org/cabal/users-guide/
-
 name:                NominalAngluin
 version:             0.1.0.0
--- synopsis:            
--- description:         
--- license:             
-license-file:        LICENSE
-author:              Anonymous
--- maintainer:          
--- copyright:           
--- category:            
+license:             UnspecifiedLicense
+author:              Joshua Moerman
+copyright:           (c) 2016, Joshua Moerman
 build-type:          Simple
--- extra-source-files:  
 cabal-version:       >=1.10
 
 executable NominalAngluin
   main-is:             Main.hs
-  -- other-modules:       
-  -- other-extensions:    
+  other-modules:
+    AbstractLStar,
+    Angluin,
+    Bollig,
+    Examples,
+    Examples.Contrived,
+    Examples.ContrivedNFAs,
+    Examples.Fifo,
+    Examples.RunningExample,
+    Examples.Stack,
+    NLStar,
+    ObservationTable,
+    Teacher
   build-depends:
-    base >=4.8 && <4.9,
+    base >= 4.8 && < 5,
     containers,
     deepseq,
     haskeline,
     mtl,
-    NLambda
+    NLambda >= 1.1
   hs-source-dirs:      src
   default-language:    Haskell2010
diff --git a/README.md b/README.md
new file mode 100644
index 0000000..31886ec
--- /dev/null
+++ b/README.md
@@ -0,0 +1,90 @@
+Learning Nominal Automata
+=========================
+
+*NOTE*: Please download the archive `popl-artifact.zip`. This contains the
+same source code, but is bundled with the NLambda library (the specific version
+used for the paper). The remainder of this README assumes you are using that
+archive.
+
+We have bundled the implementation of the learning algorithm and the
+implementation of the NLambda library in this artifact. Note that our
+version of NLambda is slightly different from the one on the [NLambda
+website](http://www.mimuw.edu.pl/~szynwelski/nlambda/). Some bugs were
+fixed in our version and possibly some new features have appeared.
+
+This artifact was tested on a Debian system. During development both Mac and
+Windows have been used, so it should work on these operating systems too. Note
+that you will need the Z3 solver (as executable). The algorithms are
+implemented in Haskell and you will need a recent GHC (at least 7.10).
+
+
+# Building
+
+Should be just as easy as `stack build`, assuming one has installed Haskell
+stack. I noticed that the linker needed libtinfo. So you might need to install
+the libtinfo package, for example through apt. (I do not know which haskell
+package depends on this.) Building may take a while.
+
+Stack for haskell can be installed as described on
+[their website](http://haskellstack.org/).
+
+You will need to install the [Z3](https://github.com/Z3Prover/z3) theorem
+prover. The executable should be locatable through the PATH environment.
+Follow the build guide on their website.
+
+
+# Running
+
+Stack will produce a binary in the `.stack-works` directory, which can
+be invoked directly. Alternatively one can run `stack exec NominalAngluin`.
+The executable expects three arguments:
+
+```
+stack exec NominalAngluin -- <Learner> <Oracle> <Example>
+```
+
+There are three learners:
+- `NomLStar` is the nominal L* algorithm as described in the paper.
+- `NomLStarCol` is the nominal L* algorithm where counter examples are added
+  as columns (instead of rows). This is often a bit faster.
+- `NomNLStar` learns nominal NFAs.
+
+There are two oracles:
+- `EqDFA` is an equivalence oracle which returns shortest counter examples by
+  trying to prove two DFAs bisimilar. This method does *not* work for
+  `NomNLStar`.
+- `EqNFA n` is a bounded equivalence oracle for NFAs. Deciding equivalence
+  between NFAs is undecidable, so one has to fix a bound `n` for termination.
+
+There is an additional oracle which poses the queries to stdout, so that a
+human can answer them. Since this oracle is a bit buggy (and not described
+in the paper), it is not part of main.
+
+There is a bunch of examples (also described in the paper, except for the
+stack data structure):
+- `Fifo n` is a FIFO queue of capacity `n`.
+- `Stack n` is a Stack data structure of capacity `n`.
+- `Running n` is the running example from the paper with parameter `n`.
+- `NFA1` accepts the language uavaw, where u,v,w are any words and a any atom.
+- `Bollig n` is the language where the `n`-last symbol equals the first. This
+  can be encoded efficiently with an NFA. The corresponding DFA is exponential
+  in `n`.
+
+For example:
+```
+stack exec NominalAngluin -- NomLStar EqDFA "Fifo 2"
+```
+
+The program will output all the intermediate hypotheses. And will terminate
+once the oracle cannot find any counter examples. Printing the automaton is
+done with the NLambda library, it is not the most human-friendly output.
+
+You can define your own automaton in Haskell by using NLambda. Then it can be
+learnt, and the minimal automaton will be printed.
+
+In our paper we ran the algorithm on the examples `Fifo`, `Running`, `Bollig`
+and `NFA1` with the bounds as mentioned in the paper. The first two families
+are given by DFAs and we used all three learners with the `EqDFA` teacher.
+For the latter two we used the `EqNFA` teacher with a bound of at most 10.
+We proved by hand that the learnt model did indeed accept the language.
+
diff --git a/popl-artifact.zip b/popl-artifact.zip
new file mode 100644
index 0000000..38c4384
Binary files /dev/null and b/popl-artifact.zip differ