Picture of smart phone in human hand

World leading smartphone and mobile technology research at Strathclyde...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including by Strathclyde researchers from the Department of Computer & Information Sciences involved in researching exciting new applications for mobile and smartphone technology. But the transformative application of mobile technologies is also the focus of research within disciplines as diverse as Electronic & Electrical Engineering, Marketing, Human Resource Management and Biomedical Enginering, among others.

Explore Strathclyde's Open Access research on smartphone technology now...

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

[img]
Preview
Text (Chapman-etal-JFR2017-Formalizing-restriction-categories)
Chapman_etal_JFR2017_Formalizing_restriction_categories.pdf - Final Published Version
License: Creative Commons Attribution 3.0 logo

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.