guru-lang


Implementation of the Guru verified programming language.

Source code for the Guru programming language is here.

While this project is mature at this point (Summer 2012: we do not have plans to do much further development on Guru, due to other research projects), we will respond to requests for help or more information about it. A number of people have found Guru a pretty good vehicle for learning about dependent types. There is a book, which I wrote for a class at U. Iowa:

http://guru-lang.googlecode.com/svn/branches/1.0/doc/book.pdf

It does not presuppose knowledge of functional programming, dependent types, or theorem proving.

You can check out the source code this way:

svn checkout http://guru-lang.googlecode.com/svn/branches/1.0/ guru-lang

I recommend using the 1.0 version, since we have fixed some bugs since 1.0a. If you just want to work through the book, though, version 1.0a is a snapshot known to work for the material in the book, so that is also an option:

svn checkout http://guru-lang.googlecode.com/svn/branches/1.0a/ guru-lang

If you have questions, feel free to email the Guru Gang mailing list: guru-gang@googlegroups.com.

Support for this project is partially provided by the U.S. National Science Foundation.

Aaron Stump

Project Information

Labels:
compiler proofchecker programminglanguage typetheory verifiedprogramming verification