This is an implementation of Jürgen Schmidhuber's PowerPlay[1] architecture for
'Universal Artificial Intelligence', implemented in the dependently-typed
language Coq[2]. Using a system like Coq gives us two things:

 * The PowerPlay implementation is formally verified
 * We can build PowerPlay's proof machinery on top of Coq's

The repository is layed out as follows:

  * build.hs       Haskell script to build *.v files in order of dependencies

  * Expr.v         Initial attempt at defining a reflective Coq-in-Coq
                   implementation (not finished yet)

  * Simple.v       A simple, standalone PowerPlay specification
  * SimpleTests.v  Unit tests and theorems about Simple.v

  * SK.v           A Coq implementation of SK combinatory logic
  * SKTests.v      Unit tests and theorems about SK.v
  * SKUtil.v       Utility functions, theorems and proof tactics for SK.v

  * Sqrt.v         Straightforward implementation of the Simple.v specification
                   for finding square roots in lookup tables

  * Util.v         Generic utility functions and theorems

[1] http://www.idsia.ch/~juergen/interest.html
[2] http://coq.inria.fr