about.shtml 4.34 KB
Newer Older
1
2
<!DOCTYPE html>
<html lang="en">
lsf37's avatar
lsf37 committed
3
<head>
4
5
6
7
8
<meta charset="utf-8">
<title>Archive of Formal Proofs</title>
<link rel="stylesheet" type="text/css" href="front.css">
<link rel="icon" href="images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="rss.xml">
lsf37's avatar
lsf37 committed
9
</head>
10

lsf37's avatar
lsf37 committed
11
12
13
<body>

<table width="100%">
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
<tbody>
<tr>

<!-- Navigation -->
<td width="20%" align="center" valign="top">
  <p>&nbsp;</p>
  <a href="http://isabelle.in.tum.de">
    <img src="images/isabelle.png" width="100" height="86" border=0>
  </a>
  <p>&nbsp;</p>
  <p>&nbsp;</p>
  <table class="nav" width="80%">
    <tr>
      <td class="nav" width="100%"><a href="index.shtml">Home</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="about.shtml">About</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="submitting.shtml">Submission Guidelines</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="updating.shtml">Updating entries</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="using.shtml">Using entries</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="search.shtml">Search</a></td>
    </tr>
lsf37's avatar
lsf37 committed
44
    <tr>
45
46
47
48
49
50
51
52
53
54
55
56
      <td class="nav"><a href="statistics.shtml">Statistics</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="topics.shtml">Index</a></td>
    </tr>
    <tr>
      <td class="nav"><a href="download.shtml">Download</a></td>
    </tr>
  </table>
  <p>&nbsp;</p>
  <p>&nbsp;</p>
</td>
lsf37's avatar
lsf37 committed
57

58
59
60

<!-- Content -->
<td width="80%" valign="top">
lsf37's avatar
lsf37 committed
61
<div align="center">
62
63
64
65
66
67
  <p>&nbsp;</p>
  <h1><font class="first">A</font>rchive of
<font class="first">F</font>ormal
<font class="first">P</font>roofs</h1>
</h1>
  <p>&nbsp;</p>
lsf37's avatar
lsf37 committed
68
69
70
71
72
73
74
75
76

<table width="80%" class="descr">
  <tbody>
    <tr><td>

<h2>About</h2>
<p>The Archive of Formal Proofs is a collection of proof libraries, examples,
and larger scientific developments, mechanically checked in the theorem prover
<a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way
lsf37's avatar
lsf37 committed
77
of a scientific journal. <a href="submitting.shtml">Submissions</a> are
lsf37's avatar
lsf37 committed
78
79
refereed.</p>

80
81
<p>The archive repository is hosted on <a href="https://bitbucket.org">Bitbucket</a> to
provide easy free access to archive entries. The entries are
kleing's avatar
kleing committed
82
tested and maintained continuously against the current stable release of
lsf37's avatar
lsf37 committed
83
84
85
86
87
Isabelle. Older versions of archive entries will remain available.</p>

<h2>Editors</h2>
<p><a name="editors">The editors of the archive are</a></p>
<ul>
lsf37's avatar
lsf37 committed
88
<li><a href="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</a>,
Gerwin Klein's avatar
Gerwin Klein committed
89
    <a href="http://www.data61.csiro.au">Data61</a></li>
nipkow's avatar
nipkow committed
90
<li><a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>,
Lars Hupel's avatar
Lars Hupel committed
91
    <a href="http://www.tum.de/">Technische Universit&auml;t M&uuml;nchen</a></li>
lsf37's avatar
lsf37 committed
92
<li><a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
lsf37's avatar
lsf37 committed
93
    <a href="http://www.cam.ac.uk/">University of Cambridge</a></li>
Gerwin Klein's avatar
Gerwin Klein committed
94
95
<li><a href="http://cl-informatik.uibk.ac.at/users/thiemann/">René Thiemann</a>,
    <a href="https://www.uibk.ac.at/">University of Innsbruck</a></li>
lsf37's avatar
lsf37 committed
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
</ul>

<h2>Why</h2>
<p>We aim to strengthen the community and to foster the development of formal
proofs.</p>

<p>We hope that the archive will provide</p>
<ul>
<li>a resource of knowledge, examples, and libraries for users,</li>
<li>a large and relevant test bed of theories for Isabelle developers, and</li>
<li>a central, citable place for authors to publish their theories</li>
</ul>

<p>We encourage authors of publications that contain Isabelle developments
to make their theories available in the Archive of Formal Proofs and to refer
kleing's avatar
kleing committed
111
to the archive entry in their publication. It makes it easier for referees to
lsf37's avatar
lsf37 committed
112
113
114
115
116
117
check the validity of theorems (all entries in the archive are
mechanically checked), it makes it easier for readers of the publication to
understand details of your development, and it makes it easier to use and
build on your work.</p>

<h2>License</h2>
nipkow's avatar
The    
nipkow committed
118
<p>All entries in the Archive of Formal Proofs are licensed under 
lsf37's avatar
lsf37 committed
119
120
a <a href="LICENSE">BSD-style License</a> or
the <a href="http://www.gnu.org/copyleft/lesser.html">GNU LGPL</a>.
lsf37's avatar
lsf37 committed
121
This means they are free to download, free to use, free to change, and
lsf37's avatar
lsf37 committed
122
free to redistribute with minimal restrictions.</p>
lsf37's avatar
lsf37 committed
123
124
125
126
127

<p>The authors retain their full copyright on their original work,
including their right to make the development available under another, 
additional license in the future.</p>

128
129
130
131
132
133
134
135
136

    </td></tr>
  </tbody>
</table>

</div>
</td>

</tr>
lsf37's avatar
lsf37 committed
137
138
139
</tbody>
</table>

140

lsf37's avatar
lsf37 committed
141
</body>
142
</html>