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
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
Search math-classes/corn docs
(google custom search)
(the Coq mailing list)
I have a background in programming, arts, AI and mathematics. I'm interested in
(homotopy) type theory,
computational complexity, algorithmic art and many
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)