[Prev][Next][Index][Thread]
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
Coq.)
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:
<http://www.cs.kun.nl/~freek/digimath/>
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
systems:
- 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
list.
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