Abstract
| Language | English |
|---|---|
| Pages | 83-107 |
| Number of pages | 25 |
| Journal | International Journal of Foundations of Computer Science |
| Volume | 20 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - Feb 2009 |
Keywords
- inductive families
- data types
- programming
Cite this
}
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
T2 - International Journal of Foundations of Computer Science
JF - International Journal of Foundations of Computer Science
SN - 0129-0541
IS - 1
ER -