Formalizing restriction categories
Chapman, James and Uustalu, Tarmo and Veltri, Niccolò (2017) Formalizing restriction categories. Journal of Formalized Reasoning, 10 (1). pp. 1-36. ISSN 1972-5787
Preview |
Text (Chapman-etal-JFR2017-Formalizing-restriction-categories)
Chapman_etal_JFR2017_Formalizing_restriction_categories.pdf Final Published Version License: 
Download (361kB)| Preview |
Abstract
Restriction categories are an abstract axiomatic framework by Cockett and Lack for reasoning about (generalizations of the idea of) partiality of functions. In a restriction category, every map defines an endomap on its domain, the corresponding partial identity map. Restriction categories cover a number of examples of different flavors and are sound and complete with respect to the more synthetic and concrete partial map categories. A partial map category is based on a given category (of total maps) and a map in it is a map from a subobject of the domain. In this paper, we report on an Agda formalization of the first chapters of the theory of restriction categories, including the challenging completeness result. We explain the mathematics formalized, comment on the design decisions we made for the formalization, and illustrate them at work.
ORCID iDs
Chapman, James
ORCID: https://orcid.org/0000-0001-9036-8252, Uustalu, Tarmo and Veltri, Niccolò;
Item type: Article ID code: 60204 Dates: DateEvent10 March 2017Published18 February 2017AcceptedKeywords: restriction categories, fuctions, Agda formalization, Electronic computers. Computer science, Computer Science(all) Subjects: Science > Mathematics > Electronic computers. Computer science Department: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 15 Mar 2017 14:27 Last modified: 29 Jan 2021 02:36 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/60204
CORE (COnnecting REpositories)
CORE (COnnecting REpositories)