Strathprints logo
Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

A universe of strictly positive families

Morris, Peter and Altenkirch, Thorsten and Ghani, Neil (2009) A universe of strictly positive families. International Journal of Foundations of Computer Science, 20 (1). pp. 83-107. ISSN 0129-0541

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

Abstract

In order to represent, compute and reason with advanced data types one must go beyond the traditional treatment of data types as being inductive types and, instead, consider them as inductive families. Strictly positive types (SPTs) form a grammar for defining inductive types and, consequently, a fundamental question in the the theory of inductive families is what constitutes a corresponding grammar for inductive families. This paper answers this question in the form of strictly positive families or SPFs. We show that these SPFs can be used to represent and compute with a variety of advanced data types and that generic programs can naturally be written over the universe of SPFs.

Item type: Article
ID code: 33725
Keywords: inductive families , data types, programming, Electronic computers. Computer science, Computer Science (miscellaneous)
Subjects: Science > Mathematics > Electronic computers. Computer science
Department: Faculty of Science > Computer and Information Sciences
Related URLs:
    Depositing user: Pure Administrator
    Date Deposited: 18 Oct 2011 14:52
    Last modified: 05 Sep 2014 11:08
    URI: http://strathprints.strath.ac.uk/id/eprint/33725

    Actions (login required)

    View Item