**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

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 on building Coq from SVN under Mac OS X

TAGS support for coq (this doesn't work nicely, `coqtags`

needs to be updated)