Overview of systems

I'm working in the group of Henk Barendregt, where we apply
type theory to formalizing pure mathematics (we are currently
working on a proof of the fundamental theorem of algebra in

When I was introduced to type theory I found the number of
systems (Coq, Lego, Alf, Agda, Typelab, Yarrow, Nuprl, HOL,
Twelf, Isabelle, PVS, etc.) bewildering.  So, to get some
grip on what's out there, I compiled a list of "math in the
computer" systems.  I put it on the web as:


Because I decided that non type theoretical but related
systems are interesting too, I didn't restrict this list to
one category of computer math.  It contains all kinds of

  - proof assistants
  - theorem provers
  - computer algebra systems
  - "mathematical" specification environments for software
  - math typesetting systems

I included something if:

  (a) it's related to mathematics
  (b) it's related to computers
  (c) it's active (has a web page)

Anything that satisfies these three requirements I put in the

I hope this list is useful to other people from the Types
community too.  Also, I'd very much appreciate it if people
from this mailing list would give me feedback so I can
improve it.

Freek Wiedijk