Warbo/powerplay
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Folders and files
Name | Name | Last commit message | Last commit date | |
---|---|---|---|---|
Repository files navigation
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
Releases
No releases published
Packages 0
No packages published