altenkirch_indexed_2015:
  type: article
  title: Indexed containers
  author:
  - Altenkirch, Thorsten
  - Ghani, Neil
  - Hancock, Peter
  - Mcbride, Conor
  - Morris, Peter
  date: 2015-01
  page-range: e5
  url:
    value: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/indexed-containers/FB9C7DC88A65E7529D39554379D9765F
    date: 2024-11-14
  serial-number:
    doi: 10.1017/S095679681500009X
    issn: 0956-7968, 1469-7653
  abstract: We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.
  parent:
    type: periodical
    title: Journal of Functional Programming
    volume: 25