A universe of strictly positive families

Peter Morris, Thorsten Altenkirch, Neil Ghani

Research output: Contribution to journal › Article

10 Citations (Scopus)
1 Downloads (Pure)

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.
Original languageEnglish
Pages (from-to)83-107
Number of pages25
JournalInternational Journal of Foundations of Computer Science
Volume20
Issue number1
DOIs
Publication statusPublished - Feb 2009

Keywords

  • inductive families
  • data types
  • programming

Cite this

Morris, Peter ; Altenkirch, Thorsten ; Ghani, Neil. / A universe of strictly positive families. In: International Journal of Foundations of Computer Science. 2009 ; Vol. 20, No. 1. pp. 83-107.
@article{9bb0f513fdc2456d8c1738151e91b0fd,
title = "A universe of strictly positive families",
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.",
keywords = "inductive families , data types, programming",
author = "Peter Morris and Thorsten Altenkirch and Neil Ghani",
year = "2009",
month = "2",
doi = "10.1142/S0129054109006462",
language = "English",
volume = "20",
pages = "83--107",
journal = "International Journal of Foundations of Computer Science",
issn = "0129-0541",
number = "1",

}

Morris, P, Altenkirch, T & Ghani, N 2009, 'A universe of strictly positive families', International Journal of Foundations of Computer Science, vol. 20, no. 1, pp. 83-107. https://doi.org/10.1142/S0129054109006462

A universe of strictly positive families. / Morris, Peter; Altenkirch, Thorsten; Ghani, Neil.

In: International Journal of Foundations of Computer Science, Vol. 20, No. 1, 02.2009, p. 83-107.

Research output: Contribution to journal › Article

TY - JOUR

T1 - A universe of strictly positive families

AU - Morris, Peter

AU - Altenkirch, Thorsten

AU - Ghani, Neil

PY - 2009/2

Y1 - 2009/2

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

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

KW - inductive families

KW - data types

KW - programming

UR - http://www.cs.nott.ac.uk/~txa/publ/jcats07.pdf

U2 - 10.1142/S0129054109006462

DO - 10.1142/S0129054109006462

M3 - Article

VL - 20

SP - 83

EP - 107

JO - International Journal of Foundations of Computer Science

JF - International Journal of Foundations of Computer Science

SN - 0129-0541

IS - 1

ER -

Morris P, Altenkirch T, Ghani N. A universe of strictly positive families. International Journal of Foundations of Computer Science. 2009 Feb;20(1):83-107. https://doi.org/10.1142/S0129054109006462

Access to Document