Latest update: 18 January 2005

ConCoq is my internal code-name for my Master's thesis, whose subject was formalising Surreal Numbers in Coq. It was intended mainly as a torture-test for Coq.

I did my Master's at the Technische Universiteit Eindhoven.The idea of the subject comes from Freek Wiedijk, from the Catholic University of Nijmegen. My supervisors were Rob Nederpelt, Roel Bloo and Francien Dechesne.

There is a mailing list for discussions around this.

You can download a copy of my report as GZip-compresses PostScript or BZip2-compressed PostScript.

While employed by the Radboud University Nijmegen (formerly Catholic University of Nijmegen), I updated the work to:

That's the first version that I dare show publicly; get it as a single .v file or a (bzip2-compressed) tarball. It needs Coq version “successor of 8.0” (or, in the meantime, a CVS checkout - the version as of 18 January works).

A paper about it is being written.