*Last updated: 2015-10-09 01:57:35 +0100*

Upstream URL: `git clone http://chriswarbo.net/git/powerplay.git`

Contents of follows

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