A universe of strictly positive families

Peter Morris, Thorsten Altenkirch, Neil Ghani

Research output: Contribution to journalArticlepeer-review

13 Citations (Scopus)
1 Downloads (Pure)


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
Issue number1
Publication statusPublished - Feb 2009


  • inductive families
  • data types
  • programming


Dive into the research topics of 'A universe of strictly positive families'. Together they form a unique fingerprint.

Cite this