Hello, I am a researcher working for Bas Spitters.

We are working on the ForMath project, a library of formalized mathematics concerning algebra, linear algebra, real number computation and algebraic topology.

Here is a nice video lecture about the project by Bas Spitters and Russel O'Connor: lecture.

Further work on math classes and the real number computation is done by Robbert Krebbers and Eelis van der Weegen.

Radboud Category Theory Seminar

Documentation for math-classes
Documentation for corn | Dependency Graph

Search math-classes/corn docs (google custom search)
coq-club (the Coq mailing list)

About me

I have a background in programming, arts, AI and mathematics. I'm interested in (homotopy) type theory, computational complexity, algorithmic art and many other things.

Sometimes I build silly things like this waveplotter or this reconfigurable boolean feedback network.
I like topology, check out Marius Crainic' page for (IMHO) nice lecture notes.

You can find some of my code here: github

Notes

Notes on building Coq from SVN under Mac OS X
TAGS support for coq (this doesn't work nicely, coqtags needs to be updated)