+++ /dev/null
-<?xml version="1.0"?>
-
-<!DOCTYPE site SYSTEM "site.dtd">
-
-<site>
- <name>Katholieke Universiteit Nijmegen</name>
- <country>The Netherlands</country>
- <url>http://www.cs.kun.nl</url>
- <address>Subfaculteit Informatica,
- Faculteit Natuurwetenschappen, Wiskunde en Informatica,
- Katholieke Universiteit Nijmegen,
- Toernooiveld 1, 6525 ED Nijmegen, The Netherlands</address>
- <responsible file="nijmegen/geuvers"/>
- <description>
- <p>The Sub-faculty of Computer Science at the University of Nijmegen hosts
- a broad experience in logic, formal methods and theorem proving. The
- Faculty of Mathematics and Computer Science of Eindhoven University of
- Technology is strong in computer algebra, theorem proving and applying
- Web technology to mathematics. Nijmegen and Eindhoven have a long
- history in cooperation on topics related to this FET proposal, notably
- type theory, theorem proving and combining various computer
- mathematics applications, especially using OpenMath. This cooperation
- was mainly taking place between the research groups of Geuvers and
- Barendregt in Nijmegen and the research group of Cohen in Eindhoven.</p>
- <p>The research group of Geuvers and Barendregt is part of the EC
- sponsored Thematic Network ``TYPES'' (IST-1999-29001) and of its
- ancestor, the EC Working Group ``Types for Proofs and Programs'',
- which testifies there interest in theorem proving, especially using
- type theory based theorem provers. The FTA project (Fundamental
- Theorem of Algebra), started in 1999 and to be finished in 2001, has
- as its main goal to formalize (in Coq) a large body of undergraduate
- mathematics (algebra and analysis), culminating in a proof of the
- fundamental theorem of algebra. The formalization of the mathematics
- is now finished and the next step is to make the formalization
- accessible and usable by others, preferably through the World Wide
- Web.</p>
- <p>The research group in Nijmegen and the research group of Cohen in
- Eindhoven are both part of the EC Working Group Calculemus, which aims
- at bridging the gap between different mathematical computer
- applications, like computer algebra systems and theorem provers. One
- of the vehicles for doing so is the definition of OpenMath as an
- intermediate language for the exchange of mathematical objects among
- computer applications.
- The research group of Cohen is part of the
- IST Thematic Network ``OpenMath'' (IST-2000-28719) and its ancestor,
- the OpenMath Esprit project (see <a target="_top" href="http://www.openmath.org/">http://www.openmath.org/</a>).</p>
- </description>
- <member file="nijmegen/geuvers"/>
- <member file="nijmegen/cohen"/>
- <member file="nijmegen/barendregt"/>
- <member file="nijmegen/wiedijk"/>
- <member file="nijmegen/barreiro"/>
- <member file="nijmegen/cruz-filipe"/>
- <member file="nijmegen/niqui"/>
- <member file="nijmegen/stein"/>
- <member file="nijmegen/synek"/>
-
-</site>