3 <!DOCTYPE site SYSTEM "site.dtd">
6 <name>Katholieke Universiteit Nijmegen</name>
7 <country>The Netherlands</country>
8 <url>http://www.cs.kun.nl</url>
9 <address>Subfaculteit Informatica,
10 Faculteit Natuurwetenschappen, Wiskunde en Informatica,
11 Katholieke Universiteit Nijmegen,
12 Toernooiveld 1, 6525 ED Nijmegen, The Netherlands</address>
13 <responsible file="nijmegen/geuvers"/>
15 <p>The Sub-faculty of Computer Science at the University of Nijmegen hosts
16 a broad experience in logic, formal methods and theorem proving. The
17 Faculty of Mathematics and Computer Science of Eindhoven University of
18 Technology is strong in computer algebra, theorem proving and applying
19 Web technology to mathematics. Nijmegen and Eindhoven have a long
20 history in cooperation on topics related to this FET proposal, notably
21 type theory, theorem proving and combining various computer
22 mathematics applications, especially using OpenMath. This cooperation
23 was mainly taking place between the research groups of Geuvers and
24 Barendregt in Nijmegen and the research group of Cohen in Eindhoven.</p>
25 <p>The research group of Geuvers and Barendregt is part of the EC
26 sponsored Thematic Network ``TYPES'' (IST-1999-29001) and of its
27 ancestor, the EC Working Group ``Types for Proofs and Programs'',
28 which testifies there interest in theorem proving, especially using
29 type theory based theorem provers. The FTA project (Fundamental
30 Theorem of Algebra), started in 1999 and to be finished in 2001, has
31 as its main goal to formalize (in Coq) a large body of undergraduate
32 mathematics (algebra and analysis), culminating in a proof of the
33 fundamental theorem of algebra. The formalization of the mathematics
34 is now finished and the next step is to make the formalization
35 accessible and usable by others, preferably through the World Wide
37 <p>The research group in Nijmegen and the research group of Cohen in
38 Eindhoven are both part of the EC Working Group Calculemus, which aims
39 at bridging the gap between different mathematical computer
40 applications, like computer algebra systems and theorem provers. One
41 of the vehicles for doing so is the definition of OpenMath as an
42 intermediate language for the exchange of mathematical objects among
43 computer applications.
44 The research group of Cohen is part of the
45 IST Thematic Network ``OpenMath'' (IST-2000-28719) and its ancestor,
46 the OpenMath Esprit project (see <a target="_top" href="http://www.openmath.org/">http://www.openmath.org/</a>).</p>
48 <member file="nijmegen/geuvers"/>
49 <member file="nijmegen/cohen"/>
50 <member file="nijmegen/barendregt"/>
51 <member file="nijmegen/wiedijk"/>
52 <member file="nijmegen/barreiro"/>
53 <member file="nijmegen/cruz-filipe"/>
54 <member file="nijmegen/niqui"/>
55 <member file="nijmegen/stein"/>
56 <member file="nijmegen/synek"/>