diff --git a/admin/site/content/about.md b/admin/site/content/about.md --- a/admin/site/content/about.md +++ b/admin/site/content/about.md @@ -1,44 +1,53 @@ --- title: "About" menu: main: name: "About" weight: 6 --- -> This website is a reimagining of the [Archive of Formal Proofs](https://www.isa-afp.org/), a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover [Isabelle](http://isabelle.in.tum.de/). The entries are updated daily to match the [upstream repository](https://foss.heptapod.net/isa-afp/afp-2021). -> -> The repository for this website will be released freely in the summer of 2021. -> ## Development -> This is a project from the School of Informatics at the University of Edinburgh by: ->* Carlin MacKenzie, MInf Informatics -> * James Vaughan, PhD Student, [AIAI](http://web.inf.ed.ac.uk/aiai/) -> * Jacques Fleuriot, Director of Institute, [AIAI](http://web.inf.ed.ac.uk/aiai/) +The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, +mechanically checked in the theorem prover Isabelle. +It is organized in the way of a scientific journal. +[Submissions](/contribution) are refereed. + +The archive repository is hosted on [Heptapod](https://foss.heptapod.net/isa-afp/) to provide easy free access to archive entries. +The entries are tested and maintained continuously against the current stable release of Isabelle. +Older versions of archive entries will remain available. ## Editors The editors of the Archive of Formal Proofs are: * [Manuel Eberl](http://www.in.tum.de/~eberlm/), [Technische Universität München](http://www.tum.de/) * [Gerwin Klein](http://www.cse.unsw.edu.au/~kleing/), [Data61](http://www.data61.csiro.au) * [Tobias Nipkow](http://www.in.tum.de/~nipkow/), [Technische Universität München](http://www.tum.de/) * [Larry Paulson](http://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](http://www.cam.ac.uk/) * [René Thiemann](http://cl-informatik.uibk.ac.at/users/thiemann/), [University of Innsbruck](https://www.uibk.ac.at/) ## Why We aim to strengthen the community and to foster the development of formal proofs. We hope that the Archive will provide: * a resource of knowledge, examples, and libraries for users, * a large and relevant test bed of theories for Isabelle developers, and * a central, citable place for authors to publish their theories We encourage authors of publications that contain Isabelle developments to make their theories available in the Archive of Formal Proofs and to refer to the archive entry in their publication. It makes it easier for referees to 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. ## License All entries in the Archive of Formal Proofs are licensed under a [BSD-style License](LICENSE) or the [GNU LGPL](http://www.gnu.org/copyleft/lesser.html). This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions. 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. + +## Website +This website is the result of a project from the School of Informatics at the University of Edinburgh by: + * Carlin MacKenzie + * James Vaughan, [AIAI](http://web.inf.ed.ac.uk/aiai/) + * Jacques Fleuriot, [AIAI](http://web.inf.ed.ac.uk/aiai/) + +Integration and maintenance by: + * [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](http://www.tum.de/) \ No newline at end of file