Re-imagining the Isabelle Archive of Formal Proofs

Carlin MacKenzie; Fabian Huch; James Vaughan; Jacques Fleuriot

doi:10.1007/978-3-031-16681-5_11

Re-imagining the Isabelle Archive of Formal Proofs

Carlin MacKenzie^*, Fabian Huch, James Vaughan, Jacques Fleuriot

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

Since its inception in 2004 the Archive of Formal Proofs has grown in size but its interface and functionality have only been minimally improved. To transform the AFP into a more user-friendly and effective resource, we redesigned the website to meet modern web standards and practices. We ensure that our work is community-driven by basing the redesign on results from a survey of the Isabelle community. The site generation uses Hugo and is implemented as a proper Isabelle component, which also allows us to adapt the AFP metadata model to avoid inconsistencies in the future. Notable improvements include a responsive design, new theory browsing interface, integrated search, and enhanced navigation.

Original language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	15th International Conference
Editors	Kevin Buzzard, Temur Kutsia
Publisher	Springer
Pages	162-167
Number of pages	6
Volume	13467
ISBN (Electronic)	9783031166815
ISBN (Print)	9783031166808
DOIs	https://doi.org/10.1007/978-3-031-16681-5_11
Publication status	Published - 17 Sept 2022
Event	15th Conference on Intelligent Computer Mathematics - Tbilisi, Georgia Duration: 19 Sept 2022 → 23 Sept 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th Conference on Intelligent Computer Mathematics
Abbreviated title	CICM 2022
Country/Territory	Georgia
City	Tbilisi
Period	19/09/22 → 23/09/22

Keywords / Materials (for Non-textual outputs)

Archive of Formal Proofs
Isabelle
user experience
user interface

Access to Document

10.1007/978-3-031-16681-5_11

MacKenzieEtalCICM2023Re-imaginingTheIsabelleArchiveAccepted author manuscript, 606 KBLicence: Creative Commons: Attribution (CC-BY)

Cite this

@inproceedings{93fc5a54ffc14764aa678d289cee49d6,

title = "Re-imagining the Isabelle Archive of Formal Proofs",

abstract = "Since its inception in 2004 the Archive of Formal Proofs has grown in size but its interface and functionality have only been minimally improved. To transform the AFP into a more user-friendly and effective resource, we redesigned the website to meet modern web standards and practices. We ensure that our work is community-driven by basing the redesign on results from a survey of the Isabelle community. The site generation uses Hugo and is implemented as a proper Isabelle component, which also allows us to adapt the AFP metadata model to avoid inconsistencies in the future. Notable improvements include a responsive design, new theory browsing interface, integrated search, and enhanced navigation.",

keywords = "Archive of Formal Proofs, Isabelle, user experience, user interface",

author = "Carlin MacKenzie and Fabian Huch and James Vaughan and Jacques Fleuriot",

year = "2022",

month = sep,

day = "17",

doi = "10.1007/978-3-031-16681-5_11",

language = "English",

isbn = "9783031166808",

volume = "13467",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "162--167",

editor = "Kevin Buzzard and Temur Kutsia",

booktitle = "Intelligent Computer Mathematics",

address = "United Kingdom",

note = "15th Conference on Intelligent Computer Mathematics, CICM 2022 ; Conference date: 19-09-2022 Through 23-09-2022",

}

MacKenzie, C, Huch, F, Vaughan, J & Fleuriot, J 2022, Re-imagining the Isabelle Archive of Formal Proofs. in K Buzzard & T Kutsia (eds), Intelligent Computer Mathematics: 15th International Conference. vol. 13467, Lecture Notes in Computer Science, Springer, pp. 162-167, 15th Conference on Intelligent Computer Mathematics, Tbilisi, Georgia, 19/09/22. https://doi.org/10.1007/978-3-031-16681-5_11

Re-imagining the Isabelle Archive of Formal Proofs. / MacKenzie, Carlin; Huch, Fabian; Vaughan, James et al.
Intelligent Computer Mathematics: 15th International Conference. ed. / Kevin Buzzard; Temur Kutsia. Vol. 13467 Springer, 2022. p. 162-167 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Re-imagining the Isabelle Archive of Formal Proofs

AU - MacKenzie, Carlin

AU - Huch, Fabian

AU - Vaughan, James

AU - Fleuriot, Jacques

PY - 2022/9/17

Y1 - 2022/9/17

N2 - Since its inception in 2004 the Archive of Formal Proofs has grown in size but its interface and functionality have only been minimally improved. To transform the AFP into a more user-friendly and effective resource, we redesigned the website to meet modern web standards and practices. We ensure that our work is community-driven by basing the redesign on results from a survey of the Isabelle community. The site generation uses Hugo and is implemented as a proper Isabelle component, which also allows us to adapt the AFP metadata model to avoid inconsistencies in the future. Notable improvements include a responsive design, new theory browsing interface, integrated search, and enhanced navigation.

AB - Since its inception in 2004 the Archive of Formal Proofs has grown in size but its interface and functionality have only been minimally improved. To transform the AFP into a more user-friendly and effective resource, we redesigned the website to meet modern web standards and practices. We ensure that our work is community-driven by basing the redesign on results from a survey of the Isabelle community. The site generation uses Hugo and is implemented as a proper Isabelle component, which also allows us to adapt the AFP metadata model to avoid inconsistencies in the future. Notable improvements include a responsive design, new theory browsing interface, integrated search, and enhanced navigation.

KW - Archive of Formal Proofs

KW - Isabelle

KW - user experience

KW - user interface

UR - http://www.scopus.com/inward/record.url?scp=85138815608&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-16681-5_11

DO - 10.1007/978-3-031-16681-5_11

M3 - Conference contribution

AN - SCOPUS:85138815608

SN - 9783031166808

VL - 13467

T3 - Lecture Notes in Computer Science

SP - 162

EP - 167

BT - Intelligent Computer Mathematics

A2 - Buzzard, Kevin

A2 - Kutsia, Temur

PB - Springer

T2 - 15th Conference on Intelligent Computer Mathematics

Y2 - 19 September 2022 through 23 September 2022

ER -