Towards a readable formalisation of category theory

Greg O'Keefe

doi:10.1016/j.entcs.2003.12.014

Towards a readable formalisation of category theory

Greg O'Keefe

Research output: Contribution to journal › Conference article › peer-review

5 Citations (Scopus)

Abstract

We formally develop category theory up to Yoneda's lemma, using Isabelle/HOL/Isar, and survey previous formalisations. By using recently added Isabelle features, we have produced a formal text that more closely approximates informal mathematics.

Original language	English
Pages (from-to)	212-228
Number of pages	17
Journal	Electronic Notes in Theoretical Computer Science
Volume	91
DOIs	https://doi.org/10.1016/j.entcs.2003.12.014
Publication status	Published - 16 Feb 2004
Event	Proceedings of Computing: The Australasian Theory Symposium (CATS) - Dunedin, New Zealand Duration: 19 Jan 2004 → 20 Jan 2004

Access to Document

10.1016/j.entcs.2003.12.014

Cite this

@article{4d80b307848c422f971556c054f294bf,

title = "Towards a readable formalisation of category theory",

abstract = "We formally develop category theory up to Yoneda's lemma, using Isabelle/HOL/Isar, and survey previous formalisations. By using recently added Isabelle features, we have produced a formal text that more closely approximates informal mathematics.",

keywords = "Category theory, Formalised mathematics, Theorem proving",

author = "Greg O'Keefe",

year = "2004",

month = feb,

day = "16",

doi = "10.1016/j.entcs.2003.12.014",

language = "English",

volume = "91",

pages = "212--228",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

note = "Proceedings of Computing: The Australasian Theory Symposium (CATS) ; Conference date: 19-01-2004 Through 20-01-2004",

}

TY - JOUR

T1 - Towards a readable formalisation of category theory

AU - O'Keefe, Greg

PY - 2004/2/16

Y1 - 2004/2/16

N2 - We formally develop category theory up to Yoneda's lemma, using Isabelle/HOL/Isar, and survey previous formalisations. By using recently added Isabelle features, we have produced a formal text that more closely approximates informal mathematics.

AB - We formally develop category theory up to Yoneda's lemma, using Isabelle/HOL/Isar, and survey previous formalisations. By using recently added Isabelle features, we have produced a formal text that more closely approximates informal mathematics.

KW - Category theory

KW - Formalised mathematics

KW - Theorem proving

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

U2 - 10.1016/j.entcs.2003.12.014

DO - 10.1016/j.entcs.2003.12.014

M3 - Conference article

SN - 1571-0661

VL - 91

SP - 212

EP - 228

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - Proceedings of Computing: The Australasian Theory Symposium (CATS)

Y2 - 19 January 2004 through 20 January 2004

ER -

Towards a readable formalisation of category theory

Abstract

Access to Document

Other files and links

Fingerprint

Cite this