-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
44 lines (40 loc) · 1.64 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
<html>
<head>
<title>C-CoRN</title>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style>
.box {
border: 2px solid gray;
background: #ee8;
padding: 7px;
margin: 2em;
border-radius: 8px;
}
</style>
</head>
<body bgcolor="#FFFFFF" text="#000000">
<h1 align="center">Coq Repository at Nijmegen</h1>
<p>
The CoRN library has very roughly been developed in the following stages, chronologically:
<ul>
<li>Fundamental Theorem of Algebra and the algebraic hierarchy. (Geuvers, Pollack, Wiedijk and Zwanenburg)</li>
<li>Fundamental Theorem of Calculus, closely following the Bishop-Bridges book on Constructive Analysis. (PhD: Cruz-Filipe, advisor: Geuvers)</li>
<li>Program extraction for real computation (Cruz-Filipe, Letouzey, Spitters)</li>
<li>Abstract model of the real numbers (PhD: Niqui, advisor: Geuvers)</li>
<li>Efficient computation with real numbers and metric spaces (PhD: O'Connor, advisor: Spitters) </li>
<li>Riemann integration (O'Connor, Spitters)</li>
<li>Interface with Coq's standard library reals (Kaliszyk, O'Connor).</li>
<li><a href="http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath">ForMath</a>
project (Spitters, Krebbers, van der Weegen, Makarov):<ul>
<li> Fast computation inside Coq</li>
<li> Development of the <a href="https://github.com/math-classes/math-classes">math-classes</a> library using type classes.</li>
<li> Development of a simple ODE-solver. </li></ul>
</li>
</ul>
</p>
See the publications section for a longer description.<br>
<div align="center">
<a href="pub.html">[Publications]</a>
<a href="http://github.com/c-corn/corn">[Sources]</a>
</body>
</html>