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...

Fibred data types

Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik and Setzer, Anton (2013) Fibred data types. In: 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS). IEEE, New York, pp. 243-252. ISBN 9781479904136

Full text not available in this repository. Request a copy from the Strathclyde author

Abstract

Data types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory.